The Lie embedding of sl₂ attached to an sl₂ triple

An sl₂ triple t : IsSl2Triple h e f in a Lie algebra L over K is the same thing as a Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ L that does not kill the Cartan element: such a homomorphism carries the standard triple

E = E₀₁, F = E₁₀, H = E₀₀ - E₁₁

to a triple, and conversely IsSl2Triple.toLieHom sends E, F, H to e, f, h. Over a domain of characteristic zero, with L torsion-free, this homomorphism is injective, being the identification of sl (Fin 2) K with the Lie subalgebra t.toLieSubalgebra K spanned by the triple. This is the form in which statements about triples become statements about embeddings sl₂ ↪ 𝔤, and it is the map along which a representation of L restricts to sl₂.

Read through this dictionary, the Jacobson–Morozov theorem says that in a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, the images of E under the embeddings sl₂ ↪ 𝔤 are exactly the nonzero ad-nilpotent elements, and Kostant's conjugacy theorem says that two embeddings with the same value at E differ by an automorphism in TauCeti.expAdSubgroup.

Main definitions

• IsSl2Triple.toLieHom: the Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ L of a triple.
• IsSl2Triple.toLieSubalgebraEquiv: over a domain of characteristic zero, with L torsion-free, the Lie algebra isomorphism of sl (Fin 2) K with the subalgebra t.toLieSubalgebra K spanned by the triple.

Main results

• IsSl2Triple.toLieHom_apply: the formula A ↦ A₀₁ • e + A₁₀ • f + A₀₀ • h.
• IsSl2Triple.range_toLieHom: the range of t.toLieHom K is t.toLieSubalgebra K.
• IsSl2Triple.toLieHom_map and LieHom.eq_toLieHom_map: naturality, and every homomorphism φ out of sl (Fin 2) K with φ H ≠ 0 is the homomorphism of the image of the standard triple.
• IsSl2Triple.toLieHom_injective and LieHom.injective_iff_map_singleSubSingle_ne_zero: over a domain of characteristic zero, into a torsion-free Lie algebra, a homomorphism out of sl (Fin 2) K is injective if and only if it does not kill H; by LieHom.map_singleSubSingle_ne_zero_of_map_single_ne_zero, it suffices that it does not kill E.
• TauCeti.exists_injective_lieHom_slFinTwo_iff: Jacobson–Morozov for embeddings. An element e is the image of E under an embedding sl₂ ↪ L if and only if e ≠ 0 and ad e is nilpotent.
• TauCeti.exists_lieEquiv_comp_eq_of_apply_eq: Kostant's conjugacy for embeddings. An embedding sl₂ ↪ L and a homomorphism agreeing with it at E are conjugate by an automorphism in TauCeti.expAdSubgroup.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 7–9, Chapter VIII, §11.
• D. H. Collingwood and W. M. McGovern, Nilpotent Orbits in Semisimple Lie Algebras, Van Nostrand Reinhold, 1993, §3.3.

noncomputable def IsSl2Triple.toLieHom (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L

The Lie algebra homomorphism of an sl₂ triple. The homomorphism sl (Fin 2) K →ₗ⁅K⁆ L sending the standard triple E = E₀₁, F = E₁₀, H = E₀₀ - E₁₁ to e, f, h. Its values are computed by IsSl2Triple.toLieHom_apply.

theorem IsSl2Triple.toLieHom_slFinTwoBasis (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) (i : Fin 3) : (toLieHom K t) ((TauCeti.slFinTwoBasis K) i) = ![e, f, h] i

The homomorphism of a triple sends the standard basis of sl (Fin 2) K to e, f, h.

@[simp]

theorem IsSl2Triple.toLieHom_single_zero_one (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : (toLieHom K t) ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) = e

The homomorphism of a triple sends the raising element E₀₁ to e.

@[simp]

theorem IsSl2Triple.toLieHom_single_one_zero (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : (toLieHom K t) ((LieAlgebra.SpecialLinear.single 1 0 ⋯) 1) = f

The homomorphism of a triple sends the lowering element E₁₀ to f.

@[simp]

theorem IsSl2Triple.toLieHom_singleSubSingle (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) : (toLieHom K t) ((LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1) = h

The homomorphism of a triple sends the Cartan element E₀₀ - E₁₁ to h.

theorem IsSl2Triple.toLieHom_apply (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) (A : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) : (toLieHom K t) A = ↑A 0 1 • e + ↑A 1 0 • f + ↑A 0 0 • h

The homomorphism of a triple on an arbitrary trace-zero matrix A: it is A₀₁ • e + A₁₀ • f + A₀₀ • h.

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

The range of the homomorphism of a triple is the Lie subalgebra spanned by the triple.

theorem IsSl2Triple.toLieHom_map (K : Type u_1) {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {h e f : L} (t : IsSl2Triple h e f) {L' : Type u_3} [LieRing L'] [LieAlgebra K L'] (ψ : L →ₗ⁅K⁆ L') (hψ : ψ h ≠ 0) : toLieHom K ⋯ = ψ.comp (toLieHom K t)

Naturality. The homomorphism of the image of a triple under a Lie algebra homomorphism ψ is the composite with ψ.

@[simp]

theorem IsSl2Triple.toLieHom_isSl2Triple_single (K : Type u_1) [CommRing K] [Nontrivial K] : toLieHom K ⋯ = LieHom.id

The homomorphism of the standard triple of sl (Fin 2) K is the identity.

theorem IsSl2Triple.toLieHom_injective (K : Type u_1) {L : Type u_2} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) : Function.Injective ⇑(toLieHom K t)

The homomorphism of a triple is an embedding. Over a domain of characteristic zero, with L torsion-free, it sends the standard basis of sl (Fin 2) K to the linearly independent family e, f, h (TauCeti.linearIndependent_isSl2Triple).

noncomputable def IsSl2Triple.toLieSubalgebraEquiv (K : Type u_1) {L : Type u_2} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) ≃ₗ⁅K⁆ ↥(toLieSubalgebra K t)

sl₂ is isomorphic to the subalgebra spanned by a triple. Over a domain of characteristic zero, with L torsion-free, the homomorphism of a triple is a Lie algebra isomorphism of sl (Fin 2) K onto t.toLieSubalgebra K.

@[simp]

theorem IsSl2Triple.coe_toLieSubalgebraEquiv_apply (K : Type u_1) {L : Type u_2} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] {h e f : L} (t : IsSl2Triple h e f) (A : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K)) : ↑((toLieSubalgebraEquiv K t) A) = (toLieHom K t) A

The isomorphism of sl (Fin 2) K with the subalgebra spanned by a triple is the homomorphism of the triple.

theorem LieHom.eq_toLieHom_map {K : Type u_1} {L : Type u_2} [CommRing K] [Nontrivial K] [LieRing L] [LieAlgebra K L] (φ : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L) (hφ : φ ((LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1) ≠ 0) : φ = IsSl2Triple.toLieHom K ⋯

Every homomorphism out of sl₂ comes from a triple. A Lie algebra homomorphism φ out of sl (Fin 2) K that does not kill the Cartan element H = E₀₀ - E₁₁ is the homomorphism of the triple (φ H, φ E, φ F).

theorem LieHom.injective_iff_map_singleSubSingle_ne_zero {K : Type u_1} {L : Type u_2} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] (φ : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L) : Function.Injective ⇑φ ↔ φ ((LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1) ≠ 0

Over a domain of characteristic zero, a Lie algebra homomorphism out of sl (Fin 2) K into a torsion-free Lie algebra is injective if and only if it does not kill the Cartan element H = E₀₀ - E₁₁.

theorem LieHom.map_singleSubSingle_ne_zero_of_map_single_ne_zero {K : Type u_1} {L : Type u_2} [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] (φ : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L) (hφ : φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) ≠ 0) : φ ((LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1) ≠ 0

Over a domain of characteristic zero, a Lie algebra homomorphism out of sl (Fin 2) K into a torsion-free Lie algebra that does not kill the raising element E = E₀₁ does not kill the Cartan element H = E₀₀ - E₁₁ either, since ⁅H, E⁆ = 2 • E.

theorem TauCeti.exists_injective_lieHom_slFinTwo_iff {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {e : L} : (∃ (φ : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L), Function.Injective ⇑φ ∧ φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) = e) ↔ IsNilpotent ((LieAlgebra.ad K L) e) ∧ e ≠ 0

The Jacobson–Morozov theorem for embeddings. In a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, e is the image of the raising element E₀₁ under an injective Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ L if and only if e ≠ 0 and ad e is nilpotent.

theorem TauCeti.exists_lieEquiv_comp_eq_of_apply_eq {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra ℚ L] {φ φ' : ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) →ₗ⁅K⁆ L} (hφ : Function.Injective ⇑φ) (he : φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1) = φ' ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1)) : ∃ (ψ : L ≃ₗ⁅K⁆ L), ψ.toLinearEquiv ∈ expAdSubgroup K (φ ((LieAlgebra.SpecialLinear.single 0 1 ⋯) 1)) ∧ ψ.comp φ = φ'

Kostant's conjugacy theorem for embeddings. Let φ be an injective Lie algebra homomorphism sl (Fin 2) K →ₗ⁅K⁆ L into a finite-dimensional Lie algebra over a field of characteristic zero, and φ' any Lie algebra homomorphism agreeing with φ at the raising element E₀₁ (it is then injective too). Some automorphism ψ of L in the subgroup TauCeti.expAdSubgroup K e attached to their common value e satisfies ψ ∘ φ = φ'.