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.

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

• LieModule.traceForm R L M = ((LinearMap.mul R (Module.End R M)).compl₁₂ ↑(LieModule.toEndomorphism R L M) ↑(LieModule.toEndomorphism R L M)).compr₂ (LinearMap.trace R M)

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 ∈ ⊤.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) ⟨x, 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) ⟨y, 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 = ⋯.toFinset.sum 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 ≤ N.idealizer) (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) (((LieModule.toEndomorphism R L M) x ∘ₗ (LieModule.toEndomorphism R L M) y).restrict 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 ≤ N.idealizer) : LieModule.traceForm R ↥↑I ↥↑N = (LieModule.traceForm R L M).restrict (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 ≤ N.idealizer) (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).

@[reducible, inline]

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

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) : 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 := (killingForm R L).orthogonal ↑I; { toSubmodule := __spread.0, lie_mem := ⋯ }

@[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) = (killingForm R L).orthogonal ↑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 = (killingForm R L).restrict (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) : (killingForm R L).restrict (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 ⊤

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.univ.sum 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.univ.sum fun (χ : LieModule.Weight K L M) => FiniteDimensional.finrank K ↥↑(LieModule.weightSpace M ⇑χ) • (LieModule.Weight.toLinear K L M χ).smulRight (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))