27.4. TailDuality.PairDualityInjective🔗

Jacobians.TailDuality.PairDualityInjective — source

pairOrderAt

The order of the canonical 1-form dg₀ at p: the meromorphic order of the chart-pullback derivative (g₀ ∘ chart⁻¹)' at the chart centre (the pair-frame analog of omegaOrderAt).

noncomputable def pairOrderAt (g₀ : MeromorphicFunction X) (p : X) : WithTop ℤ

meromorphicOrderAt_pairCoeffFun

The order of the pair integrand is the order of dg₀ plus the order of h.

theorem meromorphicOrderAt_pairCoeffFun (g₀ h : MeromorphicFunction X) (p : X) :
    meromorphicOrderAt (pairCoeffFun g₀ h p) ((chartAt (H := ℂ) p) p)
      = pairOrderAt g₀ p + h.orderW p

tailResidueWeight_eq_zero_of_germZero

The weight vanishes for germ-zero h.

theorem tailResidueWeight_eq_zero_of_germZero (g₀ : MeromorphicFunction X)
    {h : MeromorphicFunction X} (hh : ∀ x, h.orderW x = ⊤) (q : X × ℤ) :
    tailResidueWeight g₀ h q = 0

pairOrderAt_eq_formOrderW

pairOrderAt is the form order of the genuine meromorphic 1-form dg₀ (CanonicalFormDifferential.formOrderW_differentialForm).

theorem pairOrderAt_eq_formOrderW [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (p : X) :
    pairOrderAt g₀ p = (differentialForm g₀).formOrderW p

pairOrderAt_ne_top

For nonconstant g₀, the order of dg₀ is finite at every point: dg₀ ≠ 0 somewhere (differentialForm_ne_zero) and the form identity theorem spreads it everywhere.

theorem pairOrderAt_ne_top [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀) (p : X) :
    pairOrderAt g₀ p ≠ ⊤

pairCanonicalDivisor

The canonical divisor K = div (dg₀) (Miranda p. 186; Forster 17.4): the divisor of the nonzero meromorphic 1-form dg₀, via exists_differentialForm_divisor.

noncomputable def pairCanonicalDivisor [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X)
    (hg₀ : ¬ IsGermConstant g₀) : Divisor X

formOrderW_pairCanonicalDivisor

K = div (dg₀) reads the form order of dg₀ (the defining property, for the §17.4 datum).

theorem formOrderW_pairCanonicalDivisor [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X)
    (hg₀ : ¬ IsGermConstant g₀) (p : X) :
    (differentialForm g₀).formOrderW p = ((pairCanonicalDivisor g₀ hg₀ p : ℤ) : WithTop ℤ)

coe_pairCanonicalDivisor

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

theorem coe_pairCanonicalDivisor [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (p : X) :
    ((pairCanonicalDivisor g₀ hg₀ p : ℤ) : WithTop ℤ) = pairOrderAt g₀ p

pairOrderBounded_iff_mem

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

theorem pairOrderBounded_iff_mem [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (h : MeromorphicFunction X) (D : Divisor X) :
    PairOrderBounded g₀ h D
      ↔ h ∈ linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D)

tailResidueWeight_add

The weight is additive in h.

theorem tailResidueWeight_add [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ h₁ h₂ : MeromorphicFunction X) (q : X × ℤ) :
    tailResidueWeight g₀ (h₁ + h₂) q
      = tailResidueWeight g₀ h₁ q + tailResidueWeight g₀ h₂ q

tailResidueWeight_smul

The weight is homogeneous in h.

theorem tailResidueWeight_smul [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (a : ℂ)
    (h : MeromorphicFunction X) (q : X × ℤ) :
    tailResidueWeight g₀ (a • h) q = a * tailResidueWeight g₀ h q

pairDualFun

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

noncomputable def pairDualFun [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X)
    (h : ↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D))) :
    Module.Dual ℂ (mittagLefflerH1 (X := X) D)

pairDualFun_mk

@[simp] theorem pairDualFun_mk [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X)
    (h : ↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D)))
    (Z : ↥(tailSubspace (X := X) D)) :
    pairDualFun g₀ hg₀ D h (Submodule.Quotient.mk Z)
      = tailResidue g₀ h.1 (Z : TailSpace X)

pairDualMapAux

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

noncomputable def pairDualMapAux [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X) :
    ↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D))
      →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) D) where

pairDualMap

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 pairDualMap [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X) :
    (↥(linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D))
        ⧸ (germZeroSubmodule (X := X)).submoduleOf
            (linearSystem (X := X) (pairCanonicalDivisor g₀ hg₀ - D)))
      →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) D)

pairDualMap_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·dg₀) to the leading Laurent coefficient — nonzero by laurentCoeff_order_ne_zero.

theorem pairDualMap_injective [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [IsManifold 𝓘(ℂ) ω X] (g₀ : MeromorphicFunction X) (hg₀ : ¬ IsGermConstant g₀)
    (D : Divisor X) :
    Function.Injective (pairDualMap g₀ hg₀ D)