25.4. AbelWeak.AbelChains🔗

Jacobians.AbelWeak.AbelChains — source

hasDerivAt_comp_of_isLocalPrimitiveOn

Pointwise FTC along a path. If F is a local primitive of η near γ t, and the chart pullback of γ is differentiable at t, then F ∘ γ has derivative η (γ t) (pathSpeed γ t) at t.

theorem hasDerivAt_comp_of_isLocalPrimitiveOn
    {η : HolomorphicOneForms X} {F : X → ℂ} {U : Set X}
    (hprim : IsLocalPrimitiveOn η F U) {γ : ℝ → X} {t : ℝ}
    (hmem : γ t ∈ U) (hcont : ContinuousAt γ t)
    (hdiff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    HasDerivAt (F ∘ γ) ((η.toFun (γ t) (pathSpeed γ t) : ℂ)) t

pathPrimValue_eq_lineIntegral

The FTC bridge. For a chart-C¹ path with integrable integrand, the discrete path value (the telescoping primitive-chain sum, classically ∫_γ η) equals the line integral. Each chain block integrates by the pointwise FTC; the blocks sum by adjacency.

theorem pathPrimValue_eq_lineIntegral (η : HolomorphicOneForms X) {γ : ℝ → X}
    (hγ : ContinuousOn γ (Icc 0 1)) (hcont : Continuous γ)
    (hdiff : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t)
    (hint : IntervalIntegrable (fun s => η.toFun (γ s) (pathSpeed γ s)) volume 0 1) :
    pathPrimValue η γ hγ = lineIntegral η γ

IsSmoothPath.pathPrimValue_eq_lineIntegral

The FTC bridge for a smooth path, any holomorphic form (the integrand is integrable from the continuous-velocity field).

theorem IsSmoothPath.pathPrimValue_eq_lineIntegral {P Q : X} {γ : ℝ → X}
    (h : IsSmoothPath P Q γ) (η : HolomorphicOneForms X)
    (hγ : ContinuousOn γ (Icc 0 1)) :
    pathPrimValue η γ hγ = lineIntegral η γ

IsClosedSmoothLoop.pathPrimValue_eq_lineIntegral

The FTC bridge for a closed smooth loop, any holomorphic form.

theorem IsClosedSmoothLoop.pathPrimValue_eq_lineIntegral {γ : ℝ → X}
    (h : IsClosedSmoothLoop γ) (η : HolomorphicOneForms X)
    (hγ : ContinuousOn γ (Icc 0 1)) :
    pathPrimValue η γ hγ = lineIntegral η γ

IsSmoothPath.pathPrimValue_eq_periodVec

The discrete path value of the i-th basis form along a smooth path is the i-th component of the period vector.

theorem IsSmoothPath.pathPrimValue_eq_periodVec {P Q : X} {γ : ℝ → X}
    (h : IsSmoothPath P Q γ) (i : Fin (genus X)) (hγ : ContinuousOn γ (Icc 0 1)) :
    pathPrimValue (periodBasisForm X i) γ hγ = periodVec γ i

IsClosedSmoothLoop.pathPrimValue_eq_periodVec

The discrete path value of the i-th basis form along a closed smooth loop is the i-th component of the period vector.

theorem IsClosedSmoothLoop.pathPrimValue_eq_periodVec {γ : ℝ → X}
    (h : IsClosedSmoothLoop γ) (i : Fin (genus X)) (hγ : ContinuousOn γ (Icc 0 1)) :
    pathPrimValue (periodBasisForm X i) γ hγ = periodVec γ i

OneChain

A 1-chain on X (Forster §20.4): finitely many curves with ℤ-coefficients. Curves are totalized to ℝ → X; only the restriction to [0,1] matters, and continuity is required there.

structure OneChain (X : Type*) [TopologicalSpace X] where

boundary

The boundary divisor ∂c = ∑ n_j ((γ_j 1) − (γ_j 0)) of a 1-chain (Forster §20.4).

def boundary (c : OneChain X) : Divisor X

period

The period ∫_c η = ∑ n_j ∫_{γ_j} η of a 1-chain against a holomorphic 1-form, with each curve integral in its discrete (pathPrimValue) incarnation.

def period (c : OneChain X) (η : HolomorphicOneForms X) : ℂ

exists_oneChain_of_abelJacobi_eq_zero

The Abel hypothesis, unfolded (Forster 20.7 (∗)): if the Abel–Jacobi class of the two-point divisor P − Q vanishes (P ≠ Q), there is a 1-chain c with ∂c = P − Q whose period against every basis form is zero.

theorem exists_oneChain_of_abelJacobi_eq_zero {P Q : X} (hPQ : P ≠ Q)
    (h : abelJacobi ⟨twoPointDivisor X P Q, twoPointDivisor_mem_degZero X P Q⟩ = 0) :
    ∃ c : OneChain X, c.boundary = twoPointDivisor X P Q ∧
      ∀ i : Fin (genus X), c.period (periodBasisForm X i) = 0