Roots of Lie algebras with non-degenerate Killing forms

The file contains definitions and results about roots of Lie algebras with non-degenerate Killing forms.

Main definitions

• LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra: if the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted to a Cartan subalgebra.
• LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra: if the Killing form of a Lie algebra is non-singular, then its Cartan subalgebras are Abelian.
• LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra: over a perfect field, if a Lie algebra has non-degenerate Killing form, Cartan subalgebras contain only semisimple elements.
• LieAlgebra.IsKilling.span_weight_eq_top: given a splitting Cartan subalgebra H of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of H.
• LieAlgebra.IsKilling.coroot: the coroot corresponding to a root.
• LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot: given a root α with respect to a Cartan subalgebra H, we have a natural decomposition of H as the kernel of α and the span of the coroot corresponding to α.
• LieAlgebra.IsKilling.finrank_rootSpace_eq_one: root spaces are one-dimensional.

theorem LieAlgebra.restrict_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : (killingForm R L).restrict H.toSubmodule = LieModule.traceForm R (↥H) L

theorem LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥

If the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted to a Cartan subalgebra.

@[simp]

theorem LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : LinearMap.ker (LieModule.traceForm R (↥H) L) = ⊥

theorem LieAlgebra.IsKilling.traceForm_cartan_nondegenerate (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : (LieModule.traceForm R (↥H) L).Nondegenerate

instance LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : IsLieAbelian ↥H

theorem LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α β : ↥H → K} {x y : L} (hx : x ∈ rootSpace H α) (hy : y ∈ rootSpace H β) (hαβ : α + β ≠ 0) : ((killingForm K L) x) y = 0

For any α and β, the corresponding root spaces are orthogonal with respect to the Killing form, provided α + β ≠ 0.

theorem LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α : ↥H → K} {x : L} (hx : x ∈ rootSpace H α) (hx' : ∀ y ∈ rootSpace H (-α), ((killingForm K L) x) y = 0) : x ∈ LinearMap.ker (killingForm K L)

Elements of the α root space which are Killing-orthogonal to the -α root space are Killing-orthogonal to all of L.

instance LieModule.Weight.instInvolutiveNegSubtypeMemLieSubalgebra {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] : InvolutiveNeg (Weight K (↥H) L)

@[simp]

theorem LieModule.Weight.coe_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} : ⇑(-α) = -⇑α

theorem LieModule.Weight.IsZero.neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} (h : α.IsZero) : (-α).IsZero

@[simp]

theorem LieModule.Weight.isZero_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} : (-α).IsZero ↔ α.IsZero

theorem LieModule.Weight.IsNonZero.neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} (h : α.IsNonZero) : (-α).IsNonZero

@[simp]

theorem LieModule.Weight.isNonZero_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} : (-α).IsNonZero ↔ α.IsNonZero

@[simp]

theorem LieModule.Weight.toLinear_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K (↥H) L] {α : Weight K (↥H) L} : toLinear K (↥H) L (-α) = -toLinear K (↥H) L α

theorem LieAlgebra.IsKilling.eq_zero_of_isNilpotent_ad_of_mem_isCartanSubalgebra (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsKilling K L] {x : L} (hx : x ∈ H) (hx' : IsNilpotent ((ad K L) x)) : x = 0

If a Lie algebra L has non-degenerate Killing form, the only element of a Cartan subalgebra whose adjoint action on L is nilpotent, is the zero element.

Over a perfect field a much stronger result is true, see LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra.

@[simp]

theorem LieAlgebra.IsKilling.corootSpace_zero_eq_bot (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsKilling K L] : corootSpace 0 = ⊥

noncomputable def LieAlgebra.IsKilling.cartanEquivDual {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsKilling K L] : ↥H ≃ₗ[K] Module.Dual K ↥H

The restriction of the Killing form to a Cartan subalgebra, as a linear equivalence to the dual.

@[simp]

theorem LieAlgebra.IsKilling.cartanEquivDual_apply_apply {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsKilling K L] (a✝ a✝¹ : ↥H) : ((cartanEquivDual H) a✝) a✝¹ = (LinearMap.trace K L) ((LieModule.toEnd K (↥H) L) a✝ * (LieModule.toEnd K (↥H) L) a✝¹)

noncomputable def LieAlgebra.IsKilling.coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] (α : LieModule.Weight K (↥H) L) : ↥H

The coroot corresponding to a root.

theorem LieAlgebra.IsKilling.traceForm_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] (α : LieModule.Weight K (↥H) L) (x : ↥H) : ((LieModule.traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)))⁻¹ • α x

@[simp]

theorem LieAlgebra.IsKilling.coroot_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) : coroot (-α) = -coroot α

theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L} {e f : L} (heα : e ∈ rootSpace H ⇑α) (hfα : f ∈ rootSpace H (-⇑α)) (aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e) : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))

theorem LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L) : (cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α

This is Proposition 4.18 from [carter2005] except that we use LieModule.exists_forall_lie_eq_smul instead of Lie's theorem (and so avoid assuming K has characteristic zero).

@[simp]

theorem LieAlgebra.IsKilling.span_weight_eq_top {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] : Submodule.span K (Set.range (LieModule.Weight.toLinear K (↥H) L)) = ⊤

Given a splitting Cartan subalgebra H of a finite-dimensional Lie algebra with non-singular Killing form, the corresponding roots span the dual space of H.

@[simp]

theorem LieAlgebra.IsKilling.span_weight_isNonZero_eq_top (K : Type u_2) (L : Type u_3) [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] : Submodule.span K (LieModule.Weight.toLinear K (↥H) L '' {α : LieModule.Weight K (↥H) L | α.IsNonZero}) = ⊤

@[simp]

theorem LieAlgebra.IsKilling.iInf_ker_weight_eq_bot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] : ⨅ (α : LieModule.Weight K (↥H) L), LieModule.Weight.ker = ⊥

theorem LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K] {x : L} (hx : x ∈ H) : ((ad K L) x).IsSemisimple

theorem LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K] {α : ↥H → K} {x : L} (hx : x ∈ rootSpace H α) (h : ↥H) : ⁅h, x⁆ = α h • x

theorem LieAlgebra.IsKilling.lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K] {α : LieModule.Weight K (↥H) L} {e f : L} (heα : e ∈ rootSpace H ⇑α) (hfα : f ∈ rootSpace H (-⇑α)) : ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α))

theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton' {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [PerfectField K] (α : LieModule.Weight K (↥H) L) : ↑(corootSpace ⇑α) = Submodule.span K {(cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)}

theorem LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (x : ↥H) (α : ↥H → K) (hαx : α x = 0) (hx : x ∈ corootSpace α) : x = 0

The contrapositive of this result is very useful, taking x to be the element of H corresponding to a root α under the identification between H and H^* provided by the Killing form.

theorem LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L) : Disjoint LieModule.Weight.ker (LieIdeal.toLieSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule

theorem LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) : α ((cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)) ≠ 0

theorem LieAlgebra.IsKilling.root_apply_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) : α (coroot α) = 2

@[simp]

theorem LieAlgebra.IsKilling.coroot_eq_zero_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} : coroot α = 0 ↔ α.IsZero

@[simp]

theorem LieAlgebra.IsKilling.coroot_zero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] [Nontrivial L] : coroot 0 = 0

theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L) : ↑(corootSpace ⇑α) = Submodule.span K {coroot α}

@[simp]

theorem LieAlgebra.IsKilling.corootSpace_eq_bot_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} : corootSpace ⇑α = ⊥ ↔ α.IsZero

theorem LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L) : IsCompl LieModule.Weight.ker (Submodule.span K {coroot α})

theorem LieAlgebra.IsKilling.traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} {x y : ↥H} (hx : x ∈ LieModule.Weight.ker) (hy : y ∈ Submodule.span K {coroot α}) : ((LieModule.traceForm K (↥H) L) x) y = 0

@[simp]

theorem LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L) : (LieModule.traceForm K (↥H) L).orthogonal (Submodule.span K {coroot α}) = LieModule.Weight.ker

@[simp]

theorem LieAlgebra.IsKilling.coroot_eq_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α β : LieModule.Weight K (↥H) L) : coroot α = coroot β ↔ α = β

theorem LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) : ∃ (h : L) (e : L) (f : L), IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)

theorem IsSl2Triple.h_eq_coroot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {h e f : L} (ht : IsSl2Triple h e f) (heα : e ∈ LieAlgebra.rootSpace H ⇑α) (hfα : f ∈ LieAlgebra.rootSpace H (-⇑α)) : h = ↑(LieAlgebra.IsKilling.coroot α)

theorem LieAlgebra.IsKilling.finrank_rootSpace_eq_one {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : Module.finrank K ↥(rootSpace H ⇑α) = 1

noncomputable def LieAlgebra.IsKilling.sl2SubalgebraOfRoot {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) : LieSubalgebra K L

The embedded sl₂ associated to a root.

theorem LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) {h e f : L} (t : IsSl2Triple h e f) (hte : e ∈ rootSpace H ⇑α) (htf : f ∈ rootSpace H (-⇑α)) {x : L} : x ∈ sl2SubalgebraOfRoot hα ↔ ∃ (c₁ : K) (c₂ : K) (c₃ : K), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

@[reducible, inline]

noncomputable abbrev LieSubalgebra.root {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] : Finset (LieModule.Weight K (↥H) L)

The collection of roots as a Finset.

theorem LieAlgebra.IsKilling.restrict_killingForm_eq_sum {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K] : (killingForm K L).restrict H.toSubmodule = ∑ α ∈ LieSubalgebra.root, (LieModule.Weight.toLinear K (↥H) L α).smulRight (LieModule.Weight.toLinear K (↥H) L α)