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.

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 y : L) : ((traceForm R L M) x) y = (LinearMap.trace R M) ((toEnd R L M) x ∘ₗ (toEnd 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 y : L) : ((traceForm R L M) x) y = ((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 (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 (traceForm R L M) = 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 y z : L) : ((traceForm R L M) ⁅x, y⁆) z = ((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 y z : L) : ((traceForm R L M) ⁅x, y⁆) z = -((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.

theorem LieModule.traceForm_lieInvariant (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.lieInvariant L (traceForm R L M)

@[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, 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] [IsReduced R] [IsNilpotent L M] : traceForm R L M = 0

@[simp]

theorem LieModule.traceForm_genWeightSpace_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] [IsDomain R] [IsPrincipalIdealRing R] [LieRing.IsNilpotent L] [IsNoetherian R M] [LinearWeights R L M] (χ : L → R) (x y : L) : ((traceForm R L ↥(genWeightSpace M χ)) x) y = Module.finrank R ↥(genWeightSpace 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 y : L} (k : ℕ) (hx : x ∈ ⊤.lcs L k) (hy : y ∈ LieSubmodule.ucs k ⊥) : ((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 y : L} (hx : x ∈ lowerCentralSeries R L L 1) (hy : y ∈ LieAlgebra.center R L) : ((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] [IsTrivial L M] : traceForm R L M = 0

theorem LieModule.eq_zero_of_mem_genWeightSpace_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] [LieRing.IsNilpotent L] {B : LinearMap.BilinForm R M} (hB : ∀ (x : L) (m n : M), (B ⁅x, m⁆) n = -(B m) ⁅x, n⁆) {m₀ m₁ : M} (hm₀ : m₀ ∈ genWeightSpace M 0) (hm₁ : m₁ ∈ 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_toEnd_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 ∈ lowerCentralSeries R L L k) : (LinearMap.trace R M) ((toEnd 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') : ((traceForm R (↥L') M) ⟨x, hx⟩) y = ((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') : ((traceForm R (↥L') M) x) ⟨y, hy⟩ = ((traceForm R L M) ↑x) y

theorem LieModule.traceForm_eq_sum_genWeightSpaceOf (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] [LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [NoZeroSMulDivisors R M] [IsNoetherian R M] [IsTriangularizable R L M] (z : L) : traceForm R L M = ∑ χ ∈ ⋯.toFinset, traceForm R L ↥(genWeightSpaceOf 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] [LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] : (LieIdeal.toLieSubalgebra R L (lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L)).toSubmodule ≤ LinearMap.ker (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] [LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M] (h : LinearMap.ker (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' : ∀ m ∈ N, ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) m ∈ N := ⋯) : (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) = (LinearMap.trace R ↥N) (((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd 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 (LieIdeal.toLieSubalgebra 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.toEnd R L M) x ∘ₗ (LieModule.toEnd 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.

theorem killingForm_apply_apply (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (x 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) [LieRing.IsNilpotent ↥H] {x₀ 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.

@[simp]

theorem LieIdeal.toSubmodule_killingCompl (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : ↑(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 ∈ 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] : (toLieSubalgebra R L (killingCompl R L ⊤)).toSubmodule = LinearMap.ker (killingForm R L)

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 (toLieSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥I) L

theorem LieIdeal.killingForm_eq (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] : killingForm R ↥I = (killingForm R L).restrict (toLieSubalgebra R L I).toSubmodule

@[simp]

theorem LieIdeal.le_killingCompl_top_of_isLieAbelian (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] [IsLieAbelian ↥I] : I ≤ 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] [LieRing.IsNilpotent L] [LinearWeights K L M] [IsTriangularizable K L M] (x y : L) : ((traceForm K L M) x) y = ∑ χ : Weight K L M, Module.finrank K ↥(genWeightSpace 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] [LieRing.IsNilpotent L] [LinearWeights K L M] [IsTriangularizable K L M] : traceForm K L M = ∑ χ : Weight K L M, Module.finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

See also LieModule.traceForm_eq_sum_finrank_nsmul' for an expression omitting the zero weights.

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] [LieRing.IsNilpotent L] [LinearWeights K L M] [IsTriangularizable K L M] : traceForm K L M = ∑ χ : Weight K L M with χ.IsNonZero, Module.finrank K ↥(genWeightSpace M ⇑χ) • (Weight.toLinear K L M χ).smulRight (Weight.toLinear K L M χ)

A variant of LieModule.traceForm_eq_sum_finrank_nsmul in which the sum is taken only over the non-zero weights.

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] [LieRing.IsNilpotent L] [LinearWeights K L M] [IsTriangularizable K L M] : LinearMap.range (traceForm K L M) ≤ Submodule.span K (Set.range (Weight.toLinear K L M))