25.6. AbelWeak.AbelPieceSolution🔗

Jacobians.AbelWeak.AbelPieceSolution — source

exists_chartCompare_unit

The chart-comparison unit. For p in the source of the chart at x₀, the centred x₀-chart coordinate of p factors as a smooth nonvanishing unit times the canonical centred coordinate chartCoord p:

chartAt x₀ x − chartAt x₀ p = u x · chartCoord p x near p.

u is dslope of the chart transition read through the chart at p; its value at p is the transition derivative, nonzero on a complex manifold.

theorem exists_chartCompare_unit {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {x₀ p : X}
    (hp : p ∈ (chartAt (H := ℂ) x₀).source) :
    ∃ (V : Set X) (u : X → ℂ), IsOpen V ∧ p ∈ V ∧
      V ⊆ (chartAt (H := ℂ) x₀).source ∩ (chartAt (H := ℂ) p).source ∧
      (∀ x ∈ V, ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) u x) ∧ (∀ x ∈ V, u x ≠ 0) ∧
      ∀ x ∈ V, (chartAt (H := ℂ) x₀) x - (chartAt (H := ℂ) x₀) p
        = u x * chartCoord p x

contMDiffAt_chart_real

The chart map is real-smooth at every source point.

theorem contMDiffAt_chart_real {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {x₀ x : X} (hx : x ∈ (chartAt (H := ℂ) x₀).source) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (chartAt (H := ℂ) x₀ : X → ℂ) x

contMDiffAt_planar_comp_chart

A planar C^∞ function read through a chart is real-smooth at every source point.

theorem contMDiffAt_planar_comp_chart {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {φ : ℂ → ℂ} (hφ : ContDiff ℝ (⊤ : ℕ∞) φ)
    {x₀ x : X} (hx : x ∈ (chartAt (H := ℂ) x₀).source) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (fun y => φ ((chartAt (H := ℂ) x₀) y)) x

AbelPlanar.PlanarPieceSolution.contMDiffAt_F_comp_chart

The piece solution F = W·(z−β)/(z−α) read through a chart is real-smooth at every source point whose chart image avoids the pole α.

theorem AbelPlanar.PlanarPieceSolution.contMDiffAt_F_comp_chart {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {c₀ α β : ℂ} {ρ : ℝ}
    (S : PlanarPieceSolution c₀ ρ α β) {x₀ x : X}
    (hx : x ∈ (chartAt (H := ℂ) x₀).source) (hne : (chartAt (H := ℂ) x₀) x ≠ α) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞)
      (fun y => S.F ((chartAt (H := ℂ) x₀) y)) x

exists_pieceWeakSolution

The per-piece weak solution. Given a planar piece solution S for the chart endpoints α = chart Pa, β = chart Pb (with trivial cofactor in the degenerate case Pa = Pb), the function S.F ∘ chart, glued with the constant 1 off the compact closedBall c₀ (5ρ)-preimage, is a weak solution of the divisor (Pb) − (Pa). It is ≡ 1 as soon as the chart image leaves ball c₀ (5ρ) (or off the chart source), and it reads as the planar S.F throughout the chart source away from the pole point.

theorem exists_pieceWeakSolution {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {x₀ Pa Pb : X} {ρ : ℝ}
    (hPa : Pa ∈ (chartAt (H := ℂ) x₀).source) (hPb : Pb ∈ (chartAt (H := ℂ) x₀).source)
    (hball : Metric.ball ((chartAt (H := ℂ) x₀) x₀) (8 * ρ) ⊆ (chartAt (H := ℂ) x₀).target)
    (S : PlanarPieceSolution ((chartAt (H := ℂ) x₀) x₀) ρ
      ((chartAt (H := ℂ) x₀) Pa) ((chartAt (H := ℂ) x₀) Pb))
    (hW1 : Pa = Pb → ∀ z, S.W z = 1) :
    ∃ sol : WeakSolution (Finsupp.single Pb (1 : ℤ) - Finsupp.single Pa 1),
      (∀ x, (x ∈ (chartAt (H := ℂ) x₀).source →
          5 * ρ < dist ((chartAt (H := ℂ) x₀) x) ((chartAt (H := ℂ) x₀) x₀)) →
        sol.toFun x = 1) ∧
      (∀ x, x ∈ (chartAt (H := ℂ) x₀).source →
        (chartAt (H := ℂ) x₀) x ≠ (chartAt (H := ℂ) x₀) Pa →
        sol.toFun x = S.F ((chartAt (H := ℂ) x₀) x))