def IsSingularVector {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) {M : Type u_mod} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (v : M) : Prop

structure ChevalleyData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) : Type u_2

• rank : ℕ
• simpleCoroot : Fin self.rank → ↥Δ.𝔥
• posGen : Fin self.rank → 𝔤
• negGen : Fin self.rank → 𝔤
• posGen_mem (i : Fin self.rank) : self.posGen i ∈ Δ.𝔫_pos
• negGen_mem (i : Fin self.rank) : self.negGen i ∈ Δ.𝔫_neg
• bracket_ef (i : Fin self.rank) : ⁅self.posGen i, self.negGen i⁆ = ↑(self.simpleCoroot i)
• bracket_he (i : Fin self.rank) : ⁅↑(self.simpleCoroot i), self.posGen i⁆ = self.posGen i + self.posGen i
• bracket_hf (i : Fin self.rank) : ⁅↑(self.simpleCoroot i), self.negGen i⁆ = -(self.negGen i + self.negGen i)

theorem ChevalleyData.sl2_weight_integrality {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (i : Fin chev.rank) {V : Type u_mod} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [IsNoetherian R V] [Module.IsTorsionFree R V] [IsDomain R] [CharZero R] (v : V) (hv : v ≠ 0) (he : ⁅chev.posGen i, v⁆ = 0) (μ : R) (hh : ⁅↑(chev.simpleCoroot i), v⁆ = μ • v) : ∃ (n : ℕ), μ = ↑n

def ChevalleyData.IsDominantIntegral {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

def ChevalleyData.IsInWeightLattice {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem exercise_8_11 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [IsNoetherian R V] [Module.IsTorsionFree R V] [IsDomain R] [CharZero R] (hV : IsHighestWeightModule Δ V wt) (i : Fin chev.rank) : ∃ (n : ℕ), wt (chev.simpleCoroot i) = ↑n

theorem dominantIntegral_implies_finiteDim {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.IsTorsionFree R V] [IsDomain R] [CharZero R] [IsNoetherianRing R] (hV : IsHighestWeightModule Δ V wt) (hirr : LieModule.IsIrreducible R 𝔤 V) (hdom : chev.IsDominantIntegral wt) : Module.Finite R V

theorem proposition_8_12 {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (chev : ChevalleyData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.IsTorsionFree R V] [IsDomain R] [CharZero R] [IsNoetherianRing R] (hV : IsHighestWeightModule Δ V wt) (hirr : LieModule.IsIrreducible R 𝔤 V) : Module.Finite R V ↔ chev.IsDominantIntegral wt