Lie algebra cohomology in low degree

This file defines low degree cochains of Lie algebras with coefficients given by a module. They are useful in the construction of central extensions, so we treat these easier cases separately from the general theory of Lie algebra cohomology.

Main definitions

• LieAlgebra.oneCochain: an abbreviation for a linear map.
• LieAlgebra.twoCochain: a submodule of bilinear maps, giving 2-cochains.
• LieAlgebra.d₁₂: The coboundary map taking 1-cochains to 2-cochains.
• LieAlgebra.d₂₃: A coboundary map taking 2-cochains to a space containing 3-cochains.
• LieAlgebra.twoCocycle: The submodule of 2-cocycles.

TODO

• coboundaries, cohomology
• comparison to the Chevalley-Eilenberg complex.
• construction and classification of central extensions

References

• H. Cartan, S. Eilenberg, Homological Algebra

@[reducible, inline]

abbrev LieModule.Cohomology.oneCochain (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] : Type (max u_2 u_3)

Lie algebra 1-cochains over L with coefficients in the module M.

def LieModule.Cohomology.twoCochain (R : Type u_1) [CommRing R] (L : Type u_2) [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] : Submodule R (L →ₗ[R] L →ₗ[R] M)

Lie algebra 2-cochains over L with coefficients in the module M.

instance LieModule.Cohomology.instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] : FunLike (↥(twoCochain R L M)) L (L →ₗ[R] M)

instance LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] : LinearMapClass (↥(twoCochain R L M)) R L (L →ₗ[R] M)

@[simp]

theorem LieModule.Cohomology.mem_twoCochain_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] {c : L →ₗ[R] L →ₗ[R] M} : c ∈ twoCochain R L M ↔ ∀ (x : L), (c x) x = 0

@[simp]

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

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

@[simp]

theorem LieModule.Cohomology.twoCochain_val_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] (a : ↥(twoCochain R L M)) (x : L) : ↑a x = a x

@[simp]

theorem LieModule.Cohomology.add_apply_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] (a b : ↥(twoCochain R L M)) (x y : L) : ((a + b) x) y = (a x) y + (b x) y

@[simp]

theorem LieModule.Cohomology.smul_apply_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] (r : R) (a : ↥(twoCochain R L M)) (x y : L) : ((r • a) x) y = r • (a x) y

def 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] : oneCochain R L M →ₗ[R] ↥(twoCochain R L M)

The coboundary operator taking degree 1 cochains to degree 2 cochains.

@[simp]

theorem LieModule.Cohomology.d₁₂_apply_coe_apply_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] (f : oneCochain R L M) (x y : L) : (↑((d₁₂ R L M) f) x) y = ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆

@[simp]

theorem LieModule.Cohomology.d₁₂_apply_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] (f : oneCochain R L M) (x y : L) : (((d₁₂ R L M) f) x) y = ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆

theorem LieModule.Cohomology.d₁₂_apply_apply_ofTrivial (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] [IsTrivial L M] (f : oneCochain R L M) (x y : L) : (((d₁₂ R L M) f) x) y = -f ⁅x, y⁆

def 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] : ↥(twoCochain R L M) →ₗ[R] L →ₗ[R] L →ₗ[R] L →ₗ[R] M

The coboundary operator taking degree 2 cochains to a space containing degree 3 cochains.

@[simp]

theorem 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] (a : ↥(twoCochain R L M)) (x y z : L) : ((((d₂₃ R L M) a) x) y) z = ⁅x, (a y) z⁆ - ⁅y, (a x) z⁆ + ⁅z, (a x) y⁆ - (a ⁅x, y⁆) z + (a ⁅x, z⁆) y - (a ⁅y, z⁆) x

theorem 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] : d₂₃ R L M ∘ₗ d₁₂ R L M = 0

def LieModule.Cohomology.twoCocycle (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 ↥(twoCochain R L M)

A Lie 2-cocycle is a 2-cochain that is annihilated by the coboundary map.

theorem LieModule.Cohomology.mem_twoCocycle_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] (a : ↥(twoCochain R L M)) : a ∈ twoCocycle R L M ↔ (d₂₃ R L M) a = 0

theorem LieModule.Cohomology.mem_twoCocycle_iff_of_trivial (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] [IsTrivial L M] (a : ↥(twoCochain R L M)) : a ∈ twoCocycle R L M ↔ ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆