Extensions of Lie algebras

This file defines extensions of Lie algebras, given by short exact sequences of Lie algebra homomorphisms. They are implemented in two ways: IsExtension is a Prop-valued class taking two homomorphisms as parameters, and Extension is a structure that includes the middle Lie algebra.

Because our sign convention for differentials is opposite that of Chevalley-Eilenberg, there is a change of signs in the "action" part of the Lie bracket.

Main definitions

• LieAlgebra.IsExtension: A Prop-valued class characterizing an extension of Lie algebras.
• LieAlgebra.Extension: A bundled structure giving an extension of Lie algebras.
• LieAlgebra.IsExtension.extension: A function that builds the bundled structure from the class.
• LieAlgebra.ofTwoCocycle: The Lie algebra built from a direct product, but whose bracket product is sheared by a 2-cocycle.
• LieAlgebra.Extension.ofTwoCocycle: The Lie algebra extension constructed from a 2-cocycle.
• LieAlgebra.Extension.ringModuleOf: Given an extension whose kernel is abelian, we obtain a Lie action of the target on the kernel.
• LieAlgebra.Extension.twoCocycle: The 2-cocycle attached to an extension with a linear section.
• LieAlgebra.Extension.oneCochainOfTwoSplitting: A 1-cochain attached to a pair of linear sections of an extension.

TODO

• IsCentral - central extensions
• Equiv - equivalence of extensions

References

• Chevalley, Eilenberg, Cohomology Theory of Lie Groups and Lie Algebras
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3

class LieAlgebra.IsExtension {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : Prop

A sequence of two Lie algebra homomorphisms is an extension if it is short exact.

• ker_eq_bot : i.ker = ⊥
• range_eq_top : p.range = ⊤
• exact : i.range = LieIdeal.toLieSubalgebra R L p.ker

theorem LieHom.range_eq_ker_iff {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : i.range = LieIdeal.toLieSubalgebra R L p.ker ↔ Function.Exact ⇑i ⇑p

def LieAlgebra.IsExtension.kerEquivRange {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) [IsExtension i p] : ↥p.ker ≃ₗ[R] ↥i.range

The equivalence from the kernel of the projection.

structure LieAlgebra.Extension (R : Type u_1) (N : Type u_2) (M : Type u_4) [CommRing R] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] : Type (max (max (max u_1 u_2) u_4) (u_5 + 1))

The type of all Lie extensions of M by N. That is, short exact sequences of R-Lie algebra homomorphisms 0 → N → L → M → 0 where R, M, and N are fixed.

• L : Type u_5

  The middle object in the sequence.

• instLieRing : LieRing self.L

  L is a Lie ring.

• instLieAlgebra : LieAlgebra R self.L

  L is a Lie algebra over R.

• incl : N →ₗ⁅R⁆ self.L

  The inclusion homomorphism N →ₗ⁅R⁆ L

• proj : self.L →ₗ⁅R⁆ M

  The projection homomorphism L →ₗ⁅R⁆ M

• IsExtension : LieAlgebra.IsExtension self.incl self.proj

@[implicit_reducible]

instance LieAlgebra.instLieRingL {R : Type u_1} {N : Type u_2} {M : Type u_4} [CommRing R] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (E : Extension R M N) : LieRing E.L

@[implicit_reducible]

instance LieAlgebra.instL {R : Type u_1} {N : Type u_2} {M : Type u_4} [CommRing R] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (E : Extension R M N) : LieAlgebra R E.L

def LieAlgebra.IsExtension.extension {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : Extension R N M

The bundled LieAlgebra.Extension corresponding to LieAlgebra.IsExtension

@[simp]

theorem LieAlgebra.IsExtension.extension_proj {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.proj = p

@[simp]

theorem LieAlgebra.IsExtension.extension_L {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.L = L

@[simp]

theorem LieAlgebra.IsExtension.extension_instLieRing {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.instLieRing = inst✝

@[simp]

theorem LieAlgebra.IsExtension.extension_incl {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.incl = i

@[simp]

theorem LieAlgebra.IsExtension.extension_instLieAlgebra {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.instLieAlgebra = inst✝

theorem LieAlgebra.isExtension_of_surjective {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) : IsExtension f.ker.incl f

A surjective Lie algebra homomorphism yields an extension.

theorem LieAlgebra.Extension.incl_apply_mem_ker {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) (x : M) : E.incl x ∈ E.proj.ker

@[simp]

theorem LieAlgebra.Extension.proj_incl {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) (x : M) : E.proj (E.incl x) = 0

theorem LieAlgebra.Extension.incl_injective {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) : Function.Injective ⇑E.incl

theorem LieAlgebra.Extension.proj_surjective {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) : Function.Surjective ⇑E.proj

structure LieAlgebra.ofTwoCocycle {R : Type u_5} {L : Type u_6} {M : Type u_7} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Type (max u_6 u_7)

A one-field structure giving a type synonym for a direct product. We use this to describe an alternative Lie algebra structure on the product, where the bracket is shifted by a 2-cocycle.

• carrier : L × M

  The underlying type.

def LieAlgebra.ofProd {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : L × M ≃ ofTwoCocycle c

An equivalence between the direct product and the corresponding one-field structure. This is used to transfer the additive and scalar-multiple structure on the direct product to the type synonym.

@[implicit_reducible]

instance LieAlgebra.instAddCommGroupOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : AddCommGroup (ofTwoCocycle c)

@[implicit_reducible]

instance LieAlgebra.instModuleOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Module R (ofTwoCocycle c)

@[simp]

theorem LieAlgebra.of_zero {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : (ofProd c) 0 = 0

@[simp]

theorem LieAlgebra.of_add {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : L × M) : (ofProd c) (x + y) = (ofProd c) x + (ofProd c) y

@[simp]

theorem LieAlgebra.of_smul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : L × M) : (ofProd c) (r • x) = r • (ofProd c) x

@[simp]

theorem LieAlgebra.of_symm_zero {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : (ofProd c).symm 0 = 0

@[simp]

theorem LieAlgebra.of_symm_add {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : ofTwoCocycle c) : (ofProd c).symm (x + y) = (ofProd c).symm x + (ofProd c).symm y

@[simp]

theorem LieAlgebra.of_symm_smul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : ofTwoCocycle c) : (ofProd c).symm (r • x) = r • (ofProd c).symm x

@[simp]

theorem LieAlgebra.of_nsmul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : L × M) : (ofProd c) (n • x) = n • (ofProd c) x

@[simp]

theorem LieAlgebra.of_symm_nsmul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : ofTwoCocycle c) : (ofProd c).symm (n • x) = n • (ofProd c).symm x

@[implicit_reducible]

instance LieAlgebra.instLieRingOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieRing (ofTwoCocycle c)

theorem LieAlgebra.bracket_ofTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {c : ↥(LieModule.Cohomology.twoCocycle R L M)} (x y : ofTwoCocycle c) : ⁅x, y⁆ = (ofProd c) (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆, (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ - ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆)

@[implicit_reducible]

instance LieAlgebra.instOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieAlgebra R (ofTwoCocycle c)

def LieAlgebra.LieEquiv.ofCoboundary {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : LieModule.Cohomology.oneCochain R L M) (h : ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x) : ofTwoCocycle c ≃ₗ⁅R⁆ ofTwoCocycle c'

An equivalence of extended Lie algebras induced by translation by a coboundary.

@[simp]

theorem LieAlgebra.LieEquiv.ofCoboundary_invFun {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : LieModule.Cohomology.oneCochain R L M) (h : ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x) (z : ofTwoCocycle c') : (ofCoboundary c c' x h).invFun z = (ofProd c) (((ofProd c').symm z).1, ((ofProd c').symm z).2 + x ((ofProd c').symm z).1)

@[simp]

theorem LieAlgebra.LieEquiv.ofCoboundary_toFun {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : LieModule.Cohomology.oneCochain R L M) (h : ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x) (y : ofTwoCocycle c) : (ofCoboundary c c' x h) y = (ofProd c') (((ofProd c).symm y).1, ((ofProd c).symm y).2 - x ((ofProd c).symm y).1)

def LieAlgebra.Extension.ofTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Extension R M L

The extension of Lie algebras defined by a 2-cocycle.

def LieAlgebra.Extension.ofAlg {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieAlgebra.ofTwoCocycle c ≃ₗ⁅R⁆ (ofTwoCocycle c).L

The Lie algebra isomorphism given by the type synonym.

theorem LieAlgebra.Extension.bracket {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : (ofTwoCocycle c).L) : ⁅x, y⁆ = (ofAlg c) ⁅(ofAlg c).symm x, (ofAlg c).symm y⁆

@[simp]

theorem LieAlgebra.Extension.ofTwoCocycle_incl_apply {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : M) : (ofTwoCocycle c).incl x = { carrier := (0, x) }

@[simp]

theorem LieAlgebra.Extension.ofTwoCocycle_proj_apply {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : (ofTwoCocycle c).L) : (ofTwoCocycle c).proj x = x.carrier.1

theorem LieAlgebra.Extension.lie_incl_mem_ker {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] {E : Extension R M L} (x : E.L) (y : M) : ⁅x, E.incl y⁆ ∈ E.proj.ker

noncomputable def LieAlgebra.Extension.toKer {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) : M ≃ₗ⁅R⁆ ↥E.proj.ker

The Lie algebra isomorphism from the kernel of an extension to the kernel of the projection.

@[simp]

theorem LieAlgebra.Extension.lie_toKer_apply {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) (x : M) (y : E.L) : ⁅y, ↑(E.toKer x)⁆ = ⁅y, E.incl x⁆

instance LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) : IsLieAbelian ↥E.proj.ker

@[implicit_reducible]

noncomputable def LieAlgebra.Extension.ringModuleOf {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) : LieRingModule L M

Given an extension of L by M whose kernel M is abelian, the kernel M gets an L-module structure. We do not make this an instance, because we may have to work with more than one extension.

@[simp]

theorem LieAlgebra.Extension.ringModuleOf_bracket {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) (x : L) (y : M) : ⁅x, y⁆ = E.toKer.symm ⁅Exists.choose ⋯ x, E.toKer y⁆

theorem LieAlgebra.Extension.ringModuleOf_bracket_proj {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) (y : M) (z : E.L) : ⁅E.proj z, y⁆ = E.toKer.symm ⁅z, E.toKer y⁆

theorem LieAlgebra.Extension.lieModuleOf {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) : LieModule R L M

Given an extension of L by M whose kernel M is abelian, the kernel M gets an R-linear L-module structure. We do not make this an instance, because we may have to work with more than one extension.

theorem LieAlgebra.Extension.toKer_bracket {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) (x : ↥E.proj.ker) (y : L) : E.toKer ⁅y, E.toKer.symm x⁆ = ⁅Exists.choose ⋯ y, x⁆

theorem LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) {s : L →ₗ[R] E.L} (hs : Function.LeftInverse ⇑E.proj ⇑s) (x : E.L) (y : ↥E.proj.ker) : ⁅s (E.proj x), y⁆ = ⁅x, y⁆

noncomputable def LieAlgebra.Extension.twoCocycleOf {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) {s : L →ₗ[R] E.L} (hs : Function.LeftInverse ⇑E.proj ⇑s) : have this := ⋯; ↥(LieModule.Cohomology.twoCocycle R L M)

The 2-cocycle attached to an extension with a linear section.

@[simp]

theorem LieAlgebra.Extension.twoCocycleOf_coe_coe {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) {s : L →ₗ[R] E.L} (hs : Function.LeftInverse ⇑E.proj ⇑s) : ↑↑(E.twoCocycleOf hs) = (LieAlgebra.Extension.twoCocycleAux✝ E hs).compr₂ ↑E.toKer.symm.toLinearEquiv

noncomputable def LieAlgebra.Extension.oneCochainOfTwoSplitting {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) {s₁ s₂ : L →ₗ[R] E.L} (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁) (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂) : LieModule.Cohomology.oneCochain R L M

The 1-cochain attached to a pair of splittings of an extension.

@[simp]

theorem LieAlgebra.Extension.oneCochainOfTwoSplitting_apply {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (E : Extension R M L) {s₁ s₂ : L →ₗ[R] E.L} (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁) (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂) (x : L) : (E.oneCochainOfTwoSplitting hs₁ hs₂) x = E.toKer.symm ⟨s₁ x - s₂ x, ⋯⟩

theorem LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] (E : Extension R M L) {s₁ s₂ : L →ₗ[R] E.L} (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁) (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂) : (LieModule.Cohomology.d₁₂ R L M) (E.oneCochainOfTwoSplitting hs₁ hs₂) = ↑(E.twoCocycleOf hs₁) - ↑(E.twoCocycleOf hs₂)