27.8. TailDuality.TailDualityInjective🔗

Jacobians.TailDuality.TailDualityInjective — source

omegaCoeffFun

The local coefficient of the 1-form h·ω₀ in the canonical chart at p — the integrand of formFnResidue ω₀ h.toFun p (with coeffAt as the first factor).

noncomputable def omegaCoeffFun (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X)
    (p : X) : ℂ → ℂ

analyticAt_coeffAt_self

theorem analyticAt_coeffAt_self (ω₀ : HolomorphicOneForms X) (p : X) :
    AnalyticAt ℂ (fun z => coeffAt ω₀ p z) ((chartAt (H := ℂ) p) p)

meromorphicAt_omegaCoeffFun

theorem meromorphicAt_omegaCoeffFun (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X)
    (p : X) :
    MeromorphicAt (omegaCoeffFun ω₀ h p) ((chartAt (H := ℂ) p) p)

omegaOrderAt

The order of ω₀ at p: the meromorphic (= analytic) order of the canonical-chart coefficient.

noncomputable def omegaOrderAt (ω₀ : HolomorphicOneForms X) (p : X) : WithTop ℤ

omegaOrderAt_ne_top

For ω₀ ≠ 0, the order is finite at every point (the coefficient is not eventually zero — the identity-theorem atom coeffAt_eventually_ne_zero).

theorem omegaOrderAt_ne_top (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (p : X) :
    omegaOrderAt ω₀ p ≠ ⊤

coeffAt_self_eq_localRep

The chart-centre value of coeffAt is localRep on the diagonal.

theorem coeffAt_self_eq_localRep (ω₀ : HolomorphicOneForms X) (p : X) :
    coeffAt ω₀ p ((chartAt (H := ℂ) p) p) = Jacobians.Montel.localRep ω₀ p p

omegaOrderAt_eq_zero_of_localRep_ne_zero

A nonzero chart-centre value forces order 0 (continuity + the order-zero criterion).

theorem omegaOrderAt_eq_zero_of_localRep_ne_zero (ω₀ : HolomorphicOneForms X) (p : X)
    (hval : Jacobians.Montel.localRep ω₀ p p ≠ 0) :
    omegaOrderAt ω₀ p = 0

canonicalDivisorOf

The canonical divisor K = div ω₀ (Miranda p. 191; Forster 17.4): the zero divisor of a nonzero holomorphic 1-form, supported on its finite zero set.

noncomputable def canonicalDivisorOf (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) : Divisor X

canonicalDivisorOf_apply

theorem canonicalDivisorOf_apply (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (p : X) :
    canonicalDivisorOf ω₀ hω₀ p = WithTop.untopD 0 (omegaOrderAt ω₀ p)

coe_canonicalDivisorOf

The canonical divisor reads the order: (K p : WithTop ℤ) = omegaOrderAt ω₀ p.

theorem coe_canonicalDivisorOf (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (p : X) :
    ((canonicalDivisorOf ω₀ hω₀ p : ℤ) : WithTop ℤ) = omegaOrderAt ω₀ p

OmegaOrderBounded

Miranda's ω ∈ L^(1)(−D) in the ω₀-frame: the form h·ω₀ has local order at least D(p) at every point.

def OmegaOrderBounded (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X)
    (D : Divisor X) : Prop

meromorphicOrderAt_omegaCoeffFun

The order of the integrand is the order of ω₀ plus the order of h.

theorem meromorphicOrderAt_omegaCoeffFun (ω₀ : HolomorphicOneForms X)
    (h : MeromorphicFunction X) (p : X) :
    meromorphicOrderAt (omegaCoeffFun ω₀ h p) ((chartAt (H := ℂ) p) p)
      = omegaOrderAt ω₀ p + h.orderW p

omegaOrderBounded_iff_mem

The order bridge (Miranda p. 187): h·ω₀ has order ≥ D everywhere iff h ∈ L(K − D) for the canonical divisor K = div ω₀.

theorem omegaOrderBounded_iff_mem (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0)
    (h : MeromorphicFunction X) (D : Divisor X) :
    OmegaOrderBounded ω₀ h D
      ↔ h ∈ linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D)

omegaTailWeight

The residue pairing of a single tail monomial (p, n) against h·ω₀.

noncomputable def omegaTailWeight (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X)
    (q : X × ℤ) : ℂ

omegaTailResidue

Miranda's residue map Res_ω : 𝒯(X) → ℂ in the ω₀-frame.

noncomputable def omegaTailResidue (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X) :
    TailSpace X →ₗ[ℂ] ℂ

omegaTailResidue_apply

theorem omegaTailResidue_apply (ω₀ : HolomorphicOneForms X) (h : MeromorphicFunction X)
    (Z : TailSpace X) :
    omegaTailResidue ω₀ h Z = ∑ q ∈ Z.support, Z q * omegaTailWeight ω₀ h q

resAt_pullback_mul_omegaCoeff

The per-point pairing identity in the ω₀-frame (mirror of resAt_pullback_mul_pairCoeff, same planar core).

theorem resAt_pullback_mul_omegaCoeff (D : Divisor X) (ω₀ : HolomorphicOneForms X)
    (h f : MeromorphicFunction X) (hord : OmegaOrderBounded ω₀ 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) * omegaCoeffFun ω₀ h p z)
        ((chartAt (H := ℂ) p) p)
      = ∑ n ∈ W, tailMap D f (p, n) * omegaTailWeight ω₀ h (p, n)

omegaTailResidue_tailMap_eq_zero

The vanishing of Res_ω on realized tails, ω₀-frame (Miranda p. 187): direct from residueTheorem_formFn_unconditional at the numerator f·h, with the analytic-bad-set enlargement.

theorem omegaTailResidue_tailMap_eq_zero {D : Divisor X} (ω₀ : HolomorphicOneForms X)
    (h : MeromorphicFunction X) (hord : OmegaOrderBounded ω₀ h D)
    (f : MeromorphicFunction X) :
    omegaTailResidue ω₀ h (tailMap D f) = 0

omegaTailWeight_add

The weight is additive in h.

theorem omegaTailWeight_add (ω₀ : HolomorphicOneForms X) (h₁ h₂ : MeromorphicFunction X)
    (q : X × ℤ) :
    omegaTailWeight ω₀ (h₁ + h₂) q = omegaTailWeight ω₀ h₁ q + omegaTailWeight ω₀ h₂ q

omegaTailWeight_smul

The weight is homogeneous in h.

theorem omegaTailWeight_smul (ω₀ : HolomorphicOneForms X) (a : ℂ)
    (h : MeromorphicFunction X) (q : X × ℤ) :
    omegaTailWeight ω₀ (a • h) q = a * omegaTailWeight ω₀ h q

omegaTailWeight_eq_zero_of_germZero

The weight vanishes for germ-zero h.

theorem omegaTailWeight_eq_zero_of_germZero (ω₀ : HolomorphicOneForms X)
    {h : MeromorphicFunction X} (hh : ∀ x, h.orderW x = ⊤) (q : X × ℤ) :
    omegaTailWeight ω₀ h q = 0

omegaDualFun

The Serre duality pairing, on representatives: for h ∈ L(K−D) the descended residue functional on H¹(D).

noncomputable def omegaDualFun (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (D : Divisor X)
    (h : ↥(linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D))) :
    Module.Dual ℂ (mittagLefflerH1 (X := X) D)

omegaDualFun_mk

@[simp] theorem omegaDualFun_mk (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (D : Divisor X)
    (h : ↥(linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D)))
    (Z : ↥(tailSubspace (X := X) D)) :
    omegaDualFun ω₀ hω₀ D h (Submodule.Quotient.mk Z)
      = omegaTailResidue ω₀ h.1 (Z : TailSpace X)

omegaDualMapAux

The pairing bundled as a linear map L(K−D) →ₗ (H¹(D))* (linearity in h from the weight linearity).

noncomputable def omegaDualMapAux (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (D : Divisor X) :
    ↥(linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D))
      →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) D) where

omegaDualMap

The Serre duality pairing ι : L(K−D)/germ0 →ₗ (H¹(D))* (Miranda Thm 3.3's map, on the junk-free quotient that defines lDim).

noncomputable def omegaDualMap (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (D : Divisor X) :
    (↥(linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D))
        ⧸ (germZeroSubmodule (X := X)).submoduleOf
            (linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D)))
      →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) D)

omegaDualMap_injective

Injectivity of the duality pairing (Miranda Thm 3.3, p. 188): a class [h] ≠ 0 pairs against the single-monomial tail z^{−1−o}·p (at a point p where h's germ survives, o the local order of h·ω₀) to the leading Laurent coefficient — nonzero by laurentCoeff_order_ne_zero.

theorem omegaDualMap_injective (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) (D : Divisor X) :
    Function.Injective (omegaDualMap ω₀ hω₀ D)