The Chevalley–Eilenberg complex of a Lie algebra

Let L be a Lie algebra over a commutative ring R and M an L-module. The Chevalley–Eilenberg cochains of degree n are the alternating maps L [⋀^Fin n]→ₗ[R] M, and the differential d R L M n sends an n-cochain ω to the (n + 1)-cochain (d ω)(x₀, …, xₙ) = ∑ i, (-1)^i ⁅xᵢ, ω(x₀, …, x̂ᵢ, …, xₙ)⁆ + ∑_{i < j} (-1)^(i + j) ω(⁅xᵢ, xⱼ⁆, x₀, …, x̂ᵢ, …, x̂ⱼ, …, xₙ) (d_zero_apply, d_succ_apply). This file constructs the differential in every degree and proves d ∘ d = 0 (d_d).

The differential is constructed one degree at a time from the interior products ω.curryLeft x and the Lie derivatives ⁅x, ω⁆ of AlternatingMap.instLieRingModule, through Cartan's formula ι_x d ω = ⁅x, ω⁆ - d ι_x ω (curryLeft_d_zero, curryLeft_d_succ). This formula, together with [L_x, ι_y] = ι_{[x, y]}, shows that the differential commutes with the Lie derivatives (lie_d), and then that it squares to zero, both by induction on the degree. The explicit formula is then deduced from Cartan's formula.

The differentials assemble into a cochain complex of R-modules, whose cohomology is the Lie algebra cohomology of L with coefficients in M in every degree. In degrees one and two, the cochains are identified with Mathlib's low-degree cochains oneCochain and twoCochain, and the differential with d₀₁, Mathlib's d₁₂ and, after forgetting alternation, d₂₃.

Main definitions

• TauCeti.LieModule.Cohomology.d: the Chevalley–Eilenberg differential in degree n.
• TauCeti.LieModule.Cohomology.cochainComplex: the Chevalley–Eilenberg cochain complex.
• TauCeti.LieModule.Cohomology.cohomology: Lie algebra cohomology in degree n.
• TauCeti.LieModule.Cohomology.oneCochainEquiv, TauCeti.LieModule.Cohomology.twoCochainEquiv: the comparison with the low-degree cochains.

Main results

• TauCeti.LieModule.Cohomology.d_succ_apply: the explicit formula for the differential.
• TauCeti.LieModule.Cohomology.curryLeft_d_succ: Cartan's formula.
• TauCeti.LieModule.Cohomology.lie_d: the differential is a map of L-modules.
• TauCeti.LieModule.Cohomology.d_d: the differential squares to zero.
• TauCeti.LieModule.Cohomology.twoCochainEquiv_d_one, TauCeti.LieModule.Cohomology.d₂₃_twoCochainEquiv: the comparison with d₁₂ and d₂₃.

References

• C. Chevalley and S. Eilenberg, Cohomology theory of Lie groups and Lie algebras, Trans. Amer. Math. Soc. 63 (1948), 85–124.
• C. A. Weibel, An Introduction to Homological Algebra, Cambridge University Press, 1994, §7.7.

def TauCeti.LieModule.Cohomology.d (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : L [⋀^Fin n]→ₗ[R] M →ₗ[R] L [⋀^Fin (n + 1)]→ₗ[R] M

The Chevalley–Eilenberg differential from n-cochains to (n + 1)-cochains of L with coefficients in M.

@[simp]

theorem TauCeti.LieModule.Cohomology.curryLeft_d_zero {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (ω : L [⋀^Fin 0]→ₗ[R] M) (x : L) : ((d R L M 0) ω).curryLeft x = ⁅x, ω⁆

Cartan's formula in degree zero: the interior product of d ω is the Lie derivative.

@[simp]

theorem TauCeti.LieModule.Cohomology.curryLeft_d_succ {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {n : ℕ} (ω : L [⋀^Fin (n + 1)]→ₗ[R] M) (x : L) : ((d R L M (n + 1)) ω).curryLeft x = ⁅x, ω⁆ - (d R L M n) (ω.curryLeft x)

Cartan's formula ι_x d ω = L_x ω - d ι_x ω.

@[simp]

theorem TauCeti.LieModule.Cohomology.d_zero_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (ω : L [⋀^Fin 0]→ₗ[R] M) (v : Fin 1 → L) : ((d R L M 0) ω) v = ⁅v 0, ω ![]⁆

The differential of a 0-cochain, that is of an element ω ![] of M.

@[simp]

theorem TauCeti.LieModule.Cohomology.lie_d {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) (x : L) (ω : L [⋀^Fin n]→ₗ[R] M) : ⁅x, (d R L M n) ω⁆ = (d R L M n) ⁅x, ω⁆

The differential commutes with the action of L: it is a map of L-modules.

@[simp]

theorem TauCeti.LieModule.Cohomology.d_d {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) (ω : L [⋀^Fin n]→ₗ[R] M) : (d R L M (n + 1)) ((d R L M n) ω) = 0

The Chevalley–Eilenberg differential squares to zero.

theorem TauCeti.LieModule.Cohomology.d_comp_d {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : d R L M (n + 1) ∘ₗ d R L M n = 0

The Chevalley–Eilenberg differential squares to zero, as a composite of linear maps.

The explicit formula

theorem TauCeti.LieModule.Cohomology.d_succ_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {n : ℕ} (ω : L [⋀^Fin (n + 1)]→ₗ[R] M) (v : Fin (n + 2) → L) : ((d R L M (n + 1)) ω) v = ∑ i : Fin (n + 2), (-1) ^ ↑i • ⁅v i, ω (i.removeNth v)⁆ + ∑ i : Fin (n + 1), ∑ j ≥ i, (-1) ^ (↑i + ↑j + 1) • ω (Matrix.vecCons ⁅v i.castSucc, v j.succ⁆ (j.removeNth (i.castSucc.removeNth v)))

The Chevalley–Eilenberg formula for the differential of a cochain of positive degree: (d ω)(x₀, …, xₙ₊₁) = ∑ i, (-1)^i ⁅xᵢ, ω(…, x̂ᵢ, …)⁆ + ∑_{i < j} (-1)^(i + j) ω(⁅xᵢ, xⱼ⁆, …), where the pairs i < j are written as (i.castSucc, j.succ) with i ≤ j.

The complex and its cohomology

noncomputable def TauCeti.LieModule.Cohomology.cochainComplex (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : CochainComplex (ModuleCat R) ℕ

The Chevalley–Eilenberg cochain complex of L with coefficients in M, whose degree n term is the module of alternating maps L [⋀^Fin n]→ₗ[R] M.

@[simp]

theorem TauCeti.LieModule.Cohomology.cochainComplex_X (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : (cochainComplex R L M).X n = ↧(L [⋀^Fin n]→ₗ[R] M)

The degree n term of the Chevalley–Eilenberg complex is the module of n-cochains.

@[simp]

theorem TauCeti.LieModule.Cohomology.cochainComplex_d_succ (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : (cochainComplex R L M).d n (n + 1) = ModuleCat.ofHom (d R L M n)

The differential of the Chevalley–Eilenberg complex from degree n to degree n + 1.

@[reducible, inline]

noncomputable abbrev TauCeti.LieModule.Cohomology.cohomology (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (n : ℕ) : ModuleCat R

The n-th Lie algebra cohomology of L with coefficients in M, the homology of the Chevalley–Eilenberg complex in degree n.

Comparison with the low-degree cochains

def TauCeti.LieModule.Cohomology.oneCochainEquiv (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] : L [⋀^Fin 1]→ₗ[R] M ≃ₗ[R] LieModule.Cohomology.oneCochain R L M

One-cochains are linear maps.

@[simp]

theorem TauCeti.LieModule.Cohomology.oneCochainEquiv_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] (ω : L [⋀^Fin 1]→ₗ[R] M) (x : L) : ((oneCochainEquiv R L M) ω) x = ω ![x]

The linear map attached to a one-cochain is its value on one-element tuples.

@[simp]

theorem TauCeti.LieModule.Cohomology.oneCochainEquiv_symm_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] (f : LieModule.Cohomology.oneCochain R L M) (v : Fin 1 → L) : ((oneCochainEquiv R L M).symm f) v = f (v 0)

The one-cochain attached to a linear map evaluates it on the unique entry.

def TauCeti.LieModule.Cohomology.twoCochainEquiv (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] : L [⋀^Fin 2]→ₗ[R] M ≃ₗ[R] ↥(LieModule.Cohomology.twoCochain R L M)

Two-cochains are alternating bilinear maps.

@[simp]

theorem TauCeti.LieModule.Cohomology.twoCochainEquiv_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] (ω : L [⋀^Fin 2]→ₗ[R] M) (x y : L) : (((twoCochainEquiv R L M) ω) x) y = ω ![x, y]

The bilinear map attached to a two-cochain is its value on pairs.

@[simp]

theorem TauCeti.LieModule.Cohomology.twoCochainEquiv_symm_apply {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] (c : ↥(LieModule.Cohomology.twoCochain R L M)) (v : Fin 2 → L) : ((twoCochainEquiv R L M).symm c) v = (c (v 0)) (v 1)

The two-cochain attached to an alternating bilinear map evaluates it on the two entries.

theorem TauCeti.LieModule.Cohomology.oneCochainEquiv_d_zero {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (ω : L [⋀^Fin 0]→ₗ[R] M) : (oneCochainEquiv R L M) ((d R L M 0) ω) = (d₀₁ R L M) (ω ![])

In degree zero, the differential is the differential d₀₁ from the module to one-cochains.

theorem TauCeti.LieModule.Cohomology.twoCochainEquiv_d_one {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (ω : L [⋀^Fin 1]→ₗ[R] M) : (twoCochainEquiv R L M) ((d R L M 1) ω) = (LieModule.Cohomology.d₁₂ R L M) ((oneCochainEquiv R L M) ω)

In degree one, the differential is Mathlib's d₁₂.

theorem TauCeti.LieModule.Cohomology.d₂₃_twoCochainEquiv {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (ω : L [⋀^Fin 2]→ₗ[R] M) (x y z : L) : ((((LieModule.Cohomology.d₂₃ R L M) ((twoCochainEquiv R L M) ω)) x) y) z = ((d R L M 2) ω) ![x, y, z]

In degree two, the differential is Mathlib's d₂₃, which takes values in all trilinear maps.