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_restrictBilinear_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.

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] : L →ₗ[R] L →ₗ[R] R

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.

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

@[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.trace_toEndomorphism_weightSpace (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] (χ : L → R) (x : L) : (LinearMap.trace R ↥↑(LieModule.weightSpace M χ)) ((LieModule.toEndomorphism R L ↥↑(LieModule.weightSpace M χ)) x) = FiniteDimensional.finrank R ↥↑(LieModule.weightSpace M χ) • χ x

@[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 : M →ₗ[R] M →ₗ[R] R} (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

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 (_ : Set.Finite {χ : R | LieModule.weightSpaceOf M χ z ≠ ⊥})) 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) = ⊥) : IsLieAbelian L

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) (_ : ∀ m ∈ N, ⁅x, ((LieModule.toEndomorphism R L M) y) m⁆ ∈ N.carrier)) : (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 = Submodule.restrictBilinear (↑I) (LieModule.traceForm R L M)

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] : L →ₗ[R] L →ₗ[R] R

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

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) : LieIdeal R L

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

Equations

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

@[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) x) y = 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 = Submodule.restrictBilinear (↑I) (killingForm R L)

theorem LieIdeal.restrictBilinear_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Submodule.restrictBilinear (↑I) (killingForm R L) = 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] : Prop

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.

@[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.ker_restrictBilinear_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 (Submodule.restrictBilinear H.toSubmodule (killingForm R L)) = ⊥

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

theorem LieAlgebra.IsKilling.restrictBilinear_killingForm (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) : Submodule.restrictBilinear H.toSubmodule (killingForm R L) = 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) = ⊥

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

• (_ : LieAlgebra.IsSemisimple R L) = (_ : LieAlgebra.IsSemisimple R L)

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

• (_ : IsLieAbelian ↥H) = (_ : IsLieAbelian ↥H)

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 (LieModule.weight K L M) fun (χ : L → K) => 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 (χ : { x : L → K // x ∈ 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))

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