A machine-checked solution to the Jacobians challenge

27.10. TailDuality.TailDualitySurjectiveAssembly🔗

Jacobians.TailDuality.TailDualitySurjectiveAssembly — source

tailMul_add_multiplier

μ_ψ(Z) is additive in the multiplier ψ: the Laurent coefficients of (ψ₁ + ψ₂)·(tail polynomial) split (laurentCoeff_add).

theorem tailMul_add_multiplier (ψ₁ ψ₂ : MeromorphicFunction X) (E : Divisor X)
    (Z : TailSpace X) :
    tailMul (ψ₁ + ψ₂) E Z = tailMul ψ₁ E Z + tailMul ψ₂ E Z

tailMul_smul_multiplier

μ_ψ(Z) is homogeneous in the multiplier ψ.

theorem tailMul_smul_multiplier (a : ℂ) (ψ : MeromorphicFunction X) (E : Divisor X)
    (Z : TailSpace X) :
    tailMul (a • ψ) E Z = a • tailMul ψ E Z

tailMul_eq_zero_of_germZero

For a germ-zero multiplier the operator vanishes: ψ·(tail polynomial) is eventually 0 on every punctured chart neighbourhood, so all its Laurent coefficients vanish.

theorem tailMul_eq_zero_of_germZero {ψ : MeromorphicFunction X}
    (hψ : ∀ x, ψ.orderW x = ⊤) (E : Divisor X) (Z : TailSpace X) :
    tailMul ψ E Z = 0

tailMulDual

The Λ-side assignment on representatives: ψ ∈ L(C) ↦ φ ∘ T̄_ψ : H¹(B − C) → ℂ (T̄_ψ : H¹(B − C) → H¹(B) by the level condition mulLevelLE_of_mem). Linear in ψ because μ_ψ is (tailMul_add_multiplier/tailMul_smul_multiplier).

noncomputable def tailMulDual :
    ↥(linearSystem (X := X) C) →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) (B - C)) where

tailMulDual_apply

@[simp] theorem tailMulDual_apply (ψ : ↥(linearSystem (X := X) C)) :
    tailMulDual φ C ψ
      = φ.comp (tailMulH1 (ψ : MeromorphicFunction X) (mulLevelLE_of_mem ψ.2 B))

tailMulDual_eq_zero_of_germZero

A germ-zero multiplier is sent to the zero functional.

theorem tailMulDual_eq_zero_of_germZero (ψ : ↥(linearSystem (X := X) C))
    (hψ : ∀ x, (ψ : MeromorphicFunction X).orderW x = ⊤) :
    tailMulDual φ C ψ = 0

tailMulDualQ

The Λ-side dual map descended to the junk-free quotient L(C)/germ0 (the space whose finrank is lDim C).

noncomputable def tailMulDualQ :
    lSysModule (X := X) C →ₗ[ℂ] Module.Dual ℂ (mittagLefflerH1 (X := X) (B - C))

tailMulDualQ_mk

@[simp] theorem tailMulDualQ_mk (ψ : ↥(linearSystem (X := X) C)) :
    tailMulDualQ φ C (Submodule.Quotient.mk ψ) = tailMulDual φ C ψ

tailMulDualQ_injective

For φ ≠ 0 the Λ-side dual map is injective (Forster 17.8: φ ∘ T̄_ψ ≠ 0 whenever the germ of ψ survives).

theorem tailMulDualQ_injective (hφ : φ ≠ 0) :
    Function.Injective (tailMulDualQ φ C)

finrank_range_tailMulDualQ

dim Λ = l(C) for φ ≠ 0.

theorem finrank_range_tailMulDualQ (hφ : φ ≠ 0) :
    finrank ℂ ↥(LinearMap.range (tailMulDualQ φ C)) = lDim (X := X) C

finrank_range_omegaDualMap

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_omegaDualMap (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0)
    (D : Divisor X) :
    finrank ℂ ↥(LinearMap.range (omegaDualMap ω₀ hω₀ D))
      = lDim (X := X) (canonicalDivisorOf ω₀ hω₀ - D)

omegaDualMap_recovery

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

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

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

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

theorem omegaDualMap_recovery (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0) {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) (canonicalDivisorOf ω₀ hω₀ - (D - C))))
    (heq : φ.comp (tailMulH1 (ψ : MeromorphicFunction X) (mulLevelLE_of_mem ψ.2 D))
      = omegaDualFun ω₀ hω₀ (D - C) h) :
    ∃ g : ↥(linearSystem (X := X) (canonicalDivisorOf ω₀ hω₀ - D)),
      omegaDualMap ω₀ hω₀ D (Submodule.Quotient.mk g) = φ

omegaDualMap_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·ω₀} 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.

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

h1TailDim_eq_lDim_canonical_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 ω₀ of any nonzero holomorphic 1-form.

theorem h1TailDim_eq_lDim_canonical_sub (ω₀ : HolomorphicOneForms X) (hω₀ : ω₀ ≠ 0)
    (D : Divisor X) :
    h1TailDim (X := X) D = lDim (X := X) (canonicalDivisorOf ω₀ hω₀ - D)