Basic theory of sl₂ triples

Mathlib defines an abstract sl₂ triple (IsSl2Triple h e f: the relations ⁅e, f⁆ = h, ⁅h, e⁆ = 2e, ⁅h, f⁆ = -2f, with h ≠ 0) and the whole primitive-vector calculus that rests on it. This file adds three things Mathlib does not have.

The first is a supply of triples, none being exhibited in the special linear Lie algebra. For every pair i ≠ j of indices, the matrix units

e = Eᵢⱼ, f = Eⱼᵢ, h = Eᵢᵢ - Eⱼⱼ

form an sl₂ triple inside LieAlgebra.SpecialLinear.sl n R, over an arbitrary nontrivial commutative ring. These are the triples attached to the roots of sl n, and for n = 2 the triple is the whole Lie algebra: sl (Fin 2) R is free of rank 3 on e, f, h, so the Lie subalgebra IsSl2Triple.toLieSubalgebra generated by the standard triple is everything.

That last fact is what makes sl (Fin 2) R usable as the model sl₂: statements about a triple t which are false for a triple sitting inside a bigger Lie algebra become correct once t.toLieSubalgebra R = ⊤, and this file provides the model in which that hypothesis holds. For an arbitrary triple, IsSl2Triple.isSl2Triple_restrict regards it inside the subalgebra it generates, where IsSl2Triple.restrict_toLieSubalgebra_eq_top supplies that hypothesis.

The second is the presentation of sl₂ by its relations, for an arbitrary Lie algebra: a triple is linearly independent, so a triple generating a Lie algebra is a basis of it, and three elements of any Lie algebra obeying the same relations determine a homomorphism out of it. That is what carries a representation of the model sl₂ over to an abstract one, in TauCeti/Algebra/Lie/Sl2/Standard.lean.

The third is perfectness of a Lie algebra generated by a triple, in the form the module theory uses it: each of h, 2e and -2f is a bracket of triple elements, so an action of the algebra that composes to zero is already zero.

Main results

• Ado.isSl2Triple_single: for i ≠ j, the matrix units Eᵢⱼ, Eⱼᵢ and Eᵢᵢ - Eⱼⱼ form an sl₂ triple in sl n R. The three bracket relations are available separately as Ado.lie_single_single_eq_singleSubSingle, Ado.lie_singleSubSingle_single and Ado.lie_singleSubSingle_single_swap.
• Ado.slFinTwoBasis: the standard basis (e, f, h) of sl (Fin 2) R, obtained from the coordinate isomorphism Ado.slFinTwoEquivFun and identified vector by vector in Ado.slFinTwoBasis_zero, Ado.slFinTwoBasis_one and Ado.slFinTwoBasis_two. The rank 3 is the case n = Fin 2 of Ado.finrank_sl, and the Module.Free and Module.Finite instances come from there too.
• Ado.toLieSubalgebra_isSl2Triple_single_eq_top: in sl (Fin 2) R the subalgebra generated by a standard triple is the whole of sl (Fin 2) R. The underlying expansion of an arbitrary element in the triple is Ado.eq_smul_single_add_smul_single_add_smul_singleSubSingle.
• IsSl2Triple.isSl2Triple_restrict: an arbitrary triple regarded inside the subalgebra that it generates.
• IsSl2Triple.map: the image of a triple under a Lie algebra homomorphism that does not kill its Cartan element is a triple.
• IsSl2Triple.lieSubmoduleOfStable: a submodule stable under the raising and lowering elements of a triple is a Lie submodule over the subalgebra they generate.
• Ado.lieHomOfSl2Basis: from a basis obeying the sl₂ relations, three elements of another Lie algebra obeying the same relations determine a homomorphism, sending the basis to them (Ado.lieHomOfSl2Basis_apply).
• Ado.linearIndependent_isSl2Triple: the three elements of an sl₂ triple are linearly independent, being eigenvectors of ad h for the eigenvalues 2, -2 and 0, and Ado.basisOfIsSl2Triple: a generating sl₂ triple, as a basis of the Lie algebra it generates.
• Ado.lie_eq_zero_of_lie_lie_eq_zero: a Lie algebra generated by an sl₂ triple is perfect, so an action of it that composes to zero is zero.
• IsSl2Triple.eq_two_of_lie_h_e_eq_smul: the raising eigenvalue of an sl₂ triple is forced to be two in a torsion-free module.
• IsSl2Triple.rescale: rescaling the raising element by a unit and the lowering element by its inverse preserves an sl₂ triple.

Implementation notes

The special linear results are stated over an arbitrary commutative ring R; nontriviality of R is needed only where h ≠ 0 is claimed, and StrongRankCondition R only for the rank computation. Mathlib does not register LieRing.ofAssociativeRing as a global instance, so, as in Mathlib/Algebra/Lie/Classical.lean, it is a local instance here.

Linear independence of a triple is the eigenvector argument of Module.End.eigenvectors_linearIndependent', so it asks what that theorem asks — a domain of characteristic zero and a torsion-free Lie algebra — rather than a field: the eigenvalues 2, -2 and 0 need only be distinct, not invertible. The presentation Ado.lieHomOfSl2Basis needs neither, being a bilinearity argument over an arbitrary commutative ring.

The sl (Fin 2) R results are stated for an arbitrary pair i ≠ j of indices in Fin 2, not just for (0, 1): the opposite pair gives the opposite triple (-h, f, e), and both are standard.

References

This is the concrete input to Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose worked sl₂ is "LieAlgebra.SpecialLinear.sl (Fin 2) K with its standard triple", and whose classification targets carry the hypothesis htop : t.toLieSubalgebra K = ⊤ that Ado.toLieSubalgebra_isSl2Triple_single_eq_top discharges for that model.

theorem IsSl2Triple.eq_two_of_lie_h_e_eq_smul {S : Type u_1} {H : Type u_2} [CommRing S] [LieRing H] [LieAlgebra S H] [NoZeroSMulDivisors S H] {h e f : H} (t : IsSl2Triple h e f) {a : S} (ha : ⁅h, e⁆ = a • e) : a = 2

If the Cartan element of an sl₂ triple acts on its raising element by a scalar, that scalar is two, provided scalar multiplication on the ambient Lie algebra has no zero divisors.

theorem IsSl2Triple.rescale {S : Type u_1} {L : Type u_2} [CommRing S] [LieRing L] [LieAlgebra S L] {h e f : L} (t : IsSl2Triple h e f) (c : Sˣ) : IsSl2Triple h (↑c • e) (↑c⁻¹ • f)

Rescaling an sl₂ triple by a unit of the base ring. Scaling the raising element by c and the lowering element by c⁻¹ leaves their bracket, hence the Cartan element, unchanged.

The standard triples of sl n R

@[simp]

theorem Ado.lie_single_single_eq_singleSubSingle {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) (c : R) : ⁅(LieAlgebra.SpecialLinear.single i j hij) c, (LieAlgebra.SpecialLinear.single j i ⋯) 1⁆ = (LieAlgebra.SpecialLinear.singleSubSingle i j) c

⁅Eᵢⱼ, Eⱼᵢ⁆ = Eᵢᵢ - Eⱼⱼ in sl n R: the defining relation ⁅e, f⁆ = h of the standard sl₂ triple.

@[simp]

theorem Ado.lie_singleSubSingle_single {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) (c : R) : ⁅(LieAlgebra.SpecialLinear.singleSubSingle i j) 1, (LieAlgebra.SpecialLinear.single i j hij) c⁆ = 2 • (LieAlgebra.SpecialLinear.single i j hij) c

⁅Eᵢᵢ - Eⱼⱼ, Eᵢⱼ⁆ = 2 Eᵢⱼ in sl n R: the relation ⁅h, e⁆ = 2e of the standard sl₂ triple.

@[simp]

theorem Ado.neg_singleSubSingle {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (i j : n) (c : R) : -(LieAlgebra.SpecialLinear.singleSubSingle i j) c = (LieAlgebra.SpecialLinear.singleSubSingle j i) c

Swapping the two indices of Eᵢᵢ - Eⱼⱼ negates it.

@[simp]

theorem Ado.lie_singleSubSingle_single_swap {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) (c : R) : ⁅(LieAlgebra.SpecialLinear.singleSubSingle i j) 1, (LieAlgebra.SpecialLinear.single j i ⋯) c⁆ = -(2 • (LieAlgebra.SpecialLinear.single j i ⋯) c)

⁅Eᵢᵢ - Eⱼⱼ, Eⱼᵢ⁆ = -2 Eⱼᵢ in sl n R: the relation ⁅h, f⁆ = -2f of the standard sl₂ triple. It is the previous relation for the opposite pair of indices, since swapping them negates h.

theorem Ado.singleSubSingle_ne_zero {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) {c : R} (hc : c ≠ 0) : (LieAlgebra.SpecialLinear.singleSubSingle i j) c ≠ 0

Eᵢᵢ (c) - Eⱼⱼ (c) is nonzero in sl n R when i ≠ j and c ≠ 0: its (i, i) entry is c.

theorem Ado.isSl2Triple_single {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} [Nontrivial R] (hij : i ≠ j) : IsSl2Triple ((LieAlgebra.SpecialLinear.singleSubSingle i j) 1) ((LieAlgebra.SpecialLinear.single i j hij) 1) ((LieAlgebra.SpecialLinear.single j i ⋯) 1)

The standard sl₂ triple of sl n R. For i ≠ j the matrix units e = Eᵢⱼ, f = Eⱼᵢ and h = Eᵢᵢ - Eⱼⱼ satisfy the sl₂ relations. These are the concrete counterparts of the triples that LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero attaches to a root of a Killing-semisimple Lie algebra: e and f span the root spaces of εᵢ - εⱼ and of its negative, and h is the corresponding coroot.

sl (Fin 2) R as the model sl₂

@[simp]

theorem Ado.val_one_one_eq_neg_val_zero_zero {R : Type u_1} [CommRing R] (A : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) R)) : ↑A 1 1 = -↑A 0 0

The bottom-right entry of a trace-zero 2 × 2 matrix is minus its top-left entry.

def Ado.slFinTwoEquivFun (R : Type u_1) [CommRing R] : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) R) ≃ₗ[R] Fin 3 → R

The coordinates of a trace-zero 2 × 2 matrix in the standard basis (e, f, h), namely A ↦ (A 0 1, A 1 0, A 0 0). The inverse rebuilds A from them, using that the trace-zero condition forces A 1 1 = -A 0 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ado.slFinTwoEquivFun_apply {R : Type u_1} [CommRing R] (A : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) R)) : (slFinTwoEquivFun R) A = ![↑A 0 1, ↑A 1 0, ↑A 0 0]

@[simp]

theorem Ado.slFinTwoEquivFun_symm_apply {R : Type u_1} [CommRing R] (v : Fin 3 → R) : ↑((slFinTwoEquivFun R).symm v) = !![v 2, v 0; v 1, -v 2]

noncomputable def Ado.slFinTwoBasis (R : Type u_1) [CommRing R] : Module.Basis (Fin 3) R ↥(LieAlgebra.SpecialLinear.sl (Fin 2) R)

The standard basis of sl₂. The matrix units e = E₀₁, f = E₁₀ and h = E₀₀ - E₁₁ are a basis of sl (Fin 2) R; see Ado.slFinTwoBasis_apply.

Equations

• Ado.slFinTwoBasis R = Module.Basis.ofEquivFun (Ado.slFinTwoEquivFun R)

theorem Ado.slFinTwoBasis_apply (R : Type u_1) [CommRing R] (k : Fin 3) : ↑((slFinTwoBasis R) k) = ![Matrix.single 0 1 1, Matrix.single 1 0 1, Matrix.single 0 0 1 - Matrix.single 1 1 1] k

The three vectors of the standard basis of sl (Fin 2) R, as matrices: index 0 is the raising element e = E₀₁, index 1 the lowering element f = E₁₀, and index 2 the semisimple element h = E₀₀ - E₁₁. The individual cases, phrased inside sl (Fin 2) R rather than in matrices, are Ado.slFinTwoBasis_zero, Ado.slFinTwoBasis_one and Ado.slFinTwoBasis_two.

@[simp]

theorem Ado.slFinTwoBasis_zero (R : Type u_1) [CommRing R] : (slFinTwoBasis R) 0 = (LieAlgebra.SpecialLinear.single 0 1 ⋯) 1

The first standard basis vector of sl₂ is the raising element e = E₀₁.

@[simp]

theorem Ado.slFinTwoBasis_one (R : Type u_1) [CommRing R] : (slFinTwoBasis R) 1 = (LieAlgebra.SpecialLinear.single 1 0 ⋯) 1

The second standard basis vector of sl₂ is the lowering element f = E₁₀.

@[simp]

theorem Ado.slFinTwoBasis_two (R : Type u_1) [CommRing R] : (slFinTwoBasis R) 2 = (LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1

The third standard basis vector of sl₂ is the semisimple element h = E₀₀ - E₁₁.

theorem Ado.eq_smul_single_add_smul_single_add_smul_singleSubSingle {R : Type u_1} [CommRing R] (A : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) R)) {i j : Fin 2} (hij : i ≠ j) : A = ↑A i j • (LieAlgebra.SpecialLinear.single i j hij) 1 + ↑A j i • (LieAlgebra.SpecialLinear.single j i ⋯) 1 + ↑A i i • (LieAlgebra.SpecialLinear.singleSubSingle i j) 1

Every element of sl (Fin 2) R is a combination of a standard triple: the coefficients are read off from the entries, using A 1 1 = -A 0 0.

theorem Ado.toLieSubalgebra_isSl2Triple_single_eq_top {R : Type u_1} [CommRing R] [Nontrivial R] {i j : Fin 2} (hij : i ≠ j) : IsSl2Triple.toLieSubalgebra R ⋯ = ⊤

The standard triple generates sl₂. In sl (Fin 2) R the Lie subalgebra spanned by a standard sl₂ triple is everything, so sl (Fin 2) R is the model in which the classification hypothesis t.toLieSubalgebra R = ⊤ holds.

Homomorphisms determined by the sl₂ relations

noncomputable def Ado.lieHomOfSl2Basis {K : Type u_3} [CommRing K] {L : Type u_4} {L' : Type u_5} [LieRing L] [LieAlgebra K L] [LieRing L'] [LieAlgebra K L'] (b : Module.Basis (Fin 3) K L) (hb_ef : ⁅b 0, b 1⁆ = b 2) (hb_he : ⁅b 2, b 0⁆ = 2 • b 0) (hb_hf : ⁅b 2, b 1⁆ = -(2 • b 1)) (E F H : L') (hef : ⁅E, F⁆ = H) (hhe : ⁅H, E⁆ = 2 • E) (hhf : ⁅H, F⁆ = -(2 • F)) : L →ₗ⁅K⁆ L'

The sl₂ relations determine a homomorphism. If a basis (b₀, b₁, b₂) of a Lie algebra L obeys the sl₂ relations, then any three elements E, F, H of a Lie algebra L' obeying the same relations determine a Lie algebra homomorphism L →ₗ⁅K⁆ L' carrying the basis to them (Ado.lieHomOfSl2Basis_apply). Bracket preservation is bilinear, so it is enough to check it on the basis, where it is the nine brackets of the relations.

Equations

• Ado.lieHomOfSl2Basis b hb_ef hb_he hb_hf E F H hef hhe hhf = { toLinearMap := (b.constr K) ![E, F, H], map_lie' := ⋯ }

theorem Ado.lieHomOfSl2Basis_apply {K : Type u_3} [CommRing K] {L : Type u_4} {L' : Type u_5} [LieRing L] [LieAlgebra K L] [LieRing L'] [LieAlgebra K L'] (b : Module.Basis (Fin 3) K L) (hb_ef : ⁅b 0, b 1⁆ = b 2) (hb_he : ⁅b 2, b 0⁆ = 2 • b 0) (hb_hf : ⁅b 2, b 1⁆ = -(2 • b 1)) (E F H : L') (hef : ⁅E, F⁆ = H) (hhe : ⁅H, E⁆ = 2 • E) (hhf : ⁅H, F⁆ = -(2 • F)) (i : Fin 3) : (lieHomOfSl2Basis b hb_ef hb_he hb_hf E F H hef hhe hhf) (b i) = ![E, F, H] i

The homomorphism presented by the sl₂ relations sends the basis to the three chosen elements.

A triple inside the subalgebra it generates

theorem IsSl2Triple.map {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {L' : Type u_3} [LieRing L'] [LieAlgebra K L'] (t : IsSl2Triple h e f) (φ : L →ₗ⁅K⁆ L') (hφ : φ h ≠ 0) : IsSl2Triple (φ h) (φ e) (φ f)

An sl₂ triple is carried to an sl₂ triple by any Lie algebra homomorphism that does not kill the Cartan element. The three bracket relations hold for any homomorphism, so φ h ≠ 0 is the only hypothesis needed; an injective φ supplies it from t.h_ne_zero.

theorem IsSl2Triple.e_mem_toLieSubalgebra {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : e ∈ toLieSubalgebra K t

The raising element of an sl₂ triple belongs to the Lie subalgebra generated by the triple.

theorem IsSl2Triple.f_mem_toLieSubalgebra {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : f ∈ toLieSubalgebra K t

The lowering element of an sl₂ triple belongs to the Lie subalgebra generated by the triple.

theorem IsSl2Triple.h_mem_toLieSubalgebra {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : h ∈ toLieSubalgebra K t

The Cartan element of an sl₂ triple belongs to the Lie subalgebra generated by the triple.

theorem IsSl2Triple.isSl2Triple_restrict {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : IsSl2Triple ⟨h, ⋯⟩ ⟨e, ⋯⟩ ⟨f, ⋯⟩

An sl₂ triple, regarded inside the Lie subalgebra that it generates.

@[simp]

theorem IsSl2Triple.restrict_toLieSubalgebra_eq_top {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : toLieSubalgebra K ⋯ = ⊤

A triple regarded inside the subalgebra that it generates still generates the whole subalgebra.

def IsSl2Triple.lieSubmoduleOfStable {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (t : IsSl2Triple h e f) (S : Submodule K M) (he : ∀ m ∈ S, ⁅e, m⁆ ∈ S) (hf : ∀ m ∈ S, ⁅f, m⁆ ∈ S) : LieSubmodule K (↥(toLieSubalgebra K t)) M

A submodule stable under the raising and lowering elements of an sl₂ triple is a Lie submodule over the subalgebra they generate. Every element of t.toLieSubalgebra K is a combination c₁ • e + c₂ • f + c₃ • h, and the Cartan element is h = ⁅e, f⁆, so stability under e and f is all that has to be checked.

The underlying submodule is S itself, recorded in IsSl2Triple.lieSubmoduleOfStable_toSubmodule, and membership in IsSl2Triple.mem_lieSubmoduleOfStable.

Equations

• t.lieSubmoduleOfStable S he hf = { toSubmodule := S, lie_mem := ⋯ }

@[simp]

theorem IsSl2Triple.lieSubmoduleOfStable_toSubmodule {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (t : IsSl2Triple h e f) (S : Submodule K M) (he : ∀ m ∈ S, ⁅e, m⁆ ∈ S) (hf : ∀ m ∈ S, ⁅f, m⁆ ∈ S) : ↑(t.lieSubmoduleOfStable S he hf) = S

@[simp]

theorem IsSl2Triple.mem_lieSubmoduleOfStable {K : Type u_1} [CommRing K] {L : Type u_2} [LieRing L] [LieAlgebra K L] {h e f : L} {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (t : IsSl2Triple h e f) (S : Submodule K M) (he : ∀ m ∈ S, ⁅e, m⁆ ∈ S) (hf : ∀ m ∈ S, ⁅f, m⁆ ∈ S) {m : M} : m ∈ t.lieSubmoduleOfStable S he hf ↔ m ∈ S

Membership in IsSl2Triple.lieSubmoduleOfStable is membership in the submodule it is built from. This is the abstraction boundary for membership: a consumer should rewrite with this lemma rather than unfold the definition.

A generating triple as a basis

theorem Ado.linearIndependent_isSl2Triple {K : Type u_3} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_4} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) : LinearIndependent K ![e, f, h]

An sl₂ triple is linearly independent. Its three elements are eigenvectors of ad h for the eigenvalues 2, -2 and 0, which are distinct in characteristic zero.

noncomputable def Ado.basisOfIsSl2Triple {K : Type u_3} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_4} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) : Module.Basis (Fin 3) K L

A generating sl₂ triple is a basis. A Lie algebra spanned by an sl₂ triple is free of rank 3 on it: the triple spans by hypothesis and is linearly independent by Ado.linearIndependent_isSl2Triple.

Equations

• Ado.basisOfIsSl2Triple t htop = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Ado.basisOfIsSl2Triple_zero {K : Type u_3} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_4} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) : (basisOfIsSl2Triple t htop) 0 = e

The first vector of the basis of a generating triple is the raising element e.

@[simp]

theorem Ado.basisOfIsSl2Triple_one {K : Type u_3} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_4} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) : (basisOfIsSl2Triple t htop) 1 = f

The second vector of the basis of a generating triple is the lowering element f.

@[simp]

theorem Ado.basisOfIsSl2Triple_two {K : Type u_3} [CommRing K] [IsDomain K] [CharZero K] {L : Type u_4} [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) : (basisOfIsSl2Triple t htop) 2 = h

The third vector of the basis of a generating triple is the semisimple element h.

Perfectness of a generating triple

theorem Ado.lie_eq_zero_of_lie_lie_eq_zero {K : Type u_3} [Field K] [NeZero 2] {L : Type u_4} [LieRing L] [LieAlgebra K L] {M : Type u_5} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {h e f : L} {t : IsSl2Triple h e f} (htop : IsSl2Triple.toLieSubalgebra K t = ⊤) (hzero : ∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = 0) (x : L) (m : M) : ⁅x, m⁆ = 0

A Lie algebra generated by an sl₂ triple is perfect, in the form in which the statement is used: if the action of L on M composes to zero then it is already zero. Indeed each of h = ⁅e, f⁆, 2e = ⁅h, e⁆ and -2f = ⁅h, f⁆ is a bracket, so each acts as a composite.