Low-degree Lie algebra cohomology

This file completes the degree-zero and degree-one part of Mathlib's low-degree Chevalley--Eilenberg cochain API. It defines the differential from module elements to linear one-cochains, packages one-cocycles and one-coboundaries, and constructs first cohomology as their quotient.

The quotient interface reduces vanishing of first cohomology to the concrete statement that every one-cocycle is a principal cocycle. This is the form used by proofs of the first Whitehead lemma and by normalization arguments for Lie algebra two-cocycles.

Main definitions

• TauCeti.LieModule.Cohomology.d₀₁: the degree-zero Chevalley--Eilenberg differential.
• TauCeti.LieModule.Cohomology.oneCocycle: the kernel of Mathlib's d₁₂.
• TauCeti.LieModule.Cohomology.d₀₁Cocycle: the differential with codomain restricted to cocycles.
• TauCeti.LieModule.Cohomology.oneCoboundary: the principal one-cocycles inside the cocycles.
• TauCeti.LieModule.Cohomology.firstCohomology: first Lie algebra cohomology.
• TauCeti.LieModule.Cohomology.firstCohomologyLift: descend a linear map from cocycles to first cohomology.

References

• [N. Jacobson, Lie Algebras][jacobson1979], Chapter III, §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] : M →ₗ[R] LieModule.Cohomology.oneCochain R L M

The degree-zero Chevalley--Eilenberg differential, sending m to the principal cocycle x ↦ ⁅x, m⁆.

@[simp]

theorem TauCeti.LieModule.Cohomology.d₀₁_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] (m : M) (x : L) : ((d₀₁ R L M) m) x = ⁅x, m⁆

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] : LieModule.Cohomology.d₁₂ R L M ∘ₗ d₀₁ R L M = 0

Consecutive low-degree Chevalley--Eilenberg differentials compose to zero.

def TauCeti.LieModule.Cohomology.oneCocycle (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] : Submodule R (LieModule.Cohomology.oneCochain R L M)

Lie algebra one-cocycles: linear maps annihilated by the differential d₁₂.

theorem TauCeti.LieModule.Cohomology.mem_oneCocycle_iff (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] {f : LieModule.Cohomology.oneCochain R L M} : f ∈ oneCocycle R L M ↔ ∀ (x y : L), f ⁅x, y⁆ = ⁅x, f y⁆ - ⁅y, f x⁆

A linear map is a one-cocycle exactly when it satisfies the cocycle identity.

theorem TauCeti.LieModule.Cohomology.oneCocycle_apply_lie (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] (f : ↥(oneCocycle R L M)) (x y : L) : ↑f ⁅x, y⁆ = ⁅x, ↑f y⁆ - ⁅y, ↑f x⁆

The cocycle identity for a bundled one-cocycle.

def TauCeti.LieModule.Cohomology.d₀₁Cocycle (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] : M →ₗ[R] ↥(oneCocycle R L M)

The degree-zero differential, with codomain restricted to one-cocycles.

@[simp]

theorem TauCeti.LieModule.Cohomology.d₀₁Cocycle_coe (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] (m : M) : ↑((d₀₁Cocycle R L M) m) = (d₀₁ R L M) m

def TauCeti.LieModule.Cohomology.oneCoboundary (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] : Submodule R ↥(oneCocycle R L M)

Lie algebra one-coboundaries, regarded as a submodule of the one-cocycles.

theorem TauCeti.LieModule.Cohomology.mem_oneCoboundary_iff (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] {f : ↥(oneCocycle R L M)} : f ∈ oneCoboundary R L M ↔ ∃ (m : M), (d₀₁Cocycle R L M) m = f

A cocycle is a coboundary exactly when it is principal.

@[reducible, inline]

abbrev TauCeti.LieModule.Cohomology.firstCohomology (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] : Type (max u_2 u_3)

First Lie algebra cohomology, the quotient of one-cocycles by principal cocycles.

def TauCeti.LieModule.Cohomology.firstCohomologyMk (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] : ↥(oneCocycle R L M) →ₗ[R] firstCohomology R L M

The quotient map from one-cocycles to first cohomology.

def TauCeti.LieModule.Cohomology.firstCohomologyLift (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 : Type u_4} [AddCommGroup N] [Module R N] (f : ↥(oneCocycle R L M) →ₗ[R] N) (h : ∀ (m : M), f ((d₀₁Cocycle R L M) m) = 0) : firstCohomology R L M →ₗ[R] N

Descend a linear map on one-cocycles that vanishes on principal cocycles to first cohomology.

@[simp]

theorem TauCeti.LieModule.Cohomology.firstCohomologyLift_mk (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 : Type u_4} [AddCommGroup N] [Module R N] (f : ↥(oneCocycle R L M) →ₗ[R] N) (h : ∀ (m : M), f ((d₀₁Cocycle R L M) m) = 0) (x : ↥(oneCocycle R L M)) : (firstCohomologyLift R L M f h) ((firstCohomologyMk R L M) x) = f x

theorem TauCeti.LieModule.Cohomology.firstCohomologyLift_unique (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 : Type u_4} [AddCommGroup N] [Module R N] (f : ↥(oneCocycle R L M) →ₗ[R] N) (h : ∀ (m : M), f ((d₀₁Cocycle R L M) m) = 0) (g : firstCohomology R L M →ₗ[R] N) (hg : g ∘ₗ firstCohomologyMk R L M = f) : g = firstCohomologyLift R L M f h

A linear map from first cohomology is determined by its values on cocycle representatives.

@[simp]

theorem TauCeti.LieModule.Cohomology.firstCohomologyMk_eq_zero_iff (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] (f : ↥(oneCocycle R L M)) : (firstCohomologyMk R L M) f = 0 ↔ ∃ (m : M), (d₀₁Cocycle R L M) m = f

@[simp]

theorem TauCeti.LieModule.Cohomology.firstCohomologyMk_d₀₁Cocycle (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] (m : M) : (firstCohomologyMk R L M) ((d₀₁Cocycle R L M) m) = 0

theorem TauCeti.LieModule.Cohomology.firstCohomologyMk_eq_iff (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] (f g : ↥(oneCocycle R L M)) : (firstCohomologyMk R L M) f = (firstCohomologyMk R L M) g ↔ ∃ (m : M), (d₀₁Cocycle R L M) m = f - g

Two cocycles represent the same first cohomology class exactly when their difference is principal.

theorem TauCeti.LieModule.Cohomology.firstCohomologyMk_surjective (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] : Function.Surjective ⇑(firstCohomologyMk R L M)

Every first cohomology class has a cocycle representative.

theorem TauCeti.LieModule.Cohomology.subsingleton_firstCohomology_iff (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] : Subsingleton (firstCohomology R L M) ↔ ∀ (f : ↥(oneCocycle R L M)), ∃ (m : M), (d₀₁Cocycle R L M) m = f

First cohomology is trivial exactly when every one-cocycle is principal.