The residue 2-cocycle on formal currents

For a bilinear form Φ on a Lie algebra L over a commutative ring R, the residue pairing on formal currents R⸨X⸩ ⊗[R] L is

(f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y),

the tensor product of the Laurent residue pairing LaurentSeries.residuePairing with Φ. It has the finite coefficient formula (u, v) ↦ ∑ n Φ(u₋ₙ, vₙ), where uₖ is the L-valued coefficient of Xᵏ and only finitely many n contribute, because both currents have finite lower order. When Φ is symmetric the pairing is alternating, hence a 2-cochain with trivial coefficients, and when Φ is moreover invariant it is a 2-cocycle. Its restriction to polynomial currents is Mathlib's residue pairing LieAlgebra.LoopAlgebra.residuePairing on loopAlgebra R ℤ L, and so its cochain restricts to Mathlib's LieAlgebra.LoopAlgebra.twoCochainOfBilinear.

The pairing vanishes on currents of orders at least M and N with M + N > 0, and on two currents of nonnegative order. In particular every current pairs to zero with all currents of sufficiently high order, and the pairing vanishes on the positive currents, those of order at least zero. Dually, it vanishes on polynomial currents of orders below M and N with M + N ≤ 1, in particular on the negative currents t⁻¹ L[t⁻¹].

The sign convention is Mathlib's: on modes x_m = Xᵐ ⊗ x, the pairing is (x_m, y_n) ↦ n Φ(x, y) δ_{m + n, 0}. The central extension cocycle c_κ = -κ(x, y) Res(f dg) of an invariant symmetric form κ is the cocycle attached here to Φ = -κ.

Main results

• TauCeti.CurrentAlgebra.residuePairing: the residue pairing on formal currents.
• TauCeti.CurrentAlgebra.residuePairing_eq_sum: its finite coefficient formula.
• TauCeti.CurrentAlgebra.residuePairing_ofLoop: its restriction to polynomial currents.
• TauCeti.CurrentAlgebra.residuePairing_ofLoop_trunc: truncating both currents far enough out preserves their pairing.
• TauCeti.CurrentAlgebra.residuePairing_eq_zero_of_mem_orderSubmodule: vanishing on currents of orders summing to a positive integer.
• TauCeti.CurrentAlgebra.residuePairing_eq_zero_of_mem_truncSubmodule: vanishing on polynomial currents of orders below M and N with M + N ≤ 1.
• TauCeti.CurrentAlgebra.residuePairing_lie: the 2-cocycle identity for an invariant form.
• TauCeti.CurrentAlgebra.twoCochainOfBilinear: the alternating 2-cochain of a symmetric form.
• TauCeti.CurrentAlgebra.twoCocycleOfBilinear: the 2-cocycle of an invariant symmetric form.
• TauCeti.CurrentAlgebra.twoCochainOfBilinearSMulRight: the residue 2-cochain (u, v) ↦ Res(f dg) Φ(x, y) • z with coefficients in a module Z with trivial action, linear in z and natural in Z.

References

• V. G. Kac, Infinite-Dimensional Lie Algebras, 3rd ed., Chapter 7, for the residue cocycle defining the affine central extension.
• E. Frenkel, Langlands Correspondence for Loop Groups, §1.3, for the residue cocycle on the formal loop algebra g((t)).

noncomputable def TauCeti.CurrentAlgebra.residuePairing (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) : LinearMap.BilinForm R (currentAlgebra R L)

The residue pairing (f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y) on formal currents.

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) (f g : LaurentSeries R) (x y : L) : ((residuePairing R L Φ) (f ⊗ₜ[R] x)) (g ⊗ₜ[R] y) = ((LaurentSeries.residuePairing R) f) g * (Φ x) y

The residue pairing on pure tensors.

theorem TauCeti.CurrentAlgebra.residuePairing_single_neg_one_sub {R : Type u_1} {L : Type u_2} [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) (x y : L) : ((residuePairing R L Φ) ((HahnSeries.single (-1)) 1 ⊗ₜ[R] x)) ((HahnSeries.single 1) 1 ⊗ₜ[R] y) - ((residuePairing R L Φ) ((HahnSeries.single 0) 1 ⊗ₜ[R] x)) ((HahnSeries.single 0) 1 ⊗ₜ[R] y) = (Φ x) y

The residue pairing of X⁻¹ ⊗ x with X ⊗ y exceeds that of 1 ⊗ x with 1 ⊗ y by Φ(x, y).

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_zero (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : residuePairing R L 0 = 0

The residue pairing of the zero form is zero.

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_smul (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) (r : R) : residuePairing R L (r • Φ) = r • residuePairing R L Φ

The residue pairing is linear in the form: rescaling the form rescales the pairing.

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_add (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ Ψ : LinearMap.BilinForm R L) : residuePairing R L (Φ + Ψ) = residuePairing R L Φ + residuePairing R L Ψ

The residue pairing is additive in the form.

theorem TauCeti.CurrentAlgebra.residuePairing_eq_sum (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) {M N : ℤ} {u v : currentAlgebra R L} (hu : u ∈ orderSubmodule R L M) (hv : v ∈ orderSubmodule R L N) : ((residuePairing R L Φ) u) v = ∑ n ∈ Finset.Icc N (-M), n • (Φ ((coeff R L (-n)) u)) ((coeff R L n) v)

The finite coefficient formula for the residue pairing: if u has order at least M and v has order at least N, then the pairing is ∑_{N ≤ n ≤ -M} n Φ(u₋ₙ, vₙ).

theorem TauCeti.CurrentAlgebra.residuePairing_eq_zero_of_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) {M N : ℤ} {u v : currentAlgebra R L} (hu : u ∈ orderSubmodule R L M) (hv : v ∈ orderSubmodule R L N) (hMN : 0 < M + N) : ((residuePairing R L Φ) u) v = 0

The residue pairing vanishes on currents of orders at least M and N when M + N > 0.

theorem TauCeti.CurrentAlgebra.residuePairing_eq_zero_of_mem_orderSubmodule_zero (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) {u v : currentAlgebra R L} (hu : u ∈ orderSubmodule R L 0) (hv : v ∈ orderSubmodule R L 0) : ((residuePairing R L Φ) u) v = 0

The residue pairing vanishes on two currents of nonnegative order.

theorem TauCeti.CurrentAlgebra.residuePairing_eq_zero_of_mem_truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) {M N : ℤ} {u v : currentAlgebra R L} (hu : u ∈ truncSubmodule R L M) (hv : v ∈ truncSubmodule R L N) (hMN : M + N ≤ 1) : ((residuePairing R L Φ) u) v = 0

The residue pairing vanishes on polynomial currents of orders below M and N when M + N ≤ 1. In particular it vanishes on two negative currents.

theorem TauCeti.CurrentAlgebra.exists_orderSubmodule_le_ker_residuePairing (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (Φ : LinearMap.BilinForm R L) (u : currentAlgebra R L) : ∃ (N : ℤ), orderSubmodule R L N ≤ ((residuePairing R L Φ) u).ker

Every current pairs to zero with all currents of sufficiently high order.

theorem TauCeti.CurrentAlgebra.residuePairing_eq_neg_swap (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {Φ : LinearMap.BilinForm R L} (hΦ : Φ.IsSymm) (u v : currentAlgebra R L) : ((residuePairing R L Φ) u) v = -((residuePairing R L Φ) v) u

The residue pairing of a symmetric form is skew-symmetric.

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_self (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {Φ : LinearMap.BilinForm R L} (hΦ : Φ.IsSymm) (u : currentAlgebra R L) : ((residuePairing R L Φ) u) u = 0

The residue pairing of a symmetric form is alternating, over every commutative ring.

theorem TauCeti.CurrentAlgebra.residuePairing_lie (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {Φ : LinearMap.BilinForm R L} (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (u v w : currentAlgebra R L) : ((residuePairing R L Φ) u) ⁅v, w⁆ = ((residuePairing R L Φ) ⁅u, v⁆) w + ((residuePairing R L Φ) v) ⁅u, w⁆

The residue pairing of an invariant form satisfies the 2-cocycle identity with trivial coefficients.

@[simp]

theorem TauCeti.CurrentAlgebra.residuePairing_ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (u v : LieAlgebra.loopAlgebra R ℤ L) : ((residuePairing R L Φ) ((ofLoop R L) u)) ((ofLoop R L) v) = ((LieAlgebra.LoopAlgebra.residuePairing R ℤ L Φ) u) v

The residue pairing restricts to Mathlib's residue pairing on polynomial currents.

theorem TauCeti.CurrentAlgebra.residuePairing_ofLoop_trunc (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) {M N P Q : ℤ} {u v : currentAlgebra R L} (hu : u ∈ orderSubmodule R L M) (hv : v ∈ orderSubmodule R L N) (hPN : 0 < P + N) (hMQ : 0 < M + Q) : ((residuePairing R L Φ) ((ofLoop R L) ((trunc R L P) u))) ((ofLoop R L) ((trunc R L Q) v)) = ((residuePairing R L Φ) u) v

Truncating both currents preserves their residue pairing, provided each cutoff exceeds minus the lower order of the other current.

noncomputable def TauCeti.CurrentAlgebra.twoCochainOfBilinear (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) : ↥(LieModule.Cohomology.twoCochain R (currentAlgebra R L) (TrivialLieModule R (currentAlgebra R L) R))

The alternating residue 2-cochain with trivial coefficients attached to a symmetric bilinear form on L: (f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y).

@[simp]

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinear_apply_apply (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (u v : currentAlgebra R L) : ((twoCochainOfBilinear R L Φ hΦ) u) v = (TrivialLieModule.equiv R (currentAlgebra R L) R).symm (((residuePairing R L Φ) u) v)

The values of the residue cochain are those of the residue pairing.

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinear_ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [HasUniqueDiv R] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (u v : LieAlgebra.loopAlgebra R ℤ L) : (TrivialLieModule.equiv R (currentAlgebra R L) R) (((twoCochainOfBilinear R L Φ hΦ) ((ofLoop R L) u)) ((ofLoop R L) v)) = (TrivialLieModule.equiv R (LieAlgebra.loopAlgebra R ℤ L) R) (((LieAlgebra.LoopAlgebra.twoCochainOfBilinear R ℤ L Φ hΦ) u) v)

The residue cochain restricts to Mathlib's residue cochain on polynomial currents.

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinear_smul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (r : R) (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (hrΦ : (r • Φ).IsSymm) : twoCochainOfBilinear R L (r • Φ) hrΦ = r • twoCochainOfBilinear R L Φ hΦ

Rescaling the form rescales the residue cochain.

noncomputable def TauCeti.CurrentAlgebra.twoCocycleOfBilinear (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) : ↥(LieModule.Cohomology.twoCocycle R (currentAlgebra R L) (TrivialLieModule R (currentAlgebra R L) R))

The residue 2-cocycle with trivial coefficients attached to an invariant symmetric bilinear form on L. For Φ = -κ it is the cocycle -κ(x, y) Res(f dg) defining the affine central extension of level κ.

@[simp]

theorem TauCeti.CurrentAlgebra.twoCocycleOfBilinear_coe (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) : ↑(twoCocycleOfBilinear R L Φ hΦ hΦs) = twoCochainOfBilinear R L Φ hΦs

The underlying cochain of the residue cocycle is the residue cochain.

theorem TauCeti.CurrentAlgebra.twoCocycleOfBilinear_smul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (r : R) (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) (hrΦ : LinearMap.BilinForm.lieInvariant L (r • Φ)) (hrΦs : (r • Φ).IsSymm) : twoCocycleOfBilinear R L (r • Φ) hrΦ hrΦs = r • twoCocycleOfBilinear R L Φ hΦ hΦs

Rescaling the form rescales the residue cocycle.

noncomputable def TauCeti.CurrentAlgebra.twoCochainOfBilinearSMulRight (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {Z : Type u_3} [AddCommGroup Z] [Module R Z] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) : Z →ₗ[R] ↥(LieModule.Cohomology.twoCochain R (currentAlgebra R L) (TrivialLieModule R (currentAlgebra R L) Z))

The residue 2-cochain with coefficients in a module Z with trivial action, attached to a symmetric bilinear form Φ on L and a vector z : Z: (f ⊗ x, g ⊗ y) ↦ Res(f dg) Φ(x, y) • z. It is linear in z; for Z = R and z = 1 it is twoCochainOfBilinear.

@[simp]

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinearSMulRight_apply_apply (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {Z : Type u_3} [AddCommGroup Z] [Module R Z] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (z : Z) (u v : currentAlgebra R L) : (((twoCochainOfBilinearSMulRight R L Φ hΦ) z) u) v = (TrivialLieModule.equiv R (currentAlgebra R L) Z).symm (((residuePairing R L Φ) u) v • z)

The values of the residue cochain with coefficients in Z are the values of the residue pairing times z.

@[simp]

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinearSMulRight_one (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) : (twoCochainOfBilinearSMulRight R L Φ hΦ) 1 = twoCochainOfBilinear R L Φ hΦ

For Z = R, the residue cochain with coefficient 1 is the scalar residue cochain.

theorem TauCeti.CurrentAlgebra.twoCochainMap_twoCochainOfBilinearSMulRight (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {Z : Type u_3} {Z' : Type u_4} [AddCommGroup Z] [Module R Z] [AddCommGroup Z'] [Module R Z'] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (g : Z →ₗ[R] Z') (z : Z) : (LieModule.Cohomology.twoCochainMap (↑(TrivialLieModule.equiv R (currentAlgebra R L) Z').symm ∘ₗ g ∘ₗ ↑(TrivialLieModule.equiv R (currentAlgebra R L) Z)) LieHom.id) ((twoCochainOfBilinearSMulRight R L Φ hΦ) z) = (twoCochainOfBilinearSMulRight R L Φ hΦ) (g z)

Naturality of the residue cochain in its coefficients. Pushing the residue cochain with coefficient z forward along a linear map g : Z → Z' gives the residue cochain with coefficient g z.

theorem TauCeti.CurrentAlgebra.twoCochainOfBilinearSMulRight_mem_twoCocycle (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {Z : Type u_3} [AddCommGroup Z] [Module R Z] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) (z : Z) : (twoCochainOfBilinearSMulRight R L Φ hΦs) z ∈ LieModule.Cohomology.twoCocycle R (currentAlgebra R L) (TrivialLieModule R (currentAlgebra R L) Z)

The residue cochain with coefficients in Z of an invariant symmetric form is a 2-cocycle.

theorem TauCeti.CurrentAlgebra.smul_eq_zero_of_neg_apply_lie_eq {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {Z : Type u_3} [AddCommGroup Z] [Module R Z] (Φ : LinearMap.BilinForm R L) (F : currentAlgebra R L → Z) (z : Z) (hF : ∀ (u v : currentAlgebra R L), -F ⁅u, v⁆ = ((residuePairing R L Φ) u) v • z) (x y : L) : (Φ x) y • z = 0

A trivial-coefficient coboundary cannot equal a residue cocycle. If -F [u, v] is Res(u, v) • z for all currents u, v, then Φ(x, y) • z = 0: the coboundary takes equal values on (X⁻¹ ⊗ x, X ⊗ y) and (1 ⊗ x, 1 ⊗ y), whose brackets agree, while the residue cocycle takes the values Φ(x, y) • z and 0 there.