Invariant forms classify the continuous second cohomology of formal currents

The residue class [c_Φ] of an invariant symmetric form Φ on a Lie algebra L is the class of the residue cocycle (f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y) in the continuous second cohomology of the formal currents R⸨X⸩ ⊗[R] L with trivial coefficients. Since [c_Φ] depends linearly on Φ, this file packages it as a linear map TauCeti.CurrentAlgebra.invariantFormsResidueClass on the submodule TauCeti.LieModule.invariantForms R L L of invariant symmetric forms.

Over every commutative ring this map is injective for every Lie algebra L: a continuous cohomology class determines the form whose residue cocycle represents it. When L is finite-dimensional with nondegenerate Killing form over a field of characteristic zero, that is, when L is semisimple, the map is also surjective. So for every semisimple Lie algebra, including a finite product of simple ones (LieAlgebra.IsKilling.instProd), Φ ↦ [c_Φ] is a linear equivalence from the invariant symmetric forms on L onto the continuous second cohomology of its formal loop algebra (TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv). No algebraic closedness and no simplicity is needed.

The residue cocycle uses Mathlib's sign convention Res(f dg) Φ(x, y). The affine cocycle c_κ = -κ(x, y) Res(f dg) of a level form κ is the residue cocycle of Φ = -κ, so the map κ ↦ [c_κ] of the affine convention is the residue class map precomposed with negation of forms.

Main definitions

• TauCeti.CurrentAlgebra.invariantFormsResidueClass: the linear map Φ ↦ [c_Φ].
• TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv: for a semisimple Lie algebra, the linear equivalence from invariant symmetric forms onto continuous second cohomology.

Main results

• TauCeti.CurrentAlgebra.invariantFormsResidueClass_injective: distinct invariant symmetric forms have distinct residue classes.
• TauCeti.CurrentAlgebra.invariantFormsResidueClass_surjective: every continuous class is the residue class of an invariant symmetric form.
• TauCeti.CurrentAlgebra.exists_eq_smul_residueClass: the residue class of a spanning form spans continuous second cohomology.

References

• E. Frenkel, Langlands Correspondence for Loop Groups, §1.3, for the classification of central extensions of the formal loop algebra by its continuous second cohomology.
• V. G. Kac, Infinite-Dimensional Lie Algebras, 3rd ed., Chapter 7, for the affine central extension attached to an invariant form.

noncomputable def TauCeti.CurrentAlgebra.invariantFormsResidueClass (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : ↥(LieModule.invariantForms R L L) →ₗ[R] LieModule.Cohomology.continuousSecondCohomology R (currentAlgebra R L) (TrivialLieModule R (currentAlgebra R L) R)

The residue class map. The linear map Φ ↦ [c_Φ] from the invariant symmetric forms on L to the continuous second cohomology of formal currents with trivial coefficients, where c_Φ is the residue cocycle (f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y).

@[simp]

theorem TauCeti.CurrentAlgebra.invariantFormsResidueClass_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : ↥(LieModule.invariantForms R L L)) : (invariantFormsResidueClass R L) Φ = residueClass R L ↑Φ ⋯ ⋯

theorem TauCeti.CurrentAlgebra.invariantFormsResidueClass_injective {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective ⇑(invariantFormsResidueClass R L)

The residue class map on invariant symmetric forms is injective, over every commutative ring.

theorem TauCeti.CurrentAlgebra.invariantFormsResidueClass_surjective {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : Function.Surjective ⇑(invariantFormsResidueClass K L)

Every continuous class is a residue class. Let L be a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, for instance a semisimple Lie algebra. Then every class in the continuous second cohomology of formal currents with trivial coefficients is the residue class of an invariant symmetric form.

theorem TauCeti.CurrentAlgebra.exists_eq_smul_residueClass {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {Ψ : LinearMap.BilinForm K L} (hΨ : LinearMap.BilinForm.lieInvariant L Ψ) (hΨs : Ψ.IsSymm) (hspan : ∀ (Φ : LinearMap.BilinForm K L), LinearMap.BilinForm.lieInvariant L Φ → ∃ (t : K), Φ = t • Ψ) (a : LieModule.Cohomology.continuousSecondCohomology K (currentAlgebra K L) (TrivialLieModule K (currentAlgebra K L) K)) : ∃ (t : K), a = t • residueClass K L Ψ hΨ hΨs

The continuous second cohomology of formal currents is spanned by the residue class. Under the hypotheses of invariantFormsResidueClass_surjective, let Ψ be an invariant symmetric form on L spanning the invariant forms. Then every class in the continuous second cohomology of formal currents with trivial coefficients is a multiple of the residue class of Ψ.

noncomputable def TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv (K : Type u_1) (L : Type u_2) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : ↥(LieModule.invariantForms K L L) ≃ₗ[K] LieModule.Cohomology.continuousSecondCohomology K (currentAlgebra K L) (TrivialLieModule K (currentAlgebra K L) K)

Invariant forms classify the continuous second cohomology of formal loops. For a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, for instance a semisimple Lie algebra, Φ ↦ [c_Φ] is a linear equivalence from the invariant symmetric forms on L onto the continuous second cohomology of formal currents with trivial coefficients.

@[simp]

theorem TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (Φ : ↥(LieModule.invariantForms K L L)) : (invariantFormsResidueClassEquiv K L) Φ = residueClass K L ↑Φ ⋯ ⋯

@[simp]

theorem TauCeti.CurrentAlgebra.invariantFormsResidueClassEquiv_symm_residueClass {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {Φ : LinearMap.BilinForm K L} (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) : (invariantFormsResidueClassEquiv K L).symm (residueClass K L Φ hΦ hΦs) = ⟨Φ, ⋯⟩

The inverse of invariantFormsResidueClassEquiv recovers the form from its residue class.