Extensions built from 2-cocycles #
A 2-cocycle c of a Lie algebra L with values in an L-module M shears the bracket of L × M.
Mathlib's LieAlgebra.ofTwoCocycle c is this Lie algebra, and Mathlib packages it as an extension
(LieAlgebra.Extension.ofTwoCocycle) only when M is itself given the structure of an abelian Lie
algebra.
This file supplies cocycle-model constructions for arbitrary coefficient modules M,
and comparisons with extensions whose kernels are themselves abelian Lie algebras:
LieAlgebra.ofProdLinearEquiv: the identificationLieAlgebra.ofProdwithL × Mas a linear equivalence, so that finiteness transfers toLieAlgebra.ofTwoCocycle c;LieAlgebra.ofTwoCocycle.proj: the projection ontoLas a surjective Lie algebra homomorphism, whose kernel0 × Mis an abelian ideal;LieAlgebra.ofTwoCocycle.mapandLieAlgebra.ofTwoCocycle.mapEquiv: for trivial coefficients, the morphisms and isomorphisms of central extensions(x, m) ↦ (φ x, e m)induced by a mapφof the quotients and a linear mapeof the kernels carrying one cocycle to the other;LieAlgebra.ofTwoCocycle.sectionOfVanishingandLieAlgebra.ofTwoCocycle.splitEquivOfVanishing: the zero-coefficient Lie section over a subalgebra where the cocycle vanishes, and, for trivial coefficients, the direct-product splitting of its preimage;LieAlgebra.ofTwoCocycle.derivation: for trivial coefficients, the derivation(x, m) ↦ (D x, 0)induced by a derivationDof the quotient for which the cocycle is skew;LieAlgebra.ofTwoCocycle.centralElement: for coefficients the trivial moduleR, the central elementK = (0, 1), which is nonzero over a nontrivial ring, and in terms of which every element is an element ofLplus a multiple ofK(LieAlgebra.ofTwoCocycle.ofProd_eq_add_smul_centralElement);LieAlgebra.Extension.ofTwoCocycleEquiv: the comparison of an extension with abelian kernel and a linear section with the model of Mathlib's nativeExtension.twoCocycleOf.
The construction of map and mapEquiv follows Mathlib's LieAlgebra.LieEquiv.ofCoboundary,
which identifies the extensions of cohomologous cocycles by acting on the coordinates of ofProd.
Here the coordinates are instead transformed by a map of quotients and a map of kernels.
These let structure theorems about abelian ideals, such as the existence of Levi complements, be
applied to the sheared Lie algebra, for instance to show that a 2-cocycle is a coboundary. The
morphisms of central extensions compare the extensions attached to proportional cocycles, and an
extension with its restriction to a subalgebra. The degree-one counterpart, the module sheared by
a Lie derivation, is LieDerivation.ShearedModule in TauCeti.Algebra.Lie.Derivation.Cocycle.
References #
- E. Frenkel, Langlands Correspondence for Loop Groups, §1.3, for cocycle models of extensions.
def
LieAlgebra.ofProdLinearEquiv
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
The identification LieAlgebra.ofProd of L × M with the Lie algebra sheared by a 2-cocycle,
as a linear equivalence.
Instances For
@[simp]
theorem
LieAlgebra.coe_ofProdLinearEquiv
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
@[simp]
theorem
LieAlgebra.coe_ofProdLinearEquiv_symm
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
instance
LieAlgebra.instFiniteOfTwoCocycle_tauCeti
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[Module.Finite R L]
[Module.Finite R M]
:
Module.Finite R (ofTwoCocycle c)
def
LieAlgebra.ofTwoCocycle.proj
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
The projection of the Lie algebra sheared by a 2-cocycle onto L, as a Lie algebra
homomorphism.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.proj_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]
[LieRingModule L M]
[LieModule R L M]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
(x : ofTwoCocycle c)
:
theorem
LieAlgebra.ofTwoCocycle.proj_surjective
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
Function.Surjective ⇑(proj c)
theorem
LieAlgebra.ofTwoCocycle.mem_ker_proj
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
{x : ofTwoCocycle c}
:
instance
LieAlgebra.ofTwoCocycle.instIsLieAbelianSubtypeMemLieIdealKerProj
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
:
IsLieAbelian ↥(proj c).ker
The kernel 0 × M of the projection is an abelian ideal.
def
LieAlgebra.ofTwoCocycle.sectionOfVanishing
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
(S : LieSubalgebra R L)
(hc : ∀ x ∈ S, ∀ y ∈ S, (↑c x) y = 0)
:
The zero-coefficient Lie section over a subalgebra on which the cocycle vanishes. No triviality assumption on the coefficient action is needed.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.sectionOfVanishing_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]
[LieRingModule L M]
[LieModule R L M]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
(S : LieSubalgebra R L)
(hc : ∀ x ∈ S, ∀ y ∈ S, (↑c x) y = 0)
(x : ↥S)
:
The section has zero coefficient coordinate.
def
LieAlgebra.ofTwoCocycle.splitEquivOfVanishing
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
{N : Type u_4}
[LieRing N]
[LieAlgebra R N]
[IsLieAbelian N]
(S : LieSubalgebra R L)
(e : M ≃ₗ[R] N)
(hc : ∀ x ∈ S, ∀ y ∈ S, (↑c x) y = 0)
:
A central extension splits over a subalgebra where its cocycle vanishes. The coefficient
coordinate is expressed in any chosen abelian Lie algebra N linearly equivalent to M.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.coe_splitEquivOfVanishing
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
{N : Type u_4}
[LieRing N]
[LieAlgebra R N]
[IsLieAbelian N]
(S : LieSubalgebra R L)
(e : M ≃ₗ[R] N)
(hc : ∀ x ∈ S, ∀ y ∈ S, (↑c x) y = 0)
(p : ↥S × N)
:
Forward coordinates of the split preimage.
@[simp]
theorem
LieAlgebra.ofTwoCocycle.splitEquivOfVanishing_symm_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]
[LieRingModule L M]
[LieModule R L M]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
{N : Type u_4}
[LieRing N]
[LieAlgebra R N]
[IsLieAbelian N]
(S : LieSubalgebra R L)
(e : M ≃ₗ[R] N)
(hc : ∀ x ∈ S, ∀ y ∈ S, (↑c x) y = 0)
(v : ↥(LieSubalgebra.comap (proj c) S))
:
Inverse coordinates of the split preimage.
Morphisms of central extensions #
def
LieAlgebra.ofTwoCocycle.map
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
:
The morphism of central extensions (x, m) ↦ (φ x, e m) from the Lie algebra sheared by a
2-cocycle c with trivial coefficients to the one sheared by c', for a Lie algebra morphism φ
and a linear map e of coefficients such that c' (φ x) (φ y) = e (c x y).
With φ the identity this pushes an extension forward along a map of its kernels; with e the
identity it compares an extension with the pullback of another along φ.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.map_ofProd
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(x : L)
(m : M)
:
A morphism of central extensions acts by φ on the first coordinate and e on the
second.
@[simp]
theorem
LieAlgebra.ofTwoCocycle.ofProd_symm_map
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(v : ofTwoCocycle c)
:
theorem
LieAlgebra.ofTwoCocycle.proj_map
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(v : ofTwoCocycle c)
:
A morphism of central extensions lies over the morphism φ of the quotients.
@[simp]
theorem
LieAlgebra.ofTwoCocycle.map_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]
[LieRingModule L M]
[LieModule R L M]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
:
The identity morphism of a central extension.
theorem
LieAlgebra.ofTwoCocycle.map_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]
[LieRingModule L M]
[LieModule R L M]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
{L'' : Type u_6}
{M'' : Type u_7}
[LieRing L'']
[LieAlgebra R L'']
[AddCommGroup M'']
[Module R M'']
[LieRingModule L'' M'']
[LieModule R L'' M'']
[LieModule.IsTrivial L'' M'']
(φ' : L' →ₗ⁅R⁆ L'')
(e' : M' →ₗ[R] M'')
(c'' : ↥(LieModule.Cohomology.twoCocycle R L'' M''))
(h' : ∀ (x y : L'), (↑c'' (φ' x)) (φ' y) = e' ((↑c' x) y))
:
Morphisms of central extensions compose by composing the maps of quotients and kernels.
theorem
LieAlgebra.ofTwoCocycle.map_injective
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(hφ : Function.Injective ⇑φ)
(he : Function.Injective ⇑e)
:
Function.Injective ⇑(map c φ e c' h)
A morphism of central extensions is injective when the maps of quotients and kernels are.
theorem
LieAlgebra.ofTwoCocycle.map_surjective
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L →ₗ⁅R⁆ L')
(e : M →ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(hφ : Function.Surjective ⇑φ)
(he : Function.Surjective ⇑e)
:
Function.Surjective ⇑(map c φ e c' h)
A morphism of central extensions is surjective when the maps of quotients and kernels are.
def
LieAlgebra.ofTwoCocycle.mapEquiv
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L ≃ₗ⁅R⁆ L')
(e : M ≃ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
:
The isomorphism of central extensions (x, m) ↦ (φ x, e m) induced by isomorphisms φ of
the quotients and e of the kernels such that c' (φ x) (φ y) = e (c x y).
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.mapEquiv_ofProd
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L ≃ₗ⁅R⁆ L')
(e : M ≃ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(x : L)
(m : M)
:
@[simp]
theorem
LieAlgebra.ofTwoCocycle.ofProd_symm_mapEquiv
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L ≃ₗ⁅R⁆ L')
(e : M ≃ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(v : ofTwoCocycle c)
:
@[simp]
theorem
LieAlgebra.ofTwoCocycle.mapEquiv_symm_ofProd
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L ≃ₗ⁅R⁆ L')
(e : M ≃ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
(x : L')
(m : M')
:
@[simp]
theorem
LieAlgebra.ofTwoCocycle.toLieHom_mapEquiv
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L 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']
[LieModule.IsTrivial L M]
[LieModule.IsTrivial L' M']
(φ : L ≃ₗ⁅R⁆ L')
(e : M ≃ₗ[R] M')
(c' : ↥(LieModule.Cohomology.twoCocycle R L' M'))
(h : ∀ (x y : L), (↑c' (φ x)) (φ y) = e ((↑c x) y))
:
def
LieAlgebra.ofTwoCocycle.derivation
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
(D : LieDerivation R L L)
(hD : ∀ (x y : L), (↑c (D x)) y + (↑c x) (D y) = 0)
:
LieDerivation R (ofTwoCocycle c) (ofTwoCocycle c)
The derivation (x, m) ↦ (D x, 0) of the Lie algebra sheared by a 2-cocycle c with trivial
coefficients, for a derivation D of L which is skew for c:
c (D x) y + c x (D y) = 0. It kills the central kernel 0 × M.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.derivation_ofProd
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
(D : LieDerivation R L L)
(hD : ∀ (x y : L), (↑c (D x)) y + (↑c x) (D y) = 0)
(x : L)
(m : M)
:
The derivation acts by D on the first coordinate and kills the second.
@[simp]
theorem
LieAlgebra.ofTwoCocycle.ofProd_symm_derivation
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
(D : LieDerivation R L L)
(hD : ∀ (x y : L), (↑c (D x)) y + (↑c x) (D y) = 0)
(v : ofTwoCocycle c)
:
theorem
LieAlgebra.ofTwoCocycle.proj_derivation
{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]
(c : ↥(LieModule.Cohomology.twoCocycle R L M))
[LieModule.IsTrivial L M]
(D : LieDerivation R L L)
(hD : ∀ (x y : L), (↑c (D x)) y + (↑c x) (D y) = 0)
(v : ofTwoCocycle c)
:
The derivation lies over D.
@[simp]
theorem
LieAlgebra.Extension.coe_toKer
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
(m : M)
:
The kernel equivalence is the inclusion on underlying elements.
@[simp]
theorem
LieAlgebra.Extension.incl_toKer_symm
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
(v : ↥E.proj.ker)
:
Inverting the kernel equivalence recovers the underlying element by inclusion.
noncomputable def
LieAlgebra.Extension.splittingCoordinate
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
:
The kernel coordinate relative to a linear section, namely x - s (proj x).
Instances For
theorem
LieAlgebra.Extension.splittingCoordinate_apply
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
(x : E.L)
:
Evaluate the kernel coordinate by inverting the kernel equivalence on the difference from the section.
@[simp]
theorem
LieAlgebra.Extension.incl_splittingCoordinate
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
(x : E.L)
:
Including the kernel coordinate gives the difference from the section.
@[simp]
theorem
LieAlgebra.Extension.splittingCoordinate_section
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
(x : L)
:
The kernel coordinate vanishes on the section.
@[simp]
theorem
LieAlgebra.Extension.splittingCoordinate_incl
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
(m : M)
:
The kernel coordinate is a retraction of the inclusion.
theorem
LieAlgebra.Extension.incl_twoCocycleOf
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
(x y : L)
:
Including the native cocycle gives the defect of the section from preserving brackets.
theorem
LieAlgebra.Extension.incl_lie
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
[IsLieAbelian M]
(hs : Function.LeftInverse ⇑E.proj ⇑s)
(x : L)
(m : M)
:
The induced quotient action is computed by the bracket with the lift along any linear section.
noncomputable def
LieAlgebra.Extension.ofTwoCocycleEquiv
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
:
A split extension with abelian kernel is isomorphic to the model of its native cocycle.
The coordinates are s x + incl m; the section itself need not preserve brackets.
Instances For
@[simp]
theorem
LieAlgebra.Extension.ofTwoCocycleEquiv_ofProd
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
(x : L)
(m : M)
:
The comparison sends product coordinates to the section plus the inclusion.
@[simp]
theorem
LieAlgebra.Extension.ofTwoCocycleEquiv_symm_apply
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
(x : E.L)
:
(E.ofTwoCocycleEquiv hs).symm x = (ofProd (E.twoCocycleOf hs)) (E.proj x, (E.splittingCoordinate hs) x)
The inverse comparison consists of the projection and the kernel coordinate.
@[simp]
theorem
LieAlgebra.Extension.proj_ofTwoCocycleEquiv
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
(v : LieAlgebra.ofTwoCocycle (E.twoCocycleOf hs))
:
The comparison is over the identity on the quotient.
theorem
LieAlgebra.Extension.twoCocycleOf_eq_splittingCoordinate
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{M : Type u_4}
[LieRing M]
[LieAlgebra R M]
(E : Extension R M L)
{s : L →ₗ[R] E.L}
(hs : Function.LeftInverse ⇑E.proj ⇑s)
[IsLieAbelian M]
(x y : L)
:
The native cocycle is the kernel coordinate of the bracket of section elements.
The central element of an extension by R #
def
LieAlgebra.ofTwoCocycle.centralElement
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(c : ↥(LieModule.Cohomology.twoCocycle R L (TrivialLieModule R L R)))
:
The central element K = (0, 1) of the central extension of a Lie algebra by R defined by a
2-cocycle c with trivial coefficients, such as the residue cocycle of formal or of polynomial
currents.
Instances For
@[simp]
theorem
LieAlgebra.ofTwoCocycle.ofProd_symm_centralElement
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(c : ↥(LieModule.Cohomology.twoCocycle R L (TrivialLieModule R L R)))
:
The coordinates of K are (0, 1).
theorem
LieAlgebra.ofTwoCocycle.centralElement_mem_center
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(c : ↥(LieModule.Cohomology.twoCocycle R L (TrivialLieModule R L R)))
:
The element K is central.
theorem
LieAlgebra.ofTwoCocycle.centralElement_ne_zero
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(c : ↥(LieModule.Cohomology.twoCocycle R L (TrivialLieModule R L R)))
[Nontrivial R]
:
The element K is nonzero over a nontrivial ring.
theorem
LieAlgebra.ofTwoCocycle.ofProd_eq_add_smul_centralElement
{R : Type u_1}
{L : Type u_2}
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(c : ↥(LieModule.Cohomology.twoCocycle R L (TrivialLieModule R L R)))
(u : L)
(z : TrivialLieModule R L R)
:
Every element of the extension is an element of L plus a multiple of K.