A machine-checked solution to the Jacobians challenge

7.9. Path.SmoothPathCore🔗

Jacobians.Path.SmoothPathCore — source

basepoint

Arbitrary basepoint in X (via Nonempty). The period lattice is independent of basepoint choice, because any two basepoints can be connected by a path which conjugates closed loops without changing the integral (modulo the lattice itself).

noncomputable def basepoint (X : Type*) [Nonempty X] : X

instLocPathConnectedSpaceOfChartedSpaceC

X is locally path-connected, inherited from ℂ via charts.

instance instLocPathConnectedSpaceOfChartedSpaceC
    (X : Type*) [TopologicalSpace X] [ChartedSpace ℂ X] :
    LocPathConnectedSpace X

instPathConnectedSpaceOfConnectedChartedSpace

X is path-connected (connected + locally path-connected).

instance instPathConnectedSpaceOfConnectedChartedSpace
    (X : Type*) [TopologicalSpace X] [ChartedSpace ℂ X] [ConnectedSpace X] :
    PathConnectedSpace X

continuousPath

Classical fact: for any two points on a connected compact Riemann surface, there exists a continuous path between them.

This is just PathConnectedSpace.somePath; captured as an explicit theorem for readability and for consumption by downstream Abel-Jacobi definitions. Upgrading to a *smooth* path requires additional content (smooth-approximation theorem — a known Mathlib gap for general manifolds).

noncomputable def continuousPath {X : Type*} [TopologicalSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] (P Q : X) : Path P Q

periodBasisForm

The i-th basis element of HolomorphicOneForms X, defined via ambientIso X applied to the standard unit vector. This choice aligns the period pairing with the matrix structure of ambientPhi and ambientPsi, which are expressed in the Pi.basisFun basis.

noncomputable def periodBasisForm (X : Type*) [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (i : Fin (genus X)) : HolomorphicOneForms X

periodVec

Period vector of a path γ: line integrals of each basis form.

noncomputable def periodVec {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X) :
    Fin (genus X) → ℂ

IsClosedSmoothLoop

Regularity predicate for a closed loop in X: closed endpoints

  • continuity + chart-pullback differentiability + integrability of each basis-form integrand. Packages what's needed for the lineIntegral machinery (the algebraic identities, chain rule, basis expansion) to apply sensibly.

structure IsClosedSmoothLoop {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X) : Prop where

IsClosedSmoothLoop.integrable

Each basis-form integrand is interval-integrable derived from the geometric velCont field via intervalIntegrable_form_pathSpeed_of_velContinuous.

theorem IsClosedSmoothLoop.integrable {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {γ : ℝ → X}
    (h : IsClosedSmoothLoop γ) :
    ∀ i : Fin (genus X), IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun (γ t) (pathSpeed γ t))
        MeasureTheory.volume 0 1

closedLoopPeriods

The set of period vectors arising from closed smooth loops (at any basepoint). Requires IsClosedSmoothLoop regularity so that the line-integral identities + chain rule apply.

def closedLoopPeriods (X : Type*) [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] : Set (Fin (genus X) → ℂ)

IsSmoothPath

Smooth path between two points with periodVec-integrability. Contains exactly the data needed to apply periodVec / lineIntegral machinery to the path; the endpoint hypotheses ensure the path goes from P to Q.

structure IsSmoothPath {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (P Q : X) (γ : ℝ → X) : Prop where

IsSmoothPath.integrable

Each basis-form integrand is interval-integrable derived from the geometric velCont field via intervalIntegrable_form_pathSpeed_of_velContinuous.

theorem IsSmoothPath.integrable {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {P Q : X} {γ : ℝ → X}
    (h : IsSmoothPath P Q γ) :
    ∀ i : Fin (genus X), IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun (γ t) (pathSpeed γ t))
        MeasureTheory.volume 0 1

IsSmoothPath.toClosedSmoothLoop

A smooth path from P to itself is a closed smooth loop.

theorem IsSmoothPath.toClosedSmoothLoop {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {P : X} {γ : ℝ → X}
    (h : IsSmoothPath P P γ) : IsClosedSmoothLoop γ where

isSmoothPath_const

The constant path is a smooth path (and a smooth loop). Trivial foundational case: γ = fun _ => P satisfies all IsSmoothPath conditions because chart-pullbacks of constants are constant (differentiable), and the form-integrand vanishes since pathSpeed of a constant curve is zero (pathSpeed_const).

theorem isSmoothPath_const {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (P : X) :
    IsSmoothPath P P (fun _ : ℝ => P) where

IsSmoothPath.reverse

Reverse of a smooth path is a smooth path (REAL). The reverse path t ↦ γ(1 - t) goes from Q to P when γ goes P to Q, with smoothness preserved via the chain rule on (1 - ·).

theorem IsSmoothPath.reverse {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {P Q : X} {γ : ℝ → X}
    (h : IsSmoothPath P Q γ) : IsSmoothPath Q P (Jacobians.reverse γ) where

IsSmoothPath.concat

Concatenation of two smooth paths is a smooth path — provided the junction velocities vanish (pathSpeed γ₁ 1 = 0 and pathSpeed γ₂ 0 = 0).

concat γ₁ γ₂ runs γ₁(2t) on [0,½] and γ₂(2t−1) on [½,1]. The C¹ (diff) field at the junction t = ½ requires the left and right chart velocities to agree; the two hypotheses make both one-sided derivatives 0, glued via HasDerivWithinAt on Iic ∪ Ici. This is the general form of the proven 2-piece junction lemma OfCurveSkeleton.isClosedSmoothLoop_concat_ChartBallPathSmooth_reverse_smoothPathSmooth, and the keystone for the n-piece glued path used to discharge exists_smoothPath_family: every hop there is smoothstep-reparametrized, so its endpoint velocities are 0 and the hypotheses hold.

theorem IsSmoothPath.concat {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {P Q R : X} {γ₁ γ₂ : ℝ → X}
    (h₁ : IsSmoothPath P Q γ₁) (h₂ : IsSmoothPath Q R γ₂)
    (hv₁ : pathSpeed γ₁ 1 = 0) (hv₂ : pathSpeed γ₂ 0 = 0) :
    IsSmoothPath P R (Jacobians.concat γ₁ γ₂) where

chartFormCoeff

Chart-pulled-back periodBasisForm at a chart-coord point.

Given Q₀ : X with chart e := chartAt ℂ Q₀, and a chart-coordinate z ∈ e.target, the chart-pulled-back periodBasisForm is the value of the form's local representative (from Jacobians.Montel.LocalRep) at the point e.symm z.

The local representative localRep α x₀ y evaluates α.toFun y at the canonical tangent vector at y induced by the trivialization of the tangent bundle at x₀ (applied to the unit 1 : ℂ). It is the coefficient of dz in the chart-coord expression of α.

noncomputable def chartFormCoeff {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ : X)
    (i : Fin (genus X)) (z : ℂ) : ℂ

chartFormCoeff_differentiableOn

The chart-form coefficient is holomorphic on the chart target.

Direct corollary of Jacobians.Montel.localRep_analyticOn_chartTarget (the existing chart-coord analyticity of localRep, proven via localRep_contMDiffOn + contDiffOn_omega_iff_analyticOn).

theorem chartFormCoeff_differentiableOn {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (Q₀ : X) (i : Fin (genus X)) :
    DifferentiableOn ℂ (chartFormCoeff (X := X) Q₀ i)
      ((chartAt (H := ℂ) Q₀).target)

localLiftChart

Local lift Φ_{Q₀} in chart coordinates.

For chart coord z ∈ e.target (where e = chartAt ℂ Q₀), the local lift of ofCurve P at Q₀ is

Φ̃_{Q₀, i}(z) := constant_i + ∫_0^1 chartFormCoeff Q₀ i (z₀ + t (z - z₀)) * (z - z₀) dt

where z₀ = e Q₀ and constant_i := periodVec(some-fixed-path P → Q₀) i.

For now, we only need that Φ̃_{Q₀, i} is AnalyticAt ℂ at z₀.

noncomputable def localLiftChart {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ : X)
    (constants : Fin (genus X) → ℂ)
    (i : Fin (genus X)) (z : ℂ) : ℂ

localLift

Vector-valued local lift at Q₀.

noncomputable def localLift {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ : X)
    (constants : Fin (genus X) → ℂ)
    (Q : X) : Fin (genus X) → ℂ

trivAt_symmL_one_eq_fderiv

Chart-Q₀ tangent vector via the trivialization: at any point y in the chart source of Q₀, (trivAt Q₀).symmL ℂ y 1 equals the fderiv (over ℂ) of the chart-transition map. This is a specialization of Mathlib's TangentBundle.symmL_trivializationAt_eq_core.

Note: with I = 𝓘(ℂ), range I = univ, so fderivWithin _ _ univ = fderiv. We state the lemma in the fderivWithin form to match what tangentBundleCore gives directly; downstream we rewrite to fderiv ℂ.

lemma trivAt_symmL_one_eq_fderiv {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (Q₀ y : X)
    (hy : y ∈ (chartAt (H := ℂ) Q₀).source) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) Q₀).symmL ℂ y (1 : ℂ) =
      fderivWithin ℂ ((chartAt (H := ℂ) y) ∘ (chartAt (H := ℂ) Q₀).symm)
        Set.univ ((chartAt (H := ℂ) Q₀) y) (1 : ℂ)

trivAt_symmL_one_eq_fderiv_C

ℂ-version of the chart-Q₀-frame tangent identity. Since fderivWithin ℂ _ univ = fderiv ℂ _, we can express (trivAt Q₀).symmL ℂ y 1 as the plain fderiv ℂ of the chart transition.

lemma trivAt_symmL_one_eq_fderiv_C {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (Q₀ y : X)
    (hy : y ∈ (chartAt (H := ℂ) Q₀).source) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := X)) Q₀).symmL ℂ y (1 : ℂ) =
      fderiv ℂ ((chartAt (H := ℂ) y) ∘ (chartAt (H := ℂ) Q₀).symm)
        ((chartAt (H := ℂ) Q₀) y) (1 : ℂ)

chartBallPath_mem_source_of_affine

Chart-source membership: ChartBallPath Q₀ Q₀ Q t is in (chartAt Q₀).source when the affine point is in target. Trivial consequence of ChartBallPath_mem_source.

lemma chartBallPath_mem_source_of_affine {X : Type*} [TopologicalSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] (Q₀ Q : X) (t : ℝ)
    (h_target : ((1 - (t : ℂ)) * (chartAt ℂ Q₀) Q₀ + (t : ℂ) * (chartAt ℂ Q₀) Q)
        ∈ (chartAt ℂ Q₀).target) :
    Jacobians.ChartBallPath Q₀ Q₀ Q t ∈ (chartAt (H := ℂ) Q₀).source

chartFrame_cancel

Key chart-frame cancellation lemma (pointwise). For γ := ChartBallPath Q₀ Q₀ Q and α := periodBasisForm X i, the integrand of lineIntegral α γ equals the chart-coord straight-line integrand. Specifically:

α.toFun (γ t) (pathSpeed γ t) = chartFormCoeff Q₀ i (z₀ + t(z-z₀)) · (z - z₀)

where z = (chartAt Q₀) Q, z₀ = (chartAt Q₀) Q₀.

This is the heart of sub-lemma (a) in the docstring above. The proof uses the chain rule for pathSpeed, trivAt_symmL_one_eq_fderiv_C, and ℂ-linearity of α.toFun.

lemma chartFrame_cancel {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ Q : X) (i : Fin (genus X))
    (t : ℝ)
    (h_target_nbhd : ∀ᶠ s : ℝ in nhds t,
      ((1 - (s : ℂ)) * (chartAt ℂ Q₀) Q₀ + (s : ℂ) * (chartAt ℂ Q₀) Q)
        ∈ (chartAt (H := ℂ) Q₀).target) :
    (periodBasisForm X i).toFun (Jacobians.ChartBallPath Q₀ Q₀ Q t)
        (pathSpeed (Jacobians.ChartBallPath Q₀ Q₀ Q) t) =
      chartFormCoeff (X := X) Q₀ i
        ((1 - (t : ℂ)) * (chartAt ℂ Q₀) Q₀ + (t : ℂ) * (chartAt ℂ Q₀) Q)
      * ((chartAt ℂ Q₀) Q - (chartAt ℂ Q₀) Q₀)

Q_in_chart_source_eventually

Q ∈ (chartAt Q₀).source eventually in nhds Q₀.

Chart source is open and contains Q₀.

lemma Q_in_chart_source_eventually {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (Q₀ : X) :
    ∀ᶠ Q in nhds Q₀, Q ∈ (chartAt (H := ℂ) Q₀).source

affine_in_target_eventually

Affine path stays in chart target near Q₀. Trivially, near Q₀ (where Q = Q₀), affine s = z₀ is in the chart target. We need the target-membership uniform in s ∈ Icc 0 1, for a chart-ball neighborhood of Q₀.

lemma affine_in_target_eventually {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (Q₀ : X) :
    ∀ᶠ Q in nhds Q₀, ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) Q₀) Q₀ +
        (s : ℂ) * (chartAt (H := ℂ) Q₀) Q) ∈ (chartAt (H := ℂ) Q₀).target

localLift_eq_const_add_periodVec_ChartBallPath

localLift via lineIntegral(ChartBallPath). Using chartFrame_cancel, we identify localLift Q₀ c Q with c + periodVec(ChartBallPath Q₀ Q₀ Q) componentwise, provided the affine path stays in chart target on [0,1].

This is sub-lemma (a) in the docstring above.

lemma localLift_eq_const_add_periodVec_ChartBallPath {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (Q₀ Q : X) (c : Fin (genus X) → ℂ)
    (h_target_Icc : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) Q₀) Q₀ +
        (s : ℂ) * (chartAt (H := ℂ) Q₀) Q) ∈ (chartAt (H := ℂ) Q₀).target) :
    localLift (X := X) Q₀ c Q =
      c + Jacobians.periodVec (Jacobians.ChartBallPath Q₀ Q₀ Q)

pathSpeed_smoothStep01_comp_eq

PathSpeed chain rule for smoothStep01 reparameterization.

For a smooth path γ : ℝ → X and σ := smoothStep01, the pathSpeed of γ ∘ σ at t equals σ'(t) • pathSpeed γ (σ t) via the chain rule applied to (chartAt (γ(σ t))).toFun ∘ γ ∘ σ.

Requires:

  • γ chart-pullback differentiable at σ t (i.e., the existing pathSpeed γ (σ t) is computed from a HasDerivAt).

lemma pathSpeed_smoothStep01_comp_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (γ : ℝ → X)
    (t : ℝ)
    (hγ_diff : DifferentiableAt ℝ
      ((chartAt (H := ℂ) (γ (Jacobians.smoothStep01 t))).toFun ∘ γ)
      (Jacobians.smoothStep01 t)) :
    Jacobians.pathSpeed (γ ∘ Jacobians.smoothStep01) t =
      (Jacobians.smoothStep01_deriv t : ℂ) *
        Jacobians.pathSpeed γ (Jacobians.smoothStep01 t)

isSmoothPath_ChartBallPathSmooth

IsSmoothPath for ChartBallPathSmooth (smoothstep-reparameterized).

This variant uses smoothStep01 reparameterization so that derivatives at boundary points are zero — which is what's needed for the eventual concat-smoothness argument. The start, finish, cont, diff fields are proved via the building blocks in Jacobians/Path/SmoothPath.lean; the integrable field is closed via pathSpeed_smoothStep01_comp_eq + chartFrame_cancel + ContinuousOn argument.

lemma isSmoothPath_ChartBallPathSmooth {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (Q₀ Q : X)
    (hQ_src : Q ∈ (chartAt (H := ℂ) Q₀).source)
    (h_chart_ball : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      ((1 - (s : ℂ)) * (chartAt (H := ℂ) Q₀) Q₀ +
        (s : ℂ) * (chartAt (H := ℂ) Q₀) Q) ∈ (chartAt (H := ℂ) Q₀).target) :
    Jacobians.IsSmoothPath Q₀ Q (Jacobians.ChartBallPathSmooth Q₀ Q)