Invariant bilinear forms on Lie modules

A bilinear form Φ on a Lie module M is invariant when Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆ (LinearMap.BilinForm.lieInvariant). On a Lie algebra, a symmetric invariant form satisfies the cyclic identity Φ ⁅b, c⁆ a = Φ ⁅a, b⁆ c. This file collects the invariant symmetric forms into the submodule TauCeti.LieModule.invariantForms R L M and shows that on a finite-dimensional irreducible module over an algebraically closed field there is at most one invariant form up to scalars.

For a right-separating invariant form on a Lie algebra, the orthogonal complement of its derived ideal is its centre. This criterion needs no positivity or finite-dimensionality.

The irreducible-module uniqueness result follows from Schur's lemma. Invariance of Φ says exactly that Φ, read as a linear map M → M*, is a morphism of Lie modules (LinearMap.BilinForm.lieInvariant_iff together with LieModule.maxTrivLinearMapEquivLieModuleHom), and the morphism space between the irreducible modules M and M* is at most a line (TauCeti.LieModule.finrank_lieModuleHom_le_one, with TauCeti.LieModule.isIrreducible_dual). No nondegeneracy or symmetry of the forms is needed.

For the adjoint module of a simple Lie algebra this makes every invariant form a multiple of the Killing form; that consequence is TauCeti/Algebra/Lie/Killing/InvariantForm.lean.

Main definitions

• TauCeti.LieModule.invariantForms: the submodule of invariant symmetric bilinear forms on a Lie module.

Main results

• LinearMap.BilinForm.orthogonal_derivedSeries_one_eq_center: for a right-separating invariant form, the orthogonal complement of the derived ideal is the centre.
• LinearMap.BilinForm.lieInvariant.compl₁₂: pullback along a Lie homomorphism preserves invariance.
• LinearMap.BilinForm.lieInvariant.apply_lie_cyclic: a symmetric invariant form satisfies Φ ⁅b, c⁆ a = Φ ⁅a, b⁆ c.
• TauCeti.LieModule.traceForm_mem_invariantForms: the trace form of a Lie module, in particular the Killing form, is an invariant symmetric form on the Lie algebra.
• TauCeti.LieModule.invariantForms_le_maxTrivSubmodule: invariant symmetric forms lie in the maximal trivial submodule of the space of bilinear forms.
• TauCeti.LieModule.finrank_maxTrivSubmodule_bilinForm_le_one: the invariant bilinear forms on a finite-dimensional irreducible module over an algebraically closed field form a space of dimension at most one.
• TauCeti.LieModule.finrank_invariantForms_le_one: so do the invariant symmetric forms.
• TauCeti.LieModule.exists_eq_smul_of_lieInvariant: on such a module, every invariant form is a scalar multiple of any nonzero invariant form.
• TauCeti.LieModule.invariantForms_eq_span_singleton: the invariant symmetric forms are the line spanned by any nonzero one.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §6.1 for Schur's lemma.
• J. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups, Springer (2012), Lemma 12.1.2, for the centre/derived orthogonality criterion.

theorem LinearMap.BilinForm.lieInvariant.compl₁₂ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {B : LinearMap.BilinForm R L} (hB : lieInvariant L B) (f : L' →ₗ⁅R⁆ L) : lieInvariant L' (LinearMap.compl₁₂ B ↑f ↑f)

Pullback along a Lie homomorphism preserves invariance of a bilinear form.

The cyclic identity

theorem LinearMap.BilinForm.lieInvariant.apply_lie_cyclic {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [Module R L] {Φ : LinearMap.BilinForm R L} (hΦ : lieInvariant L Φ) (hΦs : Φ.IsSymm) (a b c : L) : (Φ ⁅b, c⁆) a = (Φ ⁅a, b⁆) c

A symmetric invariant form on a Lie algebra is invariant under cyclic permutation of a bracket and a third argument: Φ ⁅b, c⁆ a = Φ ⁅a, b⁆ c.

theorem LinearMap.BilinForm.orthogonal_derivedSeries_one_eq_center {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] (B : LinearMap.BilinForm K L) (hB : SeparatingRight B) (hinv : lieInvariant L B) : LieAlgebra.InvariantForm.orthogonal B hinv (LieAlgebra.derivedSeries K L 1) = LieAlgebra.center K L

The orthogonal complement of the derived ideal for a right-separating invariant form is the centre.

The submodule of invariant symmetric forms

def TauCeti.LieModule.invariantForms (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Submodule R (LinearMap.BilinForm R M)

The invariant symmetric bilinear forms on a Lie module M: the forms Φ with Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆ and Φ y z = Φ z y.

@[simp]

theorem TauCeti.LieModule.mem_invariantForms_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {Φ : LinearMap.BilinForm R M} : Φ ∈ invariantForms R L M ↔ LinearMap.BilinForm.lieInvariant L Φ ∧ Φ.IsSymm

theorem TauCeti.LieModule.traceForm_mem_invariantForms (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] : LieModule.traceForm R L M ∈ invariantForms R L L

The trace form of a Lie module M is an invariant symmetric form on the Lie algebra L. For M = L this is the Killing form killingForm R L.

theorem TauCeti.LieModule.invariantForms_le_maxTrivSubmodule (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] : invariantForms R L M ≤ ↑(LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M))

Invariant symmetric forms lie in the maximal trivial submodule of the space of bilinear forms, which consists of the invariant forms by LinearMap.BilinForm.lieInvariant_iff.

Invariant forms on an irreducible module

theorem TauCeti.LieModule.finrank_maxTrivSubmodule_bilinForm_le_one (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : Module.finrank K ↥(LieModule.maxTrivSubmodule K L (LinearMap.BilinForm K M)) ≤ 1

The invariant bilinear forms on a finite-dimensional irreducible Lie module over an algebraically closed field form a space of dimension at most one. Here the invariant forms are described as the maximal trivial submodule of the space of bilinear forms, as in LinearMap.BilinForm.lieInvariant_iff.

theorem TauCeti.LieModule.exists_eq_smul_of_lieInvariant {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] {Φ Ψ : LinearMap.BilinForm K M} (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΨ : LinearMap.BilinForm.lieInvariant L Ψ) (hΨ0 : Ψ ≠ 0) : ∃ (c : K), Φ = c • Ψ

Invariant bilinear forms on a finite-dimensional irreducible Lie module over an algebraically closed field are proportional: every invariant form is a scalar multiple of any nonzero one.

theorem TauCeti.LieModule.finrank_invariantForms_le_one (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] : Module.finrank K ↥(invariantForms K L M) ≤ 1

The invariant symmetric bilinear forms on a finite-dimensional irreducible Lie module over an algebraically closed field form a space of dimension at most one.

theorem TauCeti.LieModule.invariantForms_eq_span_singleton {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [LieModule.IsIrreducible K L M] {Ψ : LinearMap.BilinForm K M} (hΨ : Ψ ∈ invariantForms K L M) (hΨ0 : Ψ ≠ 0) : invariantForms K L M = K ∙ Ψ

On a finite-dimensional irreducible Lie module over an algebraically closed field, the invariant symmetric bilinear forms are the line spanned by any nonzero one.