Documentation

TauCeti.RingTheory.LaurentSeries.ResiduePairing

The residue pairing on Laurent series #

For Laurent series over a commutative ring, this file packages the bilinear form

(f, g) ↦ Res(f dg) = (f * g').coeff (-1).

The pairing is alternating, hence skew-symmetric, over every commutative ring: in the residue of f df the terms indexed by Xⁱ and X⁻ⁱ cancel in pairs, so no characteristic assumption is needed. It satisfies the cyclic identity obtained by taking the residue of d(fgh), and every vector field h d/dX is skew for it, since Res(h f' dg) + Res(f d(h g')) is the residue of d(f h g'). Its value on monomials fixes the sign convention; more generally it is the finite sum ∑ n f₋ₙ gₙ over the exponents allowed by the orders of f and g, and it vanishes on two power series. Over a field it is continuous for the Laurent valuation topology.

The convention agrees with LieAlgebra.LoopAlgebra.residuePairing: on monomials it is Res(aX^m d(bX^n)) = n(ab) when m + n = 0 and zero otherwise.

Main results #

source
noncomputable def LaurentSeries.residuePairing (R : Type u_1) [CommRing R] :
LinearMap.BilinForm R (LaurentSeries R)

The Laurent residue pairing Res(f dg), as a bilinear form over the coefficient ring.

Instances For
    source
    theorem LaurentSeries.residuePairing_apply (R : Type u_1) [CommRing R] (f g : LaurentSeries R) :
    ((residuePairing R) f) g = (f * (derivative R) g).coeff (-1)

    The residue pairing evaluates as the coefficient of X⁻¹ in f * g'.

    source
    theorem LaurentSeries.residuePairing_eq_neg_swap (R : Type u_1) [CommRing R] (f g : LaurentSeries R) :
    ((residuePairing R) f) g = -((residuePairing R) g) f

    Integration by parts for formal residues: Res(f dg) = -Res(g df).

    source
    @[simp]
    theorem LaurentSeries.residuePairing_self (R : Type u_1) [CommRing R] (f : LaurentSeries R) :
    ((residuePairing R) f) f = 0

    The residue pairing is alternating over every commutative ring.

    source
    theorem LaurentSeries.residuePairing_mul_right (R : Type u_1) [CommRing R] (f g h : LaurentSeries R) :
    ((residuePairing R) f) (g * h) = ((residuePairing R) (f * h)) g + ((residuePairing R) (f * g)) h

    Multiplication may be moved between the first input and the differentiated second input, up to the correction supplied by Leibniz's rule.

    source
    theorem LaurentSeries.residuePairing_mul_add_cyclic (R : Type u_1) [CommRing R] (f g h : LaurentSeries R) :
    ((residuePairing R) (f * g)) h + ((residuePairing R) (g * h)) f + ((residuePairing R) (h * f)) g = 0

    The three logarithmic terms in d(fgh) have residues summing to zero.

    source
    theorem LaurentSeries.residuePairing_mul_derivative_add (R : Type u_1) [CommRing R] (h f g : LaurentSeries R) :
    ((residuePairing R) (h * (derivative R) f)) g + ((residuePairing R) f) (h * (derivative R) g) = 0

    Vector fields are skew for the residue pairing. For every Laurent series h, the derivation f ↦ h f' satisfies Res(h f' dg) + Res(f d(h g')) = 0: the sum is the residue of the exact differential d(f h g').

    source
    @[simp]
    theorem LaurentSeries.residuePairing_single (R : Type u_1) [CommRing R] (m n : ℤ) (a b : R) :
    ((residuePairing R) ((HahnSeries.single m) a)) ((HahnSeries.single n) b) = if m + n = 0 then n • (a * b) else 0

    The residue pairing on Laurent monomials. This formula fixes the convention relative to the polynomial-loop pairing.

    source
    theorem LaurentSeries.residuePairing_eq_sum (R : Type u_1) [CommRing R] {M N : ℤ} {f g : LaurentSeries R} (hf : ↑M ≤ HahnSeries.orderTop f) (hg : ↑N ≤ HahnSeries.orderTop g) :
    ((residuePairing R) f) g = ∑ n ∈ Finset.Icc N (-M), n • (f.coeff (-n) * g.coeff n)

    The residue pairing is a finite sum of coefficients: if f has order at least M and g has order at least N, then Res(f dg) = ∑_{N ≤ n ≤ -M} n f₋ₙ gₙ.

    source
    @[simp]
    theorem LaurentSeries.residuePairing_single_zero_right (R : Type u_1) [CommRing R] (f : LaurentSeries R) (a : R) :
    ((residuePairing R) f) ((HahnSeries.single 0) a) = 0

    A constant in the differentiated input pairs to zero.

    source
    @[simp]
    theorem LaurentSeries.residuePairing_coe_powerSeries (R : Type u_1) [CommRing R] (f g : PowerSeries R) :
    ((residuePairing R) ((HahnSeries.ofPowerSeries ℤ R) f)) ((HahnSeries.ofPowerSeries ℤ R) g) = 0

    Two formal power series have zero residue pairing.

    source
    @[simp]
    theorem LaurentSeries.residuePairing_toLaurentSeries (R : Type u_1) [CommRing R] (f g : LaurentPolynomial R) :
    ((residuePairing R) (LaurentPolynomial.toLaurentSeries f)) (LaurentPolynomial.toLaurentSeries g) = (f * LaurentPolynomial.derivative g).coeff (-1)

    On Laurent polynomials, the residue pairing Res(f dg) is the coefficient of T⁻¹ in f * g', for the derivative of Laurent polynomials.

    source
    @[simp]
    theorem LaurentSeries.residuePairing_substAlgHom {K : Type u_2} [Field K] {φ : PowerSeries K} (hφ : PowerSeries.constantCoeff φ = 0) (hφ₀ : φ ≠ 0) (f g : LaurentSeries K) :
    ((residuePairing K) ((TauCeti.LaurentSeries.substAlgHom hφ hφ₀) f)) ((TauCeti.LaurentSeries.substAlgHom hφ hφ₀) g) = φ.order.toNat • ((residuePairing K) f) g

    Substitution by a nonzero parameter of order e multiplies the residue pairing by e. This includes ramified substitutions and holds in every characteristic.

    source
    theorem LaurentSeries.continuous_residuePairing (K : Type u_2) [Field K] [TopologicalSpace K] :
    Continuous fun (p : LaurentSeries K × LaurentSeries K) => ((residuePairing K) p.1) p.2

    The Laurent residue pairing is jointly continuous for the valuation topology, with any topology on the coefficient field.