A machine-checked solution to the Jacobians challenge

11.4. Meromorphic.Abel🔗

Jacobians.Meromorphic.Abel — source

Divisor

A divisor on X: a formal ℤ-linear combination of points, with finite support. For compact X (as here), finite support is automatic from the support condition.

abbrev Divisor : Type _

Divisor.deg

The degree of a divisor is the sum of its coefficients. Defines a group homomorphism Divisor X →+ ℤ via Finsupp.degree.

def Divisor.deg : Divisor X →+ ℤ

DivisorOfDegZero

The subgroup of degree-zero divisors. On a compact Riemann surface, every principal divisor has degree 0 (Forster Cor 4.25).

noncomputable def DivisorOfDegZero : AddSubgroup (Divisor X)

Divisor.deg_zero

theorem Divisor.deg_zero : Divisor.deg X 0 = 0

Divisor.deg_add

theorem Divisor.deg_add (D D' : Divisor X) :
    Divisor.deg X (D + D') = Divisor.deg X D + Divisor.deg X D'

Divisor.deg_sub

theorem Divisor.deg_sub (D D' : Divisor X) :
    Divisor.deg X (D - D') = Divisor.deg X D - Divisor.deg X D'

Divisor.deg_single

theorem Divisor.deg_single (P : X) (n : ℤ) :
    Divisor.deg X (Finsupp.single P n) = n

twoPointDivisor

The divisor P - Q (formal difference of points, as a degree-0 divisor via Finsupp.single).

noncomputable def twoPointDivisor (P Q : X) : Divisor X

twoPointDivisor_deg

theorem twoPointDivisor_deg (P Q : X) :
    Divisor.deg X (twoPointDivisor X P Q) = 0

twoPointDivisor_mem_degZero

theorem twoPointDivisor_mem_degZero (P Q : X) :
    twoPointDivisor X P Q ∈ DivisorOfDegZero X

IsMeromorphic

A meromorphic function on X is a map X → ℂ that is meromorphic at every chart-image point of every chart. The basic theory (addition, multiplication, order at a point) is developed in Jacobians.LinearSystem.

def IsMeromorphic [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) : Prop

MeromorphicFunction

The type of meromorphic functions on X.

structure MeromorphicFunction [TopologicalSpace X] [ChartedSpace ℂ X] : Type _ where

IsMeromorphic.zero

The zero function is trivially meromorphic: chart pullbacks of constant functions are constant, hence meromorphic. Needs only the charted-space structure (no compactness / connectedness), so it applies to open submanifolds ↥U too.

theorem IsMeromorphic.zero [TopologicalSpace X] [ChartedSpace ℂ X] :
    IsMeromorphic X (fun _ => 0)

MeromorphicFunction.orderAtPoint

The integer order of f at x, via the chart pullback.

noncomputable def MeromorphicFunction.orderAtPoint [TopologicalSpace X] [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (x : X) : ℤ

MeromorphicFunction.orderAtPoint_eq_zero_of_eventually_zero

Lemma A: f identically zero near y ⇒ orderAtPoint f y = 0.

theorem MeromorphicFunction.orderAtPoint_eq_zero_of_eventually_zero [TopologicalSpace X]
    [ChartedSpace ℂ X]
    (f : MeromorphicFunction X) (y : X)
    (h : ∀ᶠ x in 𝓝 y, f.toFun x = 0) : f.orderAtPoint y = 0

MeromorphicFunction.orderAtPoint_chart_invariant

Lemma B: chart-invariance of the order. The order computed via an arbitrary chart e matches orderAtPoint (computed via chart_y).

Proof outline (Forster §6):

  1. Show f ∘ chart_y.symm =ᶠ (f ∘ e.symm) ∘ (e ∘ chart_y.symm) in a pointed nbhd of chart_y y, using e.left_inv on points where chart_y.symm w ∈ e.source (guaranteed by continuity of chart_y.symm + openness of e.source).

  2. Apply meromorphicOrderAt_congr to turn LHS into the composition.

  3. Apply meromorphicOrderAt_comp_of_deriv_ne_zero with g := e ∘ chart_y.symm analytic at chart_y y with nonzero derivative (both from IsManifold 𝓘(ℂ) ω — chart transitions are biholomorphic).

theorem MeromorphicFunction.orderAtPoint_chart_invariant [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) {y : X}
    (e : OpenPartialHomeomorph X ℂ) (_he : e ∈ atlas ℂ X) (hy : y ∈ e.source) :
    (meromorphicOrderAt (f.toFun ∘ e.symm) (e y)).untop₀ =
      f.orderAtPoint y

MeromorphicFunction.orderAtPoint_isolated_at

Isolation of zeros/poles around a point (Forster §6 / Miranda II.4). Combines Lemma A (identically zero case) and Lemma B (chart invariance) with the dichotomy MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero.

theorem MeromorphicFunction.orderAtPoint_isolated_at [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [T2Space X]
    (f : MeromorphicFunction X) (z : X) :
    ∃ t ∈ 𝓝 z, ∀ y ∈ t, y ≠ z → f.orderAtPoint y = 0

MeromorphicFunction.orderLocallyFinsupp

The order function as a locallyFinsuppWithin on Set.univ. Wraps orderAtPoint together with the local-finiteness proof derived from orderAtPoint_isolated_at.

noncomputable def MeromorphicFunction.orderLocallyFinsupp [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [T2Space X] (f : MeromorphicFunction X) :
    Function.locallyFinsuppWithin (Set.univ : Set X) ℤ where

MeromorphicFunction.divViaOrder

The divisor of a meromorphic function via the order function: the locallyFinsuppWithin wrapper + finiteSupport + ofSupportFinite.

noncomputable def MeromorphicFunction.divViaOrder [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [T2Space X] [CompactSpace X] (f : MeromorphicFunction X) : Divisor X

MeromorphicFunction.div

The divisor of a meromorphic function (classical construction div f = (zeros of f) - (poles of f) with multiplicities).

noncomputable def MeromorphicFunction.div [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] [T2Space X] [CompactSpace X] (f : MeromorphicFunction X) : Divisor X

abelJacobi

Abel–Jacobi map: sends a degree-0 divisor D = ∑ n_i · P_i to ∑ n_i · [ofCurve basepoint P_i] in the Jacobian (Fin gX → ℂ) ⧸ lattice: sum the periodVec of smoothPaths from a fixed basepoint P₀ to each point in the support of D, weighted by multiplicities, projected to the Jacobian quotient.

Well-definedness (independence of basepoint): uses ∑ n_i = 0 to absorb the basepoint choice. For any two basepoints P₀, P₀': AJ_{P₀} D - AJ_{P₀'} D = (∑ n_i) · [smoothPath P₀' P₀] = 0 (since ∑ n_i = 0).

noncomputable def abelJacobi [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] (D : DivisorOfDegZero X) :
    (Fin (genus X) → ℂ) ⧸ (truePeriodLattice X).toAddSubgroup

abelJacobi_twoPointDivisor

Abel-Jacobi on a two-point divisor. For A ≠ B: abelJacobi (A - B) = ofCurve P₀ A - ofCurve P₀ B where P₀ = Classical.arbitrary X. Direct computation from the definition: twoPointDivisor A B = single A 1 - single B 1 has support {A, B} for A ≠ B, and the weighted periodVec sum unfolds to the difference.

theorem abelJacobi_twoPointDivisor [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X] (A B : X) (hne : A ≠ B) :
    abelJacobi ⟨twoPointDivisor X A B, twoPointDivisor_mem_degZero X A B⟩ =
      QuotientAddGroup.mk (periodVec (smoothPath (Classical.arbitrary X) A)) -
      QuotientAddGroup.mk (periodVec (smoothPath (Classical.arbitrary X) B))