def LieAlgebra.IsNilpotentElement (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (x : L) : Prop

def LieAlgebra.NilpotentCone (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] : Set L

theorem LieAlgebra.NilpotentCone.zero_mem (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] : 0 ∈ NilpotentCone R L

theorem LieAlgebra.NilpotentCone.smul_mem (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] {x : L} (hx : x ∈ NilpotentCone R L) (c : R) : c • x ∈ NilpotentCone R L

theorem LieAlgebra.NilpotentCone.mem_iff (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (x : L) : x ∈ NilpotentCone R L ↔ IsNilpotentElement R L x

structure LieAlgebra.AdjointGroupAction (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] : Type (max u_2 (u_3 + 1))

• G : Type u_3
• instGroup : Group self.G
• Ad : self.G → L ≃ₗ⁅R⁆ L
• Ad_mul (g₁ g₂ : self.G) : ⇑(self.Ad (g₁ * g₂)) = ⇑(self.Ad g₁) ∘ ⇑(self.Ad g₂)
• Ad_one : self.Ad One.one = LieEquiv.refl
• instTopologicalSpaceG : TopologicalSpace self.G
• instIrreducibleSpaceG : IrreducibleSpace self.G
• orbit_map_continuous (ts : TopologicalSpace L) (x : L) : Continuous fun (g : self.G) => (self.Ad g) x

def LieAlgebra.AdjointOrbit {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (Gact : AdjointGroupAction R L) (x : L) : Set L

def LieAlgebra.IsAdjointConjugate {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (Gact : AdjointGroupAction R L) (x y : L) : Prop

theorem LieAlgebra.AdjointOrbit.self_mem {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (Gact : AdjointGroupAction R L) (x : L) : x ∈ AdjointOrbit Gact x

theorem LieAlgebra.IsAdjointConjugate.refl {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (Gact : AdjointGroupAction R L) (x : L) : IsAdjointConjugate Gact x x

theorem LieAlgebra.IsNilpotentElement.map_lieEquiv {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (φ : L ≃ₗ⁅R⁆ L) {x : L} (hx : IsNilpotentElement R L x) : IsNilpotentElement R L (φ x)

theorem LieAlgebra.AdjointOrbit.subset_nilpotentCone {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] (Gact : AdjointGroupAction R L) {x : L} (hx : IsNilpotentElement R L x) : AdjointOrbit Gact x ⊆ NilpotentCone R L

def LieAlgebra.lieCentralizer (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (x : L) : Submodule R L

def LieAlgebra.IsRegularElement (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) : Prop

def LieAlgebra.IsRegularNilpotent (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] (x : L) : Prop

def LieAlgebra.IsAdInvariant {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (x : 𝔤) (V : Submodule ℂ 𝔤) : Prop

def LieAlgebra.IsSl2SubmoduleOf {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (h e f : 𝔤) (V : Submodule ℂ 𝔤) : Prop

def LieAlgebra.IsSl2IrreducibleSubmoduleOf {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (h e f : 𝔤) (V : Submodule ℂ 𝔤) : Prop

def LieAlgebra.IsSl2SubmoduleOf.toLieSubmodule {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hV : IsSl2SubmoduleOf h e f V) : LieSubmodule ℂ (↥(IsSl2Triple.toLieSubalgebra ℂ t)) 𝔤

@[simp]

theorem LieAlgebra.IsSl2SubmoduleOf.toLieSubmodule_toSubmodule {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hV : IsSl2SubmoduleOf h e f V) : ↑(toLieSubmodule t hV) = V

def LieAlgebra.IsSl2IrreducibleLieSubmodule {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) (V : LieSubmodule ℂ (↥(IsSl2Triple.toLieSubalgebra ℂ t)) 𝔤) : Prop

theorem LieAlgebra.lieSubmodule_isSl2SubmoduleOf {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) (W : LieSubmodule ℂ (↥(IsSl2Triple.toLieSubalgebra ℂ t)) 𝔤) : IsSl2SubmoduleOf h e f ↑W

theorem LieAlgebra.IsSl2IrreducibleSubmoduleOf.toIsSl2IrreducibleLieSubmodule {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) : IsSl2IrreducibleLieSubmodule t (IsSl2SubmoduleOf.toLieSubmodule t ⋯)

structure LieAlgebra.RootSystemData (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] : Type u_4

• rankVal : ℕ
• rank_pos : 0 < self.rankVal
• rank_eq : self.rankVal = rank ℂ 𝔤
• simpleRootVector : Fin self.rankVal → 𝔤
• simpleCorootVector : Fin self.rankVal → 𝔤
• simpleCoroot : Fin self.rankVal → 𝔤
• halfSumPosCoroots : 𝔤
• lie_simpleRootVector_simpleCorootVector (i j : Fin self.rankVal) : ⁅self.simpleRootVector i, self.simpleCorootVector j⁆ = if i = j then self.simpleCoroot i else 0
• simpleRootVector_ne_zero (i : Fin self.rankVal) : self.simpleRootVector i ≠ 0
• simpleCorootVector_ne_zero (i : Fin self.rankVal) : self.simpleCorootVector i ≠ 0
• halfSumPosCoroots_regular : Module.finrank ℂ ↥(lieCentralizer ℂ 𝔤 self.halfSumPosCoroots) = rank ℂ 𝔤
• no_joint_centralizer (v : 𝔤) : ⁅self.halfSumPosCoroots, v⁆ = 0 → ⁅∑ i : Fin self.rankVal, self.simpleRootVector i, v⁆ = 0 → v = 0
• halfSumPosCoroots_odd_dim_irreducibles {h e f : 𝔤} (_hprinc_h : h = 2 • self.halfSumPosCoroots) (_hprinc_e : e = ∑ i : Fin self.rankVal, self.simpleRootVector i) {V : Submodule ℂ 𝔤} (_hirr : IsSl2IrreducibleSubmoduleOf h e f V) : ¬Even (Module.finrank ℂ ↥V)

structure LieAlgebra.IsPrincipalSl2Triple {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] (h e f : 𝔤) extends IsSl2Triple h e f : Type u_3

• h_ne_zero : h ≠ 0
• lie_e_f : ⁅e, f⁆ = h
• lie_h_e_nsmul : ⁅h, e⁆ = 2 • e
• lie_h_f_nsmul : ⁅h, f⁆ = -(2 • f)
• rootData : RootSystemData 𝔤
• e_eq_sum : e = ∑ i : Fin self.rootData.rankVal, self.rootData.simpleRootVector i
• h_eq_two_rho : h = 2 • self.rootData.halfSumPosCoroots
• e_nilpotent : IsNilpotentElement ℂ 𝔤 e

theorem LieAlgebra.sl2_complete_reducibility_over_C {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (ht : IsSl2Triple h e f) : ∃ (n : ℕ) (V : Fin n → Submodule ℂ 𝔤), (∀ (i : Fin n), IsSl2IrreducibleSubmoduleOf h e f (V i)) ∧ DirectSum.IsInternal V

theorem LieAlgebra.nsmul_two_eq_zero_of_complex {M : Type u_4} [AddCommGroup M] [Module ℂ M] {x : M} (h : 2 • x = 0) : x = 0

theorem LieAlgebra.sl2_acts_trivially_on_one_dim_subspace {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (ht : IsSl2Triple h e f) {v : 𝔤} {c_e c_f : ℂ} (he_v : ⁅e, v⁆ = c_e • v) (hf_v : ⁅f, v⁆ = c_f • v) : ⁅e, v⁆ = 0 ∧ ⁅f, v⁆ = 0 ∧ ⁅h, v⁆ = 0

theorem LieAlgebra.principal_sl2_no_centralizer {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {v : 𝔤} (hv : v ≠ 0) (hh : ⁅h, v⁆ = 0) (he : ⁅e, v⁆ = 0) (_hf : ⁅f, v⁆ = 0) : False

theorem LieAlgebra.sl2_irreducible_submodule_dim {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) : ∃ (n : ℕ), 1 ≤ n ∧ Module.finrank ℂ ↥V = n + 1

theorem LieAlgebra.sl2_integration_minus_one_acts_trivially {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (n : ℕ) : Module.finrank ℂ ↥V = n + 1 → (-1) ^ n = 1

theorem LieAlgebra.principal_sl2_even_weights {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (n : ℕ) (hn : Module.finrank ℂ ↥V = n + 1) : Even n

theorem LieAlgebra.principal_sl2_highest_weight_even {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (n : ℕ) : Module.finrank ℂ ↥V = n + 1 → Even n

theorem LieAlgebra.h_eigenvalues_are_even {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) : ∃ (m : ℕ), 0 < m ∧ Module.finrank ℂ ↥V = 2 * m + 1

theorem LieAlgebra.lieCentralizer_smul_eq {K : Type u_4} [Field K] {L : Type u_5} [LieRing L] [LieAlgebra K L] {c : K} (hc : c ≠ 0) (x : L) : lieCentralizer K L (c • x) = lieCentralizer K L x

theorem LieAlgebra.principal_sl2_h_is_regular {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) : Module.finrank ℂ ↥(lieCentralizer ℂ 𝔤 h) = rank ℂ 𝔤

theorem LieAlgebra.finrank_ker_of_invariant_direct_sum {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] {n : ℕ} {V : Fin n → Submodule ℂ 𝔤} (hint : DirectSum.IsInternal V) {φ : 𝔤 →ₗ[ℂ] 𝔤} (hinv : ∀ (i : Fin n), ∀ v ∈ V i, φ v ∈ V i) : Module.finrank ℂ ↥φ.ker = ∑ i : Fin n, Module.finrank ℂ ↥(V i ⊓ φ.ker)

theorem LieAlgebra.sl2_irrep_zero_weight_space_dim {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (ht : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (m : ℕ) (hm : 0 < m) (hdim : Module.finrank ℂ ↥V = 2 * m + 1) : Module.finrank ℂ ↥(V ⊓ LinearMap.ker ((ad ℂ 𝔤) h)) = 1

theorem LieAlgebra.sl2_irreducible_zero_weight_dim {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) : Module.finrank ℂ ↥(V ⊓ LinearMap.ker ((ad ℂ 𝔤) h)) = 1

theorem LieAlgebra.sl2_zero_weight_space_count {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} {n : ℕ} {V : Fin n → Submodule ℂ 𝔤} (hprinc : IsPrincipalSl2Triple h e f) (hirr : ∀ (i : Fin n), IsSl2IrreducibleSubmoduleOf h e f (V i)) (hint : DirectSum.IsInternal V) : Module.finrank ℂ ↥(lieCentralizer ℂ 𝔤 h) = n

theorem LieAlgebra.zero_weight_space_dim_eq_rank {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) {n : ℕ} {V : Fin n → Submodule ℂ 𝔤} (hirr : ∀ (i : Fin n), IsSl2IrreducibleSubmoduleOf h e f (V i)) (hint : DirectSum.IsInternal V) : n = rank ℂ 𝔤

theorem LieAlgebra.adjoint_decomposes_under_principal_sl2 {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) : ∃ (r : ℕ) (V : Fin r → Submodule ℂ 𝔤) (m : Fin r → ℕ), r = rank ℂ 𝔤 ∧ (∀ (i : Fin r), IsSl2IrreducibleSubmoduleOf h e f (V i)) ∧ (∀ (i : Fin r), Module.finrank ℂ ↥(V i) = 2 * m i + 1) ∧ (∀ (i : Fin r), 0 < m i) ∧ DirectSum.IsInternal V

theorem LieAlgebra.adjoint_decomposes_under_principal_sl2_lie {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) : ∃ (r : ℕ) (V : Fin r → LieSubmodule ℂ (↥(IsSl2Triple.toLieSubalgebra ℂ ⋯)) 𝔤) (m : Fin r → ℕ), r = rank ℂ 𝔤 ∧ (∀ (i : Fin r), IsSl2IrreducibleLieSubmodule ⋯ (V i)) ∧ (∀ (i : Fin r), Module.finrank ℂ ↥↑(V i) = 2 * m i + 1) ∧ (∀ (i : Fin r), 0 < m i) ∧ DirectSum.IsInternal fun (i : Fin r) => ↑(V i)

theorem LieAlgebra.sl2_raising_kernel_nonempty {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (he : IsNilpotentElement ℂ 𝔤 e) : V ⊓ LinearMap.ker ((ad ℂ 𝔤) e) ≠ ⊥

theorem LieAlgebra.ker_ad_e_ad_h_invariant {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hV : IsSl2SubmoduleOf h e f V) (v : 𝔤) : v ∈ V ⊓ LinearMap.ker ((ad ℂ 𝔤) e) → ((ad ℂ 𝔤) h) v ∈ V ⊓ LinearMap.ker ((ad ℂ 𝔤) e)

theorem LieAlgebra.sl2_irreducible_raising_kernel_dim_le_one {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) : Module.finrank ℂ ↥(V ⊓ LinearMap.ker ((ad ℂ 𝔤) e)) ≤ 1

theorem LieAlgebra.sl2_irreducible_raising_kernel_dim {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] {h e f : 𝔤} (t : IsSl2Triple h e f) {V : Submodule ℂ 𝔤} (hirr : IsSl2IrreducibleSubmoduleOf h e f V) (he : IsNilpotentElement ℂ 𝔤 e) : Module.finrank ℂ ↥(V ⊓ LinearMap.ker ((ad ℂ 𝔤) e)) = 1

theorem LieAlgebra.principal_nilpotent_is_regular {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) : IsRegularElement ℂ 𝔤 e

theorem LieAlgebra.principal_nilpotent_isRegularNilpotent {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) : IsRegularNilpotent ℂ 𝔤 e

structure LieAlgebra.BorelSubgroupData (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] (rsd : RootSystemData 𝔤) : Type (max (max (max u_4 (u_5 + 1)) (u_6 + 1)) (u_7 + 1))

• B : Type u_5
• instGroupB : Group self.B
• AdB : self.B → 𝔤 ≃ₗ⁅ℂ⁆ 𝔤
• AdB_mul (b₁ b₂ : self.B) : ⇑(self.AdB (b₁ * b₂)) = ⇑(self.AdB b₁) ∘ ⇑(self.AdB b₂)
• numPosRoots : ℕ
• rootVector : Fin self.numPosRoots → 𝔤
• isSimple : Fin self.numPosRoots → Prop
• instDecSimple : DecidablePred self.isSimple
• numSimple_eq_rank : {i : Fin self.numPosRoots | decide (self.isSimple i) = true}.card = rsd.rankVal
• simpleRootVectorBij : Fin rsd.rankVal → Fin self.numPosRoots
• simpleRootVectorBij_isSimple (j : Fin rsd.rankVal) : self.isSimple (self.simpleRootVectorBij j)
• simpleRootVectorBij_surj (i : Fin self.numPosRoots) : self.isSimple i → ∃ (j : Fin rsd.rankVal), self.simpleRootVectorBij j = i
• simpleRootVector_eq (j : Fin rsd.rankVal) : self.rootVector (self.simpleRootVectorBij j) = rsd.simpleRootVector j
• H_torus : Type u_6
• instGroupH : Group self.H_torus
• embedH : self.H_torus → self.B
• N_unip : Type u_7
• instGroupN : Group self.N_unip
• embedN : self.N_unip → self.B
• torus_scaling : self.H_torus → Fin self.numPosRoots → ℂˣ
• levi_decomp (b : self.B) : ∃ (t : self.H_torus) (n : self.N_unip), ∀ (x : 𝔤), (self.AdB b) x = (self.AdB (self.embedH t)) ((self.AdB (self.embedN n)) x)
• unip_orbit_fwd (n : self.N_unip) : ∃ (c : Fin self.numPosRoots → ℂ), (∀ (i : Fin self.numPosRoots), self.isSimple i → c i = 1) ∧ (self.AdB (self.embedN n)) (∑ j : Fin rsd.rankVal, self.rootVector (self.simpleRootVectorBij j)) = ∑ i : Fin self.numPosRoots, c i • self.rootVector i
• unip_orbit_bwd (c : Fin self.numPosRoots → ℂ) : (∀ (i : Fin self.numPosRoots), self.isSimple i → c i = 1) → ∃ (n : self.N_unip), (self.AdB (self.embedN n)) (∑ j : Fin rsd.rankVal, self.rootVector (self.simpleRootVectorBij j)) = ∑ i : Fin self.numPosRoots, c i • self.rootVector i
• torus_action_eq (t : self.H_torus) (i : Fin self.numPosRoots) : (self.AdB (self.embedH t)) (self.rootVector i) = ↑(self.torus_scaling t i) • self.rootVector i
• torus_simple_surj (s : Fin rsd.rankVal → ℂˣ) : ∃ (t : self.H_torus), ∀ (j : Fin rsd.rankVal), self.torus_scaling t (self.simpleRootVectorBij j) = s j

theorem LieAlgebra.BorelSubgroupData.levi_product {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {rsd : RootSystemData 𝔤} (BD : BorelSubgroupData 𝔤 rsd) (t : BD.H_torus) (n : BD.N_unip) : ∃ (b : BD.B), ∀ (x : 𝔤), (BD.AdB b) x = (BD.AdB (BD.embedH t)) ((BD.AdB (BD.embedN n)) x)

def LieAlgebra.BorelSubgroupData.regularNilpotentSet {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {rsd : RootSystemData 𝔤} (BD : BorelSubgroupData 𝔤 rsd) : Set 𝔤

def LieAlgebra.BorelSubgroupData.borelOrbit {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {rsd : RootSystemData 𝔤} (BD : BorelSubgroupData 𝔤 rsd) (e : 𝔤) : Set 𝔤

theorem LieAlgebra.principal_nilpotent_borel_orbit {𝔤 : Type u_3} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] {h e f : 𝔤} (hprinc : IsPrincipalSl2Triple h e f) (BD : BorelSubgroupData 𝔤 hprinc.rootData) : BD.borelOrbit e = BD.regularNilpotentSet

theorem LieAlgebra.exists_regular_and_cartan_engel {K : Type u_3} [Field K] {L' : Type u_4} [LieRing L'] [LieAlgebra K L'] [Module.Finite K L'] [Infinite K] : ∃ (x : L'), IsRegular K x ∧ (LieSubalgebra.engel K x).IsCartanSubalgebra

theorem LieAlgebra.exists_cartan_finrank_eq_rank {K : Type u_3} [Field K] {L' : Type u_4} [LieRing L'] [LieAlgebra K L'] [Module.Finite K L'] [Infinite K] : ∃ (H : LieSubalgebra K L'), H.IsCartanSubalgebra ∧ Module.finrank K ↥H = rank K L'

theorem LieAlgebra.NilpotentCone.dim_eq (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] [Module.Finite R L] [Module.Free R L] [IsSemisimple R L] (H : LieSubalgebra R L) (hH : H.IsCartanSubalgebra) : Module.finrank R ↥H = rank R L

theorem LieAlgebra.NilpotentCone.nonempty_of_isSemisimple (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] [Nontrivial 𝔤] : (NilpotentCone ℂ 𝔤).Nonempty

theorem regularNilpotentOrbit_isOpen_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : LieAlgebra.AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : LieAlgebra.IsNilpotentElement ℂ 𝔤 e) (he_reg : LieAlgebra.IsRegularElement ℂ 𝔤 e) : ∃ (U : Set 𝔤), IsOpen U ∧ LieAlgebra.AdjointOrbit Gact e ∩ LieAlgebra.NilpotentCone ℂ 𝔤 = U ∩ LieAlgebra.NilpotentCone ℂ 𝔤

theorem adjointAction_continuous_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : LieAlgebra.AdjointGroupAction ℂ 𝔤) (g : Gact.G) : Continuous fun (x : 𝔤) => (Gact.Ad g) x

theorem nilpotent_conjugate_into_orbit_closure_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : LieAlgebra.AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : LieAlgebra.IsNilpotentElement ℂ 𝔤 e) (he_reg : LieAlgebra.IsRegularElement ℂ 𝔤 e) (x : 𝔤) (hx : LieAlgebra.IsNilpotentElement ℂ 𝔤 x) : ∃ (g : Gact.G), (Gact.Ad g) x ∈ closure (LieAlgebra.AdjointOrbit Gact e)

theorem regularNilpotentOrbit_isDense_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [LieAlgebra.IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : LieAlgebra.AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : LieAlgebra.IsNilpotentElement ℂ 𝔤 e) (he_reg : LieAlgebra.IsRegularElement ℂ 𝔤 e) : LieAlgebra.NilpotentCone ℂ 𝔤 ⊆ closure (LieAlgebra.AdjointOrbit Gact e)

theorem LieAlgebra.NilpotentCone.regularNilpotentOrbit_openDense_in_N (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) : (∃ (U : Set 𝔤), IsOpen U ∧ AdjointOrbit Gact e ∩ NilpotentCone ℂ 𝔤 = U ∩ NilpotentCone ℂ 𝔤) ∧ NilpotentCone ℂ 𝔤 ⊆ closure (AdjointOrbit Gact e)

theorem LieAlgebra.NilpotentCone.regularNilpotentOrbit_isOpen_in_N (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) : ∃ (U : Set 𝔤), IsOpen U ∧ AdjointOrbit Gact e ∩ NilpotentCone ℂ 𝔤 = U ∩ NilpotentCone ℂ 𝔤

theorem LieAlgebra.NilpotentCone.regularNilpotentOrbit_isDense_in_N (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) : NilpotentCone ℂ 𝔤 ⊆ closure (AdjointOrbit Gact e)

theorem LieAlgebra.NilpotentCone.regularNilpotentOrbit_isDense_in_N_pointwise (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) (x : 𝔤) : x ∈ NilpotentCone ℂ 𝔤 → ∀ (U : Set 𝔤), IsOpen U → x ∈ U → (U ∩ AdjointOrbit Gact e ∩ NilpotentCone ℂ 𝔤).Nonempty

theorem LieAlgebra.adjointOrbit_isIrreducible (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (_he_nil : IsNilpotentElement ℂ 𝔤 e) (_he_reg : IsRegularElement ℂ 𝔤 e) : IsIrreducible (AdjointOrbit Gact e)

theorem LieAlgebra.NilpotentCone.principal_orbit_open_dense (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) : (∃ (U : Set 𝔤), IsOpen U ∧ AdjointOrbit Gact e ∩ NilpotentCone ℂ 𝔤 = U ∩ NilpotentCone ℂ 𝔤) ∧ ∀ x ∈ NilpotentCone ℂ 𝔤, ∀ (U : Set 𝔤), IsOpen U → x ∈ U → (U ∩ AdjointOrbit Gact e ∩ NilpotentCone ℂ 𝔤).Nonempty

theorem LieAlgebra.NilpotentCone.regularNilpotent_conjugate (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {x y : 𝔤} (hx_nil : IsNilpotentElement ℂ 𝔤 x) (hx_reg : IsRegularElement ℂ 𝔤 x) (hy_nil : IsNilpotentElement ℂ 𝔤 y) (hy_reg : IsRegularElement ℂ 𝔤 y) : IsAdjointConjugate Gact x y

theorem LieAlgebra.NilpotentCone.isIrreducible (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) [Nontrivial 𝔤] : IsIrreducible (NilpotentCone ℂ 𝔤)

structure LieAlgebra.NilpotentConeCoordinateRing (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] : Type (max (u_2 + 1) (u_3 + 1))

• carrier : Type u_2
• instCommRing : CommRing self.carrier
• instAlgebra : Algebra ℂ self.carrier
• instNontrivial : Nontrivial self.carrier
• genericFiber : Type u_3
• instGenericFiberCommRing : CommRing self.genericFiber
• toGenericFiber : self.carrier →+* self.genericFiber
• instCarrierGenericFiberAlg : Algebra self.carrier self.genericFiber
• locSubmonoid : Submonoid self.carrier
• locSubmonoid_le_nonZeroDivisors (s : self.carrier) : s ∈ self.locSubmonoid → s ∈ nonZeroDivisors self.carrier
• instIsLocalization : IsLocalization self.locSubmonoid self.genericFiber
• toGenericFiber_eq : self.toGenericFiber = algebraMap self.carrier self.genericFiber
• instGenericFiberSemisimple : IsSemisimpleRing self.genericFiber

theorem LieAlgebra.NilpotentConeCoordinateRing.instIsReduced_of_structure (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsReduced Sg0.carrier

theorem LieAlgebra.NilpotentConeCoordinateRing.isDomain (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsDomain Sg0.carrier

theorem LieAlgebra.NilpotentConeCoordinateRing.instSpecIrreducible_of_structure (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IrreducibleSpace (PrimeSpectrum Sg0.carrier)

theorem LieAlgebra.NilpotentConeCoordinateRing.specIrreducible (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IrreducibleSpace (PrimeSpectrum Sg0.carrier)

theorem LieAlgebra.NilpotentConeCoordinateRing.toGenericFiber_injective (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : Function.Injective ⇑Sg0.toGenericFiber

theorem LieAlgebra.NilpotentConeCoordinateRing.genericFiber_isReduced (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsReduced Sg0.genericFiber

theorem LieAlgebra.NilpotentCone.irreducible_reduced_implies_domain (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (_hirr : IsIrreducible (NilpotentCone ℂ 𝔤)) (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsDomain Sg0.carrier

theorem LieAlgebra.NilpotentCone.coordinateRing_isDomain (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] [TopologicalSpace 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) {e : 𝔤} (he_nil : IsNilpotentElement ℂ 𝔤 e) (he_reg : IsRegularElement ℂ 𝔤 e) [Nontrivial 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsDomain Sg0.carrier

theorem LieAlgebra.NilpotentCone.isReduced (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Sg0 : NilpotentConeCoordinateRing 𝔤) : IsReduced Sg0.carrier

def LieAlgebra.maximalQuotientIdeal_17 (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : TwoSidedIdeal (UniversalEnvelopingAlgebra ℂ 𝔤)

@[reducible, inline]

abbrev LieAlgebra.MaximalQuotient_17 (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : Type u_1

def LieAlgebra.HasDomainAssociatedGraded (R : Type u_2) [Ring R] : Prop

theorem LieAlgebra.nontrivial_of_hasDomainAssociatedGraded (R : Type u_2) [Ring R] (h : HasDomainAssociatedGraded R) : Nontrivial R

theorem LieAlgebra.isDomain_of_hasDomainAssociatedGraded (R : Type u_2) [Ring R] (h : HasDomainAssociatedGraded R) : IsDomain R

structure LieAlgebra.SubMulFiltrationDomain (R : Type u_2) [Ring R] : Type u_2

• v : R → WithBot ℤ
• v_zero : self.v 0 = ⊥
• v_one : self.v 1 ≠ ⊥
• v_nonzero (a : R) : a ≠ 0 → self.v a ≠ ⊥
• v_submul (a b : R) : a ≠ 0 → b ≠ 0 → self.v a + self.v b ≤ self.v (a * b)
• gr_domain (a b : R) : a ≠ 0 → b ≠ 0 → ¬self.v a + self.v b < self.v (a * b)

theorem LieAlgebra.hasDomainAssociatedGraded_of_subMulFiltrationDomain {R : Type u_2} [Ring R] (w : SubMulFiltrationDomain R) : HasDomainAssociatedGraded R

structure LieAlgebra.SubMulFiltration (R : Type u_2) [Ring R] : Type u_2

• v : R → WithBot ℤ
• v_zero : self.v 0 = ⊥
• v_one : self.v 1 ≠ ⊥
• v_nonzero (a : R) : a ≠ 0 → self.v a ≠ ⊥
• v_submul (a b : R) : a ≠ 0 → b ≠ 0 → self.v a + self.v b ≤ self.v (a * b)

def LieAlgebra.SubMulFiltration.toSubMulFiltrationDomain {R : Type u_2} [Ring R] (F : SubMulFiltration R) (hgr : ∀ (a b : R), a ≠ 0 → b ≠ 0 → ¬F.v a + F.v b < F.v (a * b)) : SubMulFiltrationDomain R

structure LieAlgebra.PBWSymbolData {R : Type u_2} [Ring R] (v : R → WithBot ℤ) : Type (max 1 u_2)

• D : Type
• instRing : Ring self.D
• instDomain : IsDomain self.D
• σ : R → self.D
• σ_nonzero (a : R) : a ≠ 0 → self.σ a ≠ 0
• σ_cancel (a b : R) : a ≠ 0 → b ≠ 0 → v a + v b < v (a * b) → self.σ a * self.σ b = 0

theorem LieAlgebra.no_cancellation_of_pbwSymbolData {R : Type u_2} [Ring R] {v : R → WithBot ℤ} (data : PBWSymbolData v) (a b : R) : a ≠ 0 → b ≠ 0 → ¬v a + v b < v (a * b)

noncomputable def LieAlgebra.pbwSubMulFiltration_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltration (MaximalQuotient_17 𝔤 χ)

noncomputable def LieAlgebra.pbwSymbolData_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : PBWSymbolData (pbwSubMulFiltration_axiom 𝔤 χ).v

noncomputable def LieAlgebra.pbwSubMulFiltrationDomain_axiom (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltrationDomain (MaximalQuotient_17 𝔤 χ)

noncomputable def LieAlgebra.maximalQuotient_pbwSubMulFiltrationDomain_of_PBW (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltrationDomain (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_pbwFiltrationData (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : HasDomainAssociatedGraded (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_noZeroDivisors (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : NoZeroDivisors (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_nontrivial_of_pbw (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : Nontrivial (MaximalQuotient_17 𝔤 χ)

noncomputable def LieAlgebra.maximalQuotient_pbwDegree (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : MaximalQuotient_17 𝔤 χ → WithBot ℤ

theorem LieAlgebra.maximalQuotient_pbwDegree_spec (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : have v := maximalQuotient_pbwDegree 𝔤 χ; v 0 = ⊥ ∧ v 1 ≠ ⊥ ∧ (∀ (a : MaximalQuotient_17 𝔤 χ), a ≠ 0 → v a ≠ ⊥) ∧ ∀ (a b : MaximalQuotient_17 𝔤 χ), a ≠ 0 → b ≠ 0 → v (a * b) = v a + v b

noncomputable def LieAlgebra.maximalQuotient_pbwSubMulFiltration (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltration (MaximalQuotient_17 𝔤 χ)

noncomputable def LieAlgebra.maximalQuotient_pbwSymbolDataForFiltration (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : PBWSymbolData (maximalQuotient_pbwSubMulFiltration 𝔤 χ).v

noncomputable def LieAlgebra.maximalQuotient_pbwFiltrationAndSymbol (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : (F : SubMulFiltration (MaximalQuotient_17 𝔤 χ)) × PBWSymbolData F.v

noncomputable def LieAlgebra.maximalQuotient_pbwFiltration (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltration (MaximalQuotient_17 𝔤 χ)

noncomputable def LieAlgebra.maximalQuotient_pbwSymbolData (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : PBWSymbolData (maximalQuotient_pbwFiltration 𝔤 χ).v

theorem LieAlgebra.maximalQuotient_graded_noCancellation (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : have F := maximalQuotient_pbwFiltration 𝔤 χ; ∀ (a b : MaximalQuotient_17 𝔤 χ), a ≠ 0 → b ≠ 0 → ¬F.v a + F.v b < F.v (a * b)

noncomputable def LieAlgebra.maximalQuotient_subMulFiltrationDomain (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : SubMulFiltrationDomain (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_hasDomainAssociatedGraded (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : HasDomainAssociatedGraded (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_nontrivial (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : Nontrivial (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.maximalQuotient_isDomain (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [IsSemisimple ℂ 𝔤] (χ : ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤)) →ₐ[ℂ] ℂ) : IsDomain (MaximalQuotient_17 𝔤 χ)

theorem LieAlgebra.jacobson_morozov (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] {e : 𝔤} (he : IsNilpotentElement ℂ 𝔤 e) (hne : e ≠ 0) : ∃ (h : 𝔤) (f : 𝔤), IsSl2Triple h e f

theorem LieAlgebra.NilpotentCone.finitely_many_orbits (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℂ 𝔤] [Module.Finite ℂ 𝔤] [Module.Free ℂ 𝔤] [IsSemisimple ℂ 𝔤] (Gact : AdjointGroupAction ℂ 𝔤) : ∃ (S : Finset 𝔤), ∀ x ∈ NilpotentCone ℂ 𝔤, ∃ y ∈ S, IsAdjointConjugate Gact x y