27.5. TailDuality.PairDualitySurjective🔗

Jacobians.TailDuality.PairDualitySurjective — source

tailResidue_eq_sum_resAt

The master bridge: on tails of level B paired against a form of order ≥ B, the residue functional is the sum over base points of the resAt-pairings of the tail polynomial against the form's local coefficient (resAt_mul_eq_sum_tailPairing, read in reverse, with the tail polynomial as the meromorphic factor — its coefficients *are* the entries).

theorem tailResidue_eq_sum_resAt {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ g : MeromorphicFunction X) {B : Divisor X}
    (hord : PairOrderBounded g₀ g B)
    {Z : TailSpace X} (hZ : Z ∈ tailSubspace (X := X) B) (P : Finset X)
    (hP : Z.support.image Prod.fst ⊆ P) :
    tailResidue g₀ g Z = ∑ p ∈ P,
      resAt (fun z => tailFnAt Z p z * pairCoeffFun g₀ g p z) ((chartAt (H := ℂ) p) p)

pairOrderBounded_mul

The form-order bound multiplies: ord((ψ·h)·dg₀) ≥ A when ord(h·dg₀) ≥ E and A − E ≤ ord ψ.

theorem pairOrderBounded_mul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ h ψ : MeromorphicFunction X) {A E : Divisor X}
    (hord : PairOrderBounded g₀ h E) (hlev : MulLevelLE ψ A E) :
    PairOrderBounded g₀ (ψ * h) A

tailResidue_tailMul

μ-compatibility: the residue functional intertwines the multiplication action. Res_{h·dg₀}(μ_ψ Z) = Res_{(ψ·h)·dg₀}(Z) for Z of level A, the form of order ≥ E, and A − E ≤ ord ψ: per point, the defect tailFn(μ_ψ Z) − ψ·tailFn(Z) has order ≥ −E and pairs against order ≥ E to residue 0.

theorem tailResidue_tailMul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ h ψ : MeromorphicFunction X) {A E : Divisor X}
    (hord : PairOrderBounded g₀ h E) (hlev : MulLevelLE ψ A E) {Z : TailSpace X}
    (hZ : Z ∈ tailSubspace (X := X) A) :
    tailResidue g₀ h (tailMul ψ E Z) = tailResidue g₀ (ψ * h) Z

pairOrderBounded_of_vanishing

Miranda Lemma 3.6. If the residue functional of h·dg₀ (honestly defined at a fine level D') vanishes on every D'-tail killed by the D-truncation, then h·dg₀ satisfies the coarser bound D — else the single-monomial witness z^{−1−o}·p at a violating point is killed by the truncation yet pairs to the nonzero leading coefficient.

theorem pairOrderBounded_of_vanishing {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (g₀ h : MeromorphicFunction X) {D' D : Divisor X}
    (hord : PairOrderBounded g₀ h D')
    (hvan : ∀ Z : TailSpace X, Z ∈ tailSubspace (X := X) D' →
      truncateRaw (X := X) D Z = 0 → tailResidue g₀ h Z = 0) :
    PairOrderBounded g₀ h D

finrank_range_pairDualMap

dim I = l(K − D): the range of the (injective) residue pairing has the dimension of its source L(K − D)/germ0.

theorem finrank_range_pairDualMap (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X) :
    finrank ℂ ↥(LinearMap.range (pairDualMap g₀ hg₀ D))
      = lDim (X := X) (pairCanonicalDivisor g₀ hg₀ - D)

pairDualMap_recovery

The recovery step (Miranda Thm 3.3, surjectivity, second half): if φ ∘ T̄_ψ is the residue functional of h·dg₀ at the finer level D − C (with ψ ∈ L(C) of surviving germ), then φ itself is the residue functional of (ψ⁻¹h)·dg₀ at level D:

• the composite identity turns T̄_ψ ∘ μ_{ψ⁻¹} into the truncation 𝒯[D−C−div ψ] → 𝒯[D],

• μ-compatibility (tailResidue_tailMul) turns Res_{h·dg₀} ∘ μ_{ψ⁻¹} into Res_{(ψ⁻¹h)·dg₀},

• Miranda Lemma 3.6 downgrades the order bound of (ψ⁻¹h)·dg₀ from the fine level to D.

theorem pairDualMap_recovery (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    {D C : Divisor X}
    (φ : Module.Dual ℂ (mittagLefflerH1 (X := X) D))
    (ψ : ↥(linearSystem (X := X) C))
    (hψ : ∃ p : X, (ψ : MeromorphicFunction X).orderW p ≠ ⊤)
    (h : ↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - (D - C))))
    (heq : φ.comp (tailMulH1 (ψ : MeromorphicFunction X) (mulLevelLE_of_mem ψ.2 D))
      = pairDualFun g₀ hg₀ (D - C) h) :
    ∃ g : ↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D)),
      pairDualMap g₀ hg₀ D (Submodule.Quotient.mk g) = φ

pairDualMap_surjective

Serre duality for the tail H¹, the surjective half (Miranda Thm 3.3, pp. 189–191; Forster 17.9): every functional on the Mittag-Leffler H¹(D) is a residue functional Res_{h·dg₀} with h ∈ L(K − D). Pigeonhole on H¹(D − nP)* between the multiplication functionals φ ∘ T̄_ψ (ψ ∈ L(nP)) and the residue functionals, with the RR-I counts; then the recovery step pulls the matched functional back to level D. Every genus.

theorem pairDualMap_surjective (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X) :
    Function.Surjective (pairDualMap g₀ hg₀ D)

h1TailDim_eq_lDim_pairCanonical_sub

Serre duality for the tail H¹ as a dimension identity (Miranda Thm 3.3): h¹(D) = l(K − D) for the canonical divisor K = div (dg₀) of any nonconstant meromorphic g₀ — no genus hypothesis.

theorem h1TailDim_eq_lDim_pairCanonical_sub (g₀ : MeromorphicFunction X)
    (hg₀ : ¬ IsGermConstant g₀) (D : Divisor X) :
    h1TailDim (X := X) D = lDim (X := X) (pairCanonicalDivisor g₀ hg₀ - D)