27.9. TailDuality.TailDualitySurjective🔗

Jacobians.TailDuality.TailDualitySurjective — source

tailMul_tailMul_inv_trunc

The generalized composite identity: for ψ with surviving germ and the level condition A − B ≤ ord ψ, the round trip μ_ψ(μ_{ψ⁻¹}(Z)) at levels 𝒯 → 𝒯[A] → 𝒯[B] is the plain truncation of Z at B. (The exact-shift identity tailMul_tailMul_inv is the case A = B + div ψ, Z ∈ 𝒯[B].)

theorem tailMul_tailMul_inv_trunc (ψ : MeromorphicFunction X) (hψ : ∃ x, ψ.orderW x ≠ ⊤)
    {A B : Divisor X} (h : MulLevelLE ψ A B) (Z : TailSpace X) :
    tailMul ψ B (tailMul ψ⁻¹ A Z) = truncateRaw (X := X) B Z

omegaTailResidue_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 omegaTailResidue_eq_sum_resAt (ω₀ : HolomorphicOneForms X)
    (g : MeromorphicFunction X) {B : Divisor X} (hord : OmegaOrderBounded ω₀ g B)
    {Z : TailSpace X} (hZ : Z ∈ tailSubspace (X := X) B) (P : Finset X)
    (hP : Z.support.image Prod.fst ⊆ P) :
    omegaTailResidue ω₀ g Z = ∑ p ∈ P,
      resAt (fun z => tailFnAt Z p z * omegaCoeffFun ω₀ g p z) ((chartAt (H := ℂ) p) p)

omegaOrderBounded_mul

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

theorem omegaOrderBounded_mul (ω₀ : HolomorphicOneForms X)
    (h ψ : MeromorphicFunction X) {A E : Divisor X} (hord : OmegaOrderBounded ω₀ h E)
    (hlev : MulLevelLE ψ A E) : OmegaOrderBounded ω₀ (ψ * h) A

omegaTailResidue_tailMul

μ-compatibility: the residue functional intertwines the multiplication action. Res_{h·ω₀}(μ_ψ Z) = Res_{(ψ·h)·ω₀}(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 omegaTailResidue_tailMul (ω₀ : HolomorphicOneForms X)
    (h ψ : MeromorphicFunction X) {A E : Divisor X} (hord : OmegaOrderBounded ω₀ h E)
    (hlev : MulLevelLE ψ A E) {Z : TailSpace X} (hZ : Z ∈ tailSubspace (X := X) A) :
    omegaTailResidue ω₀ h (tailMul ψ E Z) = omegaTailResidue ω₀ (ψ * h) Z

omegaOrderBounded_of_vanishing

Miranda Lemma 3.6. If the residue functional of h·ω₀ (honestly defined at a fine level D') vanishes on every D'-tail killed by the D-truncation, then h·ω₀ 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 omegaOrderBounded_of_vanishing (ω₀ : HolomorphicOneForms X)
    (h : MeromorphicFunction X) {D' D : Divisor X}
    (hord : OmegaOrderBounded ω₀ h D')
    (hvan : ∀ Z : TailSpace X, Z ∈ tailSubspace (X := X) D' →
      truncateRaw (X := X) D Z = 0 → omegaTailResidue ω₀ h Z = 0) :
    OmegaOrderBounded ω₀ h D