27.13. TailDuality.TailResidue🔗

Jacobians.TailDuality.TailResidue — source

resAt_monomial

Res_c((·−c)^e) = δ_{e,−1} for every integer exponent.

theorem resAt_monomial (c : ℂ) (e : ℤ) :
    resAt (fun z => (z - c) ^ e) c = if e = -1 then 1 else 0

laurentCoeff_const_mul_monomial

resAt of a constant multiple of a monomial against the residue-extraction monomial: the Laurent coefficient of a·(·−c)^k at degree j is a·δ_{k,j}.

theorem laurentCoeff_const_mul_monomial (a c : ℂ) (k j : ℤ) :
    laurentCoeff (fun z => a * (z - c) ^ k) c j = if k = j then a else 0

meromorphicAt_finset_sum

Finite sums of meromorphic germs are meromorphic.

theorem meromorphicAt_finset_sum {ι : Type*} (s : Finset ι) (g : ι → ℂ → ℂ) {c : ℂ}
    (hg : ∀ i ∈ s, MeromorphicAt (g i) c) :
    MeromorphicAt (fun z => ∑ i ∈ s, g i z) c

laurentCoeff_finset_sum

Laurent coefficients of a finite sum of meromorphic germs.

theorem laurentCoeff_finset_sum {ι : Type*} (s : Finset ι) (g : ι → ℂ → ℂ) {c : ℂ}
    (hg : ∀ i ∈ s, MeromorphicAt (g i) c) (j : ℤ) :
    laurentCoeff (fun z => ∑ i ∈ s, g i z) c j = ∑ i ∈ s, laurentCoeff (g i) c j

resAt_monomial_mul

The residue of a monomial against a meromorphic factor extracts a Laurent coefficient: Res_c((·−c)^n · W) = W_{−1−n}.

theorem resAt_monomial_mul {W : ℂ → ℂ} {c : ℂ} (n : ℤ) :
    resAt (fun z => (z - c) ^ n * W z) c = laurentCoeff W c (-1 - n)

resAt_mul_eq_sum_tailPairing

The local tail-pairing identity (Miranda Ch. VI p. 187, planar core, uniform-window form). Suppose W has meromorphic order ≥ e at c, and S is a finite window of degrees < −e capturing every nonvanishing Laurent coefficient of F below −e. Then

Res_c(F·W) = ∑_{n ∈ S} F_n · W_{−1−n} :

only F's tail below −e pairs nontrivially against W (the rest has order ≥ 0). With S = ∅ this is the no-pole vanishing Res_c(F·W) = 0 for ord F ≥ −e.

theorem resAt_mul_eq_sum_tailPairing {F W : ℂ → ℂ} {c : ℂ} {e : ℤ}
    (hF : MeromorphicAt F c) (hW : MeromorphicAt W c)
    (hWord : (e : WithTop ℤ) ≤ meromorphicOrderAt W c)
    (S : Finset ℤ) (_hSlt : ∀ n ∈ S, n < -e)
    (hScap : ∀ n : ℤ, n < -e → laurentCoeff F c n ≠ 0 → n ∈ S) :
    resAt (fun z => F z * W z) c
      = ∑ n ∈ S, laurentCoeff F c n * laurentCoeff W c (-1 - n)

pairCoeffFun

The local coefficient function of the meromorphic pair-form ω = h·dg₀ in the canonical chart at p — the integrand of Jacobians.Dolbeault.pairFormResidue.

noncomputable def pairCoeffFun (g₀ h : MeromorphicFunction X) (p : X) : ℂ → ℂ

meromorphicAt_pairCoeffFun

theorem meromorphicAt_pairCoeffFun (g₀ h : MeromorphicFunction X) (p : X) :
    MeromorphicAt (pairCoeffFun g₀ h p) ((chartAt (H := ℂ) p) p)

PairOrderBounded

Miranda's ω ∈ L^(1)(−D) (Ch. VI p. 187): the pair-form h·dg₀ has local order at least D(p) at every point, computed in the canonical chart.

def PairOrderBounded (g₀ h : MeromorphicFunction X) (D : Divisor X) : Prop

tailResidueWeight

The residue pairing of a single tail monomial (p, n) against ω = h·dg₀: Res_p((z−c_p)^n·ω) = ω_{−1−n}, the (−1−n)-th Laurent coefficient of ω at p.

noncomputable def tailResidueWeight (g₀ h : MeromorphicFunction X) (q : X × ℤ) : ℂ

tailResidue

Miranda's residue map Res_ω : 𝒯(X) → ℂ (Ch. VI p. 187) for ω = h·dg₀: the finite sum of local residues ∑_p Res_p(r_p·ω), i.e. the coefficient pairing of each tail entry against ω — ℂ-linear by construction.

noncomputable def tailResidue (g₀ h : MeromorphicFunction X) : TailSpace X →ₗ[ℂ] ℂ

tailResidue_apply

theorem tailResidue_apply (g₀ h : MeromorphicFunction X) (Z : TailSpace X) :
    tailResidue g₀ h Z = ∑ q ∈ Z.support, Z q * tailResidueWeight g₀ h q

resAt_pullback_mul_pairCoeff

The residue of f·ω at p reads only f's tail below −D(p) (Miranda p. 187): the per-point pairing identity, with the window taken from the support of the truncated tail.

theorem resAt_pullback_mul_pairCoeff [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (g₀ h f : MeromorphicFunction X)
    (hord : PairOrderBounded g₀ h D) (p : X) (W : Finset ℤ)
    (hWlt : ∀ n ∈ W, n < -(D p))
    (hWcap : ∀ n : ℤ, n < -(D p) → laurentCoeffAt f.toFun p n ≠ 0 → n ∈ W) :
    resAt (fun z => f.toFun ((chartAt (H := ℂ) p).symm z) * pairCoeffFun g₀ h p z)
        ((chartAt (H := ℂ) p) p)
      = ∑ n ∈ W, tailMap D f (p, n) * tailResidueWeight g₀ h (p, n)

tailResidue_tailMap_eq_zero

The vanishing of Res_ω on realized tails (Miranda Ch. VI p. 187, every genus): for any global meromorphic f, Res_ω(α_D f) = ∑_p Res_p(f·ω) = 0 by the genus-free pair-form residue theorem. This is exactly what lets the residue map descend to the Mittag-Leffler H¹(D).

theorem tailResidue_tailMap_eq_zero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] [Nonempty X] {D : Divisor X}
    (g₀ h : MeromorphicFunction X) (hord : PairOrderBounded g₀ h D)
    (f : MeromorphicFunction X) :
    tailResidue g₀ h (tailMap D f) = 0