Whitehead's lemmas

Let L be a Lie algebra with nondegenerate Killing form over a field K of characteristic zero (such an L is automatically finite-dimensional, TauCeti.finite_of_isKilling), and M a finite-dimensional L-module. Whitehead's first and second lemmas say that the Lie algebra cohomology groups H¹(L, M) and H²(L, M) vanish. In terms of Mathlib's low-degree cochains (LieModule.Cohomology.d₁₂, LieModule.Cohomology.twoCocycle):

• every 1-cochain f with d₁₂ f = 0 is x ↦ ⁅x, m⁆ for some m : M; equivalently every Lie derivation L → M is inner;
• every 2-cocycle is the coboundary d₁₂ f of a 1-cochain f.

These are the vanishing theorems used to normalise Lie algebra cocycles against a semisimple subalgebra, as in the classification of the continuous central extensions of a loop algebra.

The arguments

First lemma. A Lie derivation D : L → M shears the action of L on M × K (LieDerivation.ShearedModule D): ⁅x, (m, c)⁆ = (⁅x, m⁆ + c • D x, 0). This is a Lie module precisely because D satisfies the Leibniz rule, and L carries it into the proper Lie submodule M × 0. By Weyl's theorem (TauCeti.exists_invariant_notMem_of_isKilling) there is an invariant vector (m, c) with c ≠ 0, and then D x = ⁅x, -c⁻¹ • m⁆.

Second lemma. A 2-cocycle c defines Mathlib's extension LieAlgebra.ofTwoCocycle c of L by M, in which M is an abelian ideal with quotient L. By the abelian case of Levi's theorem (LieIdeal.exists_lieSubalgebra_isCompl_of_isLieAbelian) this ideal has a complementary Lie subalgebra, which the projection identifies with L. The inverse identification is a Lie algebra section x ↦ (x, g x), and the section being a Lie homomorphism says exactly c = d₁₂ (-g).

Main results

• LieDerivation.IsKilling.exists_eq_inner: every Lie derivation into a finite-dimensional module is inner (Whitehead's first lemma).
• LieModule.Cohomology.exists_eq_lie_of_d₁₂_eq_zero: the cochain form of the first lemma.
• LieModule.Cohomology.exists_d₁₂_eq: every 2-cocycle is a coboundary (Whitehead's second lemma).
• LieModule.Cohomology.twoCocycle_eq_range_d₁₂: the 2-cocycles are exactly the coboundaries.

References

• N. Jacobson, Lie Algebras, Chapter III, for Whitehead's lemmas and their relation to the theorems of Weyl and Levi.
• C. A. Weibel, An Introduction to Homological Algebra, §7.8.

theorem LieDerivation.IsKilling.exists_eq_inner {K : Type u} {L : Type v} {M : Type w} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (D : LieDerivation K L M) : ∃ (m : M), (inner K L M) m = D

Whitehead's first lemma. Over a field of characteristic zero, every Lie derivation from a Lie algebra with nondegenerate Killing form (necessarily finite-dimensional) into a finite-dimensional module is inner: it is x ↦ ⁅x, m⁆ for some m.

theorem LieModule.Cohomology.exists_eq_lie_of_d₁₂_eq_zero {K : Type u} {L : Type v} {M : Type w} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] {f : oneCochain K L M} (hf : (d₁₂ K L M) f = 0) : ∃ (m : M), ∀ (x : L), f x = ⁅x, m⁆

Whitehead's first lemma for cochains: over a field of characteristic zero, a 1-cocycle of a Lie algebra with nondegenerate Killing form (necessarily finite-dimensional) with values in a finite-dimensional module is a coboundary, f x = ⁅x, m⁆.

theorem LieModule.Cohomology.exists_d₁₂_eq {K : Type u} {L : Type v} {M : Type w} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] (c : ↥(twoCocycle K L M)) : ∃ (f : oneCochain K L M), (d₁₂ K L M) f = ↑c

Whitehead's second lemma. Over a field of characteristic zero, every 2-cocycle of a Lie algebra with nondegenerate Killing form with values in a finite-dimensional module is a coboundary.

theorem LieModule.Cohomology.twoCocycle_eq_range_d₁₂ {K : Type u} {L : Type v} {M : Type w} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] : twoCocycle K L M = (d₁₂ K L M).range

Whitehead's second lemma, as an equality of submodules: the 2-cocycles of a Lie algebra with nondegenerate Killing form in characteristic zero, with values in a finite-dimensional module, are exactly the coboundaries.