Documentation

Mathlib.Algebra.Lie.Killing

The trace and Killing forms of a Lie algebra. #

Let L be a Lie algebra with coefficients in a commutative ring R. Suppose M is a finite, free R-module and we have a representation φ : L → End M. This data induces a natural bilinear form B on L, called the trace form associated to M; it is defined as B(x, y) = Tr (φ x) (φ y).

In the special case that M is L itself and φ is the adjoint representation, the trace form is known as the Killing form.

We define the trace / Killing form in this file and prove some basic properties.

Main definitions #

LieModule.traceForm: a finite, free representation of a Lie algebra L induces a bilinear form on L called the trace Form.
LieModule.traceForm_eq_zero_of_isNilpotent: the trace form induced by a nilpotent representation of a Lie algebra vanishes.
killingForm: the adjoint representation of a (finite, free) Lie algebra L induces a bilinear form on L via the trace form construction.
LieAlgebra.IsKilling: a typeclass encoding the fact that a Lie algebra has a non-singular Killing form.
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.isSemisimple: if a Lie algebra has non-singular Killing form then it is semisimple.
LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra: if the Killing form of a Lie algebra is non-singular, then its Cartan subalgebras are Abelian.
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 α.

TODO #

Prove that in characteristic zero, a semisimple Lie algebra has non-singular Killing form.

noncomputable def LieModule.traceForm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LinearMap.BilinForm R L

A finite, free representation of a Lie algebra L induces a bilinear form on L called the trace Form. See also killingForm.

Equations

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

Instances For

theorem LieModule.traceForm_apply_apply (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) :

((LieModule.traceForm R L M) x) y = (LinearMap.trace R M) ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y)

theorem LieModule.traceForm_comm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) :

((LieModule.traceForm R L M) x) y = ((LieModule.traceForm R L M) y) x

theorem LieModule.traceForm_isSymm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LinearMap.IsSymm (LieModule.traceForm R L M)

@[simp]

theorem LieModule.traceForm_flip (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

LinearMap.flip (LieModule.traceForm R L M) = LieModule.traceForm R L M

theorem LieModule.traceForm_apply_lie_apply (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : L) :

((LieModule.traceForm R L M) ⁅x, y⁆) z = ((LieModule.traceForm R L M) x) ⁅y, z⁆

The trace form of a Lie module is compatible with the action of the Lie algebra.

See also LieModule.traceForm_apply_lie_apply'.

theorem LieModule.traceForm_apply_lie_apply' (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : L) :

((LieModule.traceForm R L M) ⁅x, y⁆) z = -((LieModule.traceForm R L M) y) ⁅x, z⁆

Given a representation M of a Lie algebra L, the action of any x : L is skew-adjoint wrt the trace form.

@[simp]

theorem LieModule.lie_traceForm_eq_zero (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) :

⁅x, LieModule.traceForm R L M⁆ = 0

This lemma justifies the terminology "invariant" for trace forms.

@[simp]

theorem LieModule.traceForm_eq_zero_of_isNilpotent (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsReduced R] [LieModule.IsNilpotent R L M] :

LieModule.traceForm R L M = 0

@[simp]

theorem LieModule.traceForm_weightSpace_eq (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [LieModule.LinearWeights R L M] (χ : L → R) (x : L) (y : L) :

((LieModule.traceForm R L ↥↑(LieModule.weightSpace M χ)) x) y = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • (χ x * χ y)

theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} {y : L} (k : ℕ) (hx : x ∈ LieIdeal.lcs ⊤ L k) (hy : y ∈ LieSubmodule.ucs k ⊥) :

((LieModule.traceForm R L M) x) y = 0

The upper and lower central series of L are orthogonal wrt the trace form of any Lie module M.

theorem LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} {y : L} (hx : x ∈ LieModule.lowerCentralSeries R L L 1) (hy : y ∈ LieAlgebra.center R L) :

((LieModule.traceForm R L M) x) y = 0

@[simp]

theorem LieModule.traceForm_eq_zero_of_isTrivial (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsTrivial L M] :

LieModule.traceForm R L M = 0

theorem LieModule.eq_zero_of_mem_weightSpace_mem_posFitting (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] {B : LinearMap.BilinForm R M} (hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆) {m₀ : M} {m₁ : M} (hm₀ : m₀ ∈ LieModule.weightSpace M 0) (hm₁ : m₁ ∈ LieModule.posFittingComp R L M) :

(B m₀) m₁ = 0

Given a bilinear form B on a representation M of a nilpotent Lie algebra L, if B is invariant (in the sense that the action of L is skew-adjoint wrt B) then components of the Fitting decomposition of M are orthogonal wrt B.

theorem LieModule.trace_toEndomorphism_eq_zero_of_mem_lcs (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {k : ℕ} {x : L} (hk : 1 ≤ k) (hx : x ∈ LieModule.lowerCentralSeries R L L k) :

(LinearMap.trace R M) ((LieModule.toEndomorphism R L M) x) = 0

@[simp]

theorem LieModule.traceForm_lieSubalgebra_mk_left (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) {x : L} (hx : x ∈ L') (y : ↥L') :

((LieModule.traceForm R (↥L') M) { val := x, property := hx }) y = ((LieModule.traceForm R L M) x) ↑y

@[simp]

theorem LieModule.traceForm_lieSubalgebra_mk_right (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (L' : LieSubalgebra R L) {x : ↥L'} {y : L} (hy : y ∈ L') :

((LieModule.traceForm R (↥L') M) x) { val := y, property := hy } = ((LieModule.traceForm R L M) ↑x) y

theorem LieModule.traceForm_eq_sum_weightSpaceOf (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [LieAlgebra.IsNilpotent R L] [IsDomain R] [IsPrincipalIdealRing R] [LieModule.IsTriangularizable R L M] (z : L) :

LieModule.traceForm R L M = Finset.sum (Set.Finite.toFinset ⋯) fun (χ : R) => LieModule.traceForm R L ↥↑(LieModule.weightSpaceOf M χ z)

theorem LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [LieAlgebra.IsNilpotent R L] [IsDomain R] [IsPrincipalIdealRing R] :

(lieIdealSubalgebra R L (LieModule.lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L)).toSubmodule ≤ LinearMap.ker (LieModule.traceForm R L M)

theorem LieModule.isLieAbelian_of_ker_traceForm_eq_bot (R : Type u_1) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [LieAlgebra.IsNilpotent R L] [IsDomain R] [IsPrincipalIdealRing R] (h : LinearMap.ker (LieModule.traceForm R L M) = ⊥) :

A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian.

theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) (x : L) {y : L} (hy : y ∈ I) (hy' : optParam (∀ m ∈ N, ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y) m ∈ N) ⋯) :

(LinearMap.trace R M) ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y) = (LinearMap.trace R ↥↑N) (LinearMap.restrict ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y) hy')

theorem LieSubmodule.traceForm_eq_of_le_idealizer {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) :

LieModule.traceForm R ↥↑I ↥↑N = LinearMap.BilinForm.restrict (LieModule.traceForm R L M) (lieIdealSubalgebra R L I).toSubmodule

theorem LieSubmodule.traceForm_eq_zero_of_isTrivial {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) (x : L) {y : L} (hy : y ∈ I) [LieModule.IsTrivial ↥↑I ↥↑N] :

(LinearMap.trace R M) ((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y) = 0

Note that this result is slightly stronger than it might look at first glance: we only assume that N is trivial over I rather than all of L. This means that it applies in the important case of an Abelian ideal (which has M = L and N = I).

@[inline, reducible]

noncomputable abbrev killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] :

LinearMap.BilinForm R L

A finite, free (as an R-module) Lie algebra L carries a bilinear form on L.

This is a specialisation of LieModule.traceForm to the adjoint representation of L.

Equations

killingForm R L = LieModule.traceForm R L L

Instances For

theorem killingForm_apply_apply (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (y : L) :

((killingForm R L) x) y = (LinearMap.trace R L) ((LieAlgebra.ad R L) x ∘ₗ (LieAlgebra.ad R L) y)

theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R ↥H] {x₀ : L} {x₁ : L} (hx₀ : x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H) (hx₁ : x₁ ∈ LieModule.posFittingComp R (↥H) L) :

((killingForm R L) x₀) x₁ = 0

noncomputable def LieIdeal.killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

The orthogonal complement of an ideal with respect to the killing form is an ideal.

Equations

LieIdeal.killingCompl R L I = let __spread.0 := LinearMap.BilinForm.orthogonal (killingForm R L) ↑I; { toSubmodule := __spread.0, lie_mem := ⋯ }

Instances For

@[simp]

theorem LieIdeal.toSubmodule_killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

↑(LieIdeal.killingCompl R L I) = LinearMap.BilinForm.orthogonal (killingForm R L) ↑I

@[simp]

theorem LieIdeal.mem_killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {x : L} :

x ∈ LieIdeal.killingCompl R L I ↔ ∀ y ∈ I, ((killingForm R L) y) x = 0

theorem LieIdeal.coe_killingCompl_top (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] :

(lieIdealSubalgebra R L (LieIdeal.killingCompl R L ⊤)).toSubmodule = LinearMap.ker (killingForm R L)

theorem LieIdeal.killingForm_eq (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] (I : LieIdeal R L) [IsDomain R] [IsPrincipalIdealRing R] :

killingForm R ↥↑I = LinearMap.BilinForm.restrict (killingForm R L) (lieIdealSubalgebra R L I).toSubmodule

theorem LieIdeal.restrict_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

LinearMap.BilinForm.restrict (killingForm R L) (lieIdealSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥↑I) L

@[simp]

theorem LieIdeal.le_killingCompl_top_of_isLieAbelian (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] (I : LieIdeal R L) [IsDomain R] [IsPrincipalIdealRing R] [IsLieAbelian ↥↑I] :

I ≤ LieIdeal.killingCompl R L ⊤

class LieAlgebra.IsKilling (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] :

We say a Lie algebra is Killing if its Killing form is non-singular.

NB: This is not standard terminology (the literature does not seem to name Lie algebras with this property).

killingCompl_top_eq_bot : LieIdeal.killingCompl R L ⊤ = ⊥
We say a Lie algebra is Killing if its Killing form is non-singular.

Instances

@[simp]

theorem LieAlgebra.IsKilling.ker_killingForm_eq_bot (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] :

LinearMap.ker (killingForm R L) = ⊥

theorem LieAlgebra.IsKilling.killingForm_nondegenerate (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] :

LinearMap.BilinForm.Nondegenerate (killingForm R 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] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [LieSubalgebra.IsCartanSubalgebra H] :

LinearMap.ker (LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule) = ⊥

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

theorem LieAlgebra.IsKilling.restrict_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) :

LinearMap.BilinForm.restrict (killingForm R L) H.toSubmodule = LieModule.traceForm R (↥H) L

@[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] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [LieSubalgebra.IsCartanSubalgebra H] :

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] [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [LieSubalgebra.IsCartanSubalgebra H] :

LinearMap.BilinForm.Nondegenerate (LieModule.traceForm R (↥H) L)

instance LieAlgebra.IsKilling.isSemisimple (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] [IsDomain R] [IsPrincipalIdealRing R] :

LieAlgebra.IsSemisimple R L

The converse of this is true over a field of characteristic zero. There are counterexamples over fields with positive characteristic.

Equations

⋯ = ⋯

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

IsLieAbelian ↥H

Equations

⋯ = ⋯

theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul (K : Type u_2) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [LieAlgebra.IsNilpotent K L] [LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M] (x : L) (y : L) :

((LieModule.traceForm K L M) x) y = Finset.sum Finset.univ fun (χ : LieModule.Weight K L M) => FiniteDimensional.finrank K ↥↑(LieModule.weightSpace M ⇑χ) • (χ x * χ y)

theorem LieModule.traceForm_eq_sum_finrank_nsmul (K : Type u_2) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [LieAlgebra.IsNilpotent K L] [LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M] :

LieModule.traceForm K L M = Finset.sum Finset.univ fun (χ : LieModule.Weight K L M) => FiniteDimensional.finrank K ↥↑(LieModule.weightSpace M ⇑χ) • LinearMap.smulRight (LieModule.Weight.toLinear K L M χ) (LieModule.Weight.toLinear K L M χ)

theorem LieModule.range_traceForm_le_span_weight (K : Type u_2) (L : Type u_3) (M : Type u_4) [LieRing L] [AddCommGroup M] [LieRingModule L M] [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M] [LieAlgebra.IsNilpotent K L] [LieModule.LinearWeights K L M] [LieModule.IsTriangularizable K L M] :

LinearMap.range (LieModule.traceForm K L M) ≤ Submodule.span K (Set.range (LieModule.Weight.toLinear K L M))

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) [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] {α : ↥H → K} {β : ↥H → K} {x : L} {y : L} (hx : x ∈ LieAlgebra.rootSpace H α) (hy : y ∈ LieAlgebra.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) [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] {α : ↥H → K} {x : L} (hx : x ∈ LieAlgebra.rootSpace H α) (hx' : ∀ y ∈ LieAlgebra.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.

@[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) [LieSubalgebra.IsCartanSubalgebra H] [LieAlgebra.IsKilling K L] :

∀ (a m : ↥H), ((LieAlgebra.IsKilling.cartanEquivDual H) a) m = (LinearMap.trace K L) ((LieModule.toEndomorphism K (↥H) L) a * (LieModule.toEndomorphism K (↥H) L) m)

@[simp]

theorem LieAlgebra.IsKilling.cartanEquivDual_symm_apply {K : Type u_2} {L : Type u_3} [LieRing L] [Field K] [LieAlgebra K L] [FiniteDimensional K L] (H : LieSubalgebra K L) [LieSubalgebra.IsCartanSubalgebra H] [LieAlgebra.IsKilling K L] :

∀ (a : ↥H →ₗ[K] K), (LinearEquiv.symm (LieAlgebra.IsKilling.cartanEquivDual H)) a = (LinearEquiv.symm (LinearEquiv.ofInjective (LieModule.traceForm K (↥H) L) ⋯)) ((LinearEquiv.symm (LinearEquiv.ofTop (LinearMap.range (LieModule.traceForm K (↥H) L)) ⋯)) a)

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) [LieSubalgebra.IsCartanSubalgebra H] [LieAlgebra.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.

Equations

LieAlgebra.IsKilling.cartanEquivDual H = LinearMap.BilinForm.toDual (LieModule.traceForm K (↥H) L) ⋯

Instances For

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) [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] (α : LieModule.Weight K (↥H) L) :

(LinearEquiv.symm (LieAlgebra.IsKilling.cartanEquivDual H)) (LieModule.Weight.toLinear K (↥H) L α) ∈ LieAlgebra.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) [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K 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.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) [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] :

⨅ (α : LieModule.Weight K (↥H) L), LieModule.Weight.ker = ⊥

@[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) [LieSubalgebra.IsCartanSubalgebra H] [LieAlgebra.IsKilling K L] :

LieAlgebra.corootSpace 0 = ⊥

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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] (x : ↥H) (α : ↥H → K) (hαx : α x = 0) (hx : x ∈ LieAlgebra.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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] (α : LieModule.Weight K (↥H) L) :

Disjoint LieModule.Weight.ker (lieIdealSubalgebra K (↥H) (LieAlgebra.corootSpace ⇑α)).toSubmodule

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} [LieSubalgebra.IsCartanSubalgebra H] [LieAlgebra.IsKilling K L] [CharZero K] (α : LieModule.Weight K (↥H) L) :

↥H

The coroot corresponding to a root.

Equations

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

Instances For

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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : LieModule.Weight.IsNonZero α) :

α ((LinearEquiv.symm (LieAlgebra.IsKilling.cartanEquivDual H)) (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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] {α : LieModule.Weight K (↥H) L} (hα : LieModule.Weight.IsNonZero α) :

α (LieAlgebra.IsKilling.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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] {α : LieModule.Weight K (↥H) L} :

LieAlgebra.IsKilling.coroot α = 0 ↔ LieModule.Weight.IsZero α

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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] (α : LieModule.Weight K (↥H) L) :

↑(LieAlgebra.corootSpace ⇑α) = Submodule.span K {LieAlgebra.IsKilling.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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] {α : LieModule.Weight K (↥H) L} :

LieAlgebra.corootSpace ⇑α = ⊥ ↔ LieModule.Weight.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} [LieSubalgebra.IsCartanSubalgebra H] [LieModule.IsTriangularizable K (↥H) L] [LieAlgebra.IsKilling K L] [CharZero K] (α : LieModule.Weight K (↥H) L) :

IsCompl LieModule.Weight.ker (Submodule.span K {LieAlgebra.IsKilling.coroot α})

@[simp]

theorem LieAlgebra.killingForm_of_equiv_apply {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x : L) (y : L) :

((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y

Given an equivalence e of Lie algebras from L to L', and elements x y : L, the respective Killing forms of L and L' satisfy κ'(e x, e y) = κ(x, y).

theorem LieAlgebra.isKilling_of_equiv {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsKilling R L] (e : L ≃ₗ⁅R⁆ L') :

LieAlgebra.IsKilling R L'

Given a Killing Lie algebra L, if L' is isomorphic to L, then L' is Killing too.

theorem LieEquiv.isKilling {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsKilling R L] (e : L ≃ₗ⁅R⁆ L') :

LieAlgebra.IsKilling R L'

Alias of LieAlgebra.isKilling_of_equiv.

Given a Killing Lie algebra L, if L' is isomorphic to L, then L' is Killing too.