Low-degree Lie algebra cochains

Complements to Mathlib's low-degree cochain complex LieModule.Cohomology of a Lie algebra L with values in an L-module M.

• LieModule.Cohomology.range_d₁₂_le_twoCocycle: every coboundary is a 2-cocycle.
• LieModule.Cohomology.d₁₂_comp_lieHom_apply_apply_ofTrivial: with trivial coefficients, d₁₂ commutes with pulling back along a Lie algebra morphism and pushing forward along a linear map.
• LieModule.Cohomology.twoCochainMap: pulling 2-cochains back along a Lie algebra morphism and pushing them forward along a linear map; with trivial coefficients it preserves 2-cocycles (LieModule.Cohomology.twoCochainMap_mem_twoCocycle).
• An additive group structure on every submodule of 2-cochains, such as the 2-cocycles, so that quotients of such submodules can be formed.
• LieModule.Cohomology.sub_apply_apply: the values of a difference of 2-cochains.
• LieModule.Cohomology.exists_d₁₂_eq_of_forall_dual: on a perfect Lie algebra, a 2-cochain with trivial projective coefficients is a coboundary once its image under every linear functional is one.

@[instance_reducible]

instance LieModule.Cohomology.instAddCommGroupSubmoduleTwoCochain {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] (S : Submodule R ↥(twoCochain R L M)) : AddCommGroup ↥S

Submodules of 2-cochains are additive groups. Instance search does not find Submodule.addCommGroup here on its own: it cannot recover the ambient module twoCochain R L M by unification, so it is named explicitly.

@[simp]

theorem LieModule.Cohomology.sub_apply_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] (a b : ↥(twoCochain R L M)) (x y : L) : ((a - b) x) y = (a x) y - (b x) y

def LieModule.Cohomology.twoCochainMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] (e : M →ₗ[R] M') (φ : L' →ₗ⁅R⁆ L) : ↥(twoCochain R L M) →ₗ[R] ↥(twoCochain R L' M')

Pull a 2-cochain back along a Lie algebra morphism φ and push it forward along a linear map e of coefficients: (x, y) ↦ e (c (φ x) (φ y)).

@[simp]

theorem LieModule.Cohomology.twoCochainMap_apply_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] (e : M →ₗ[R] M') (φ : L' →ₗ⁅R⁆ L) (c : ↥(twoCochain R L M)) (x y : L') : (((twoCochainMap e φ) c) x) y = e ((c (φ x)) (φ y))

@[simp]

theorem LieModule.Cohomology.twoCochainMap_id {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] : twoCochainMap LinearMap.id LieHom.id = LinearMap.id

Pullback and coefficient pushforward by identity maps leave two-cochains unchanged.

theorem LieModule.Cohomology.twoCochainMap_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] {L'' : Type u_6} {M'' : Type u_7} [LieRing L''] [LieAlgebra R L''] [AddCommGroup M''] [Module R M''] (e : M →ₗ[R] M') (e' : M' →ₗ[R] M'') (φ : L' →ₗ⁅R⁆ L) (ψ : L'' →ₗ⁅R⁆ L') : twoCochainMap e' ψ ∘ₗ twoCochainMap e φ = twoCochainMap (e' ∘ₗ e) (φ.comp ψ)

Coefficient pushforward composes covariantly and Lie algebra pullback contravariantly.

theorem LieModule.Cohomology.range_d₁₂_le_twoCocycle {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : (d₁₂ R L M).range ≤ twoCocycle R L M

Every coboundary is a 2-cocycle.

theorem LieModule.Cohomology.d₁₂_comp_lieHom_apply_apply_ofTrivial {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] [LieRingModule L M] [LieModule R L M] [LieRingModule L' M'] [LieModule R L' M'] [IsTrivial L M] [IsTrivial L' M'] (e : M →ₗ[R] M') (φ : L' →ₗ⁅R⁆ L) (f : oneCochain R L M) (x y : L') : (((d₁₂ R L' M') (e ∘ₗ f ∘ₗ ↑φ)) x) y = e ((((d₁₂ R L M) f) (φ x)) (φ y))

With trivial coefficients, the differential d₁₂ commutes with pulling one-cochains back along a Lie algebra morphism φ and pushing them forward along a linear map e of coefficients.

theorem LieModule.Cohomology.twoCochainMap_d₁₂ {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] [LieRingModule L M] [LieModule R L M] [LieRingModule L' M'] [LieModule R L' M'] [IsTrivial L M] [IsTrivial L' M'] (e : M →ₗ[R] M') (φ : L' →ₗ⁅R⁆ L) (f : oneCochain R L M) : (twoCochainMap e φ) ((d₁₂ R L M) f) = (d₁₂ R L' M') (e ∘ₗ f ∘ₗ ↑φ)

With trivial coefficients, pullback and coefficient pushforward commute with d₁₂.

theorem LieModule.Cohomology.twoCochainMap_mem_twoCocycle {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] {L' : Type u_4} {M' : Type u_5} [LieRing L'] [LieAlgebra R L'] [AddCommGroup M'] [Module R M'] [LieRingModule L M] [LieModule R L M] [LieRingModule L' M'] [LieModule R L' M'] [IsTrivial L M] [IsTrivial L' M'] (e : M →ₗ[R] M') (φ : L' →ₗ⁅R⁆ L) {c : ↥(twoCochain R L M)} (hc : c ∈ twoCocycle R L M) : (twoCochainMap e φ) c ∈ twoCocycle R L' M'

With trivial coefficients, pulling back along a Lie algebra morphism and pushing forward along a linear map sends 2-cocycles to 2-cocycles.

theorem LieModule.Cohomology.exists_d₁₂_eq_of_forall_dual {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [IsTrivial L M] [Module.Projective R M] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) (c : ↥(twoCochain R L M)) (hc : ∀ (φ : Module.Dual R M), ∃ (g : Module.Dual R L), ∀ (x y : L), φ ((c x) y) = -g ⁅x, y⁆) : ∃ (f : oneCochain R L M), (d₁₂ R L M) f = c

On a perfect Lie algebra, coboundaries are detected by functionals. Let L be a perfect Lie algebra and M a projective module with trivial action, for instance a vector space. A 2-cochain c with values in M is a coboundary as soon as, for every linear functional φ on M, the scalar cochain φ ∘ c is the coboundary (x, y) ↦ -g ⁅x, y⁆ of some linear form g on L. The coefficients may be infinitely generated: since L is perfect, c descends along the bracket L ⊗ L → L, because functionals separate the points of M.