25.5. AbelWeak.AbelCurveSolution🔗

Jacobians.AbelWeak.AbelCurveSolution — source

AbelPlanar.PlanarPieceSolution.trivialOfEq

The trivial planar piece solution for equal endpoints: W ≡ 1.

def AbelPlanar.PlanarPieceSolution.trivialOfEq {c₀ α β : ℂ} {ρ : ℝ} (hρ : 0 < ρ)
    (hα : dist α c₀ < ρ) (hβ : dist β c₀ < ρ) (hαβ : α = β) :
    PlanarPieceSolution c₀ ρ α β where

exists_planarPieceSolution_unital

Planar piece solutions exist with the unital degenerate normalization: W ≡ 1 whenever the endpoints coincide (needed to keep the piece chart-read uniform).

theorem exists_planarPieceSolution_unital {c₀ α β : ℂ} {ρ : ℝ} (hρ : 0 < ρ)
    (hα : dist α c₀ < ρ) (hβ : dist β c₀ < ρ) :
    ∃ S : PlanarPieceSolution c₀ ρ α β, α = β → ∀ z, S.W z = 1

isLocalPrimitiveOn_comp_chart

A planar primitive of the chart coefficient of η over a chart ball is a local primitive of η on the ball preimage (extracted from exists_isLocalPrimitiveOn).

theorem isLocalPrimitiveOn_comp_chart {η : HolomorphicOneForms X} {x₀ : X} {r : ℝ}
    (hball : ball ((chartAt (H := ℂ) x₀) x₀) r ⊆ (chartAt (H := ℂ) x₀).target)
    {G : ℂ → ℂ}
    (hG : ∀ z ∈ ball ((chartAt (H := ℂ) x₀) x₀) r,
      HasDerivAt G (Montel.localRep η x₀ ((chartAt (H := ℂ) x₀).symm z)) z) :
    IsLocalPrimitiveOn η (G ∘ (chartAt (H := ℂ) x₀))
      ((chartAt (H := ℂ) x₀).source ∩
        (chartAt (H := ℂ) x₀) ⁻¹' ball ((chartAt (H := ℂ) x₀) x₀) r)

exists_foldWeakSolution

The telescoping product of piece solutions: the product of weak solutions of the boundary divisors (γ(t_{k+1})) − (γ(t_k)), k < n, is a weak solution of (γ(t_n)) − (γ 0), and away from all subdivision points its value is the pointwise product.

theorem exists_foldWeakSolution (γ : ℝ → X) (t : ℕ → ℝ) (ht0 : t 0 = 0)
    (piece : (k : ℕ) →
      WeakSolution (Finsupp.single (γ (t (k + 1))) (1 : ℤ) - Finsupp.single (γ (t k)) 1))
    (n : ℕ) :
    ∃ F : WeakSolution (Finsupp.single (γ (t n)) (1 : ℤ) - Finsupp.single (γ 0) 1),
      ∀ x, (∀ k, x ≠ γ (t k)) →
        F.toFun x = ∏ k ∈ Finset.range n, (piece k).toFun x

CurveWeakSolution

Per-curve weak-solution data (Forster 20.5): a chart-ball subdivision 0 = t₀ ≤ … ≤ t_n = 1 of the curve, per-piece planar solutions and weak solutions with their chart reads, the product weak solution of the boundary (γ 1) − (γ 0), and the integral identity π·∫_γ η = ∑ₖ ∫ Uₖ·(η-coefficient) for every holomorphic 1-form.

structure CurveWeakSolution (γ : ℝ → X) (hγ : ContinuousOn γ (Icc 0 1)) where

exists_curveWeakSolution

Per-curve weak solutions exist for every continuous curve (Forster 20.5): subdivision over the chart-ball cover, per-piece solutions, the telescoped product, and the identity through a chart-ball primitive chain.

theorem exists_curveWeakSolution (γ : ℝ → X) (hγ : ContinuousOn γ (Icc 0 1)) :
    Nonempty (CurveWeakSolution γ hγ)