Documentation

LeanPool.JacobianDiffgeo.JacobianConstruction.OfCurve

ofCurve, well-definedness, ofCurve_self, ofCurve_contMDiff (CC9, §8) #

Unit: jacobian-construction. The Abel–Jacobi map Jacobian.ofCurve, its any-path recipe (well-definedness, ofCurve_eq_of_path), ofCurve_self, and ofCurve_contMDiff (holomorphy). Path-connectedness of X is derived locally (§8.1; filed as a request to surfaces-and-charts, non-blocking).

ofCurve_contMDiff (§8.3) is gated by [DiscreteTopology (periodSubgroup X).topologicalClosure], for the same reason ChartedSpace/IsManifold (Jacobian X) are (Basic.lean's ledger): the statement itself does not elaborate without a ChartedSpace (Fin (genus X) → ℂ) (Jacobian X) instance for its codomain. Modulo that (unavoidable) hypothesis, the proof is complete: fix x₀, work in the chart e := chartAt ℂ x₀; each coeffIn e (basis X i) has a holomorphic primitive g i on a ball around e x₀ (planar Morera); the straight-segment path in the chart (pulled back through e.symm via Path.segment/Path.map') gives ofCurve P z = ULift.up (mk (v₀ + g (e z))) near x₀ (hkey); reading this through the Jacobian's own chart (the same locally-constant lattice-shift computation as Torus.contMDiff_add_torus/ULift.contMDiff_uliftUp) makes the chart composite affine in g (e z), hence analytic.

§8.1: path-connectedness of X (small gap, filled here; Compat) #

source
instance instLocallyPathConnectedSpace_leanPool {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] :
LocallyPathConnectedSpace X

Compat: X is locally path-connected, via its charts into ℂ (a locally convex space). Filed as a request to surfaces-and-charts (docs/requests/surfaces-and-charts.md); carried here as a local instance since no upstream unit currently provides it.

source
instance instPathConnectedSpace_leanPool {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] :
PathConnectedSpace X

Compat: X is path-connected (ConnectedSpace X + LocallyPathConnectedSpace X).

periodVector of a loop, at any basepoint, lies in periodSubgroup X #

source
theorem RS.periodVector_mem_periodSubgroup {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} (γ : Path x x) :
periodVector (basis X) γ ∈ periodSubgroup X

Basepoint-independence of the period subgroup: for any based loop γ at any point x (not just at periodSubgroup's defining basepoint), periodVector (basis X) γ still lies in periodSubgroup X, via conjugation by a connecting path (RS.period_conj).

ofCurve (§8.2) #

source
noncomputable def Jacobian.ofCurve {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : X) :
X → Jacobian X

The Abel–Jacobi map from a compact Riemann surface to its Jacobian (docs/Jacobian_challenge.lean:92): integrate the basis of holomorphic 1-forms along some path from P to x (any choice; well-defined mod periods, ofCurve_eq_of_path).

Equations
Instances For
    source
    theorem Jacobian.ofCurve_eq_of_path {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P x : X) (σ : Path P x) :
    ofCurve P x = { down := ↑fun (i : Fin (genus X)) => RS.pathIntegral σ ((RS.basis X) i) }

    ofCurve computed along any path σ : Path P x, not just the canonical PathConnectedSpace.somePath — the any-path recipe, and the source of well-definedness.

    source
    @[simp]
    theorem Jacobian.ofCurve_self {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : X) :
    ofCurve P P = 0

    ofCurve_contMDiff (§8.3) #

    source
    theorem Jacobian.ofCurve_contMDiff {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DiscreteTopology ↥(RS.periodSubgroup X).topologicalClosure] (P : X) :
    ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ⊤ (ofCurve P)

    Holomorphy of the Abel–Jacobi map. Fix x₀; work in the chart e := chartAt ℂ x₀. Each coeffIn e (basis X i) has a holomorphic primitive g i on a ball around e x₀ (planar Morera, exists_hasDerivAt_ball), normalized to vanish at e x₀. For z in a further sub-neighborhood U of x₀, the straight-segment path in the chart, pulled back through e.symm (Path.segment/Path.map'), stays inside a single chart-ball, so IsPrimitiveAlongMap gives pathIntegral (segment path) (basis X i) = g i (e z). Composing with a fixed path P → x₀ and using ofCurve_eq_of_path, ofCurve P z = ULift.up (mk (v₀ + g (e z))) on U, where v₀ is constant; reading this in the Jacobian's own chart (via Torus's locally-constant lattice-shift lemma) makes the chart composite affine in g (e z), hence analytic.