Perfectness of residue central extensions

Over a field, the residue central extension of the formal current algebra of a perfect Lie algebra is perfect exactly when the invariant symmetric form is nonzero. This is the perfectness condition needed for the universal central extension of a loop algebra.

We use Mathlib's LieAlgebra.ofTwoCocycle directly. The form Φ has Mathlib's residue convention Res(f dg) Φ(x, y); the affine convention with level form κ uses Φ = -κ. No degree derivation is adjoined. Perfectness is expressed by derivedSeries R L 1 = ⊤.

The derived-algebra membership lemmas can also be used over commutative rings to study the current summand and central form values separately, including the split extension at zero level.

References

• V. Kac, Infinite-Dimensional Lie Algebras, Chapter 7 (central extensions of loop algebras).

theorem TauCeti.CurrentAlgebra.ofProd_form_mem_derivedSeries (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) (x y : L) : (LieAlgebra.ofProd (twoCocycleOfBilinear R L Φ hΦ hΦs)) (0, (TrivialLieModule.equiv R (currentAlgebra R L) R).symm ((Φ x) y)) ∈ LieAlgebra.derivedSeries R (LieAlgebra.ofTwoCocycle (twoCocycleOfBilinear R L Φ hΦ hΦs)) 1

Values of the form occur as central elements in the derived algebra.

theorem TauCeti.CurrentAlgebra.ofProd_current_mem_derivedSeries (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) (hperfect : LieAlgebra.derivedSeries R L 1 = ⊤) (u : currentAlgebra R L) : (LieAlgebra.ofProd (twoCocycleOfBilinear R L Φ hΦ hΦs)) (u, 0) ∈ LieAlgebra.derivedSeries R (LieAlgebra.ofTwoCocycle (twoCocycleOfBilinear R L Φ hΦ hΦs)) 1

When L is perfect, the entire current summand lies in the derived algebra of its residue central extension, including at zero level.

theorem TauCeti.CurrentAlgebra.central_eq_zero_of_mem_derivedSeries (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) (hzero : Φ = 0) {v : LieAlgebra.ofTwoCocycle (twoCocycleOfBilinear R L Φ hΦ hΦs)} (hv : v ∈ LieAlgebra.derivedSeries R (LieAlgebra.ofTwoCocycle (twoCocycleOfBilinear R L Φ hΦ hΦs)) 1) : ((LieAlgebra.ofProd (twoCocycleOfBilinear R L Φ hΦ hΦs)).symm v).2 = 0

At zero level every element of the derived algebra has zero central coordinate.

theorem TauCeti.CurrentAlgebra.derivedSeries_ofTwoCocycle_eq_top_iff (L : Type u_2) [LieRing L] {K : Type u_3} [Field K] [LieAlgebra K L] (Ψ : LinearMap.BilinForm K L) (hΨ : LinearMap.BilinForm.lieInvariant L Ψ) (hΨs : Ψ.IsSymm) (hperfect : LieAlgebra.derivedSeries K L 1 = ⊤) : LieAlgebra.derivedSeries K (LieAlgebra.ofTwoCocycle (twoCocycleOfBilinear K L Ψ hΨ hΨs)) 1 = ⊤ ↔ Ψ ≠ 0

The residue central extension of a perfect Lie algebra over a field is perfect if and only if its form is nonzero. No finite-dimensionality or characteristic assumption is needed.