25.8. AbelWeak.AbelWeakSolutions🔗

Jacobians.AbelWeak.AbelWeakSolutions — source

chartCoord

The centred chart coordinate at a: z_a(x) = chartAt a x − chartAt a a, a holomorphic coordinate on the chart source vanishing exactly at a.

def chartCoord (a : X) : X → ℂ

chartCoord_self

@[simp] theorem chartCoord_self (a : X) : chartCoord a a = 0

chartCoord_ne_zero

theorem chartCoord_ne_zero {a x : X} (hx : x ∈ (chartAt (H := ℂ) a).source) (hne : x ≠ a) :
    chartCoord a x ≠ 0

chartCoord_comp_symm_eventuallyEq

The chart-read of chartCoord a in the chart at a is the affine map w − chart a a, near any point of the chart target.

theorem chartCoord_comp_symm_eventuallyEq {a : X} {w : ℂ}
    (hw : w ∈ (chartAt (H := ℂ) a).target) :
    (chartCoord a ∘ (chartAt (H := ℂ) a).symm) =ᶠ[𝓝 w]
      fun z => z - (chartAt (H := ℂ) a) a

chartCoord_chart_analyticAt_center

chartCoord a read in the chart at a is analytic at any chart point of the source.

theorem chartCoord_chart_analyticAt_center {a x : X}
    (hx : x ∈ (chartAt (H := ℂ) a).source) :
    AnalyticAt ℂ (chartCoord a ∘ (chartAt (H := ℂ) a).symm) ((chartAt (H := ℂ) a) x)

chartCoord_zpow_chart_analyticAt

Integer powers of the centred coordinate are chart-analytic at every x in the chart source with x ≠ a (any exponent) or 0 ≤ k (any point): in the chart at a, z_a^k is (w − chart a a)^k.

theorem chartCoord_zpow_chart_analyticAt [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {a x : X} (k : ℤ)
    (hx : x ∈ (chartAt (H := ℂ) a).source) (h : x ≠ a ∨ 0 ≤ k) :
    AnalyticAt ℂ ((fun y => chartCoord a y ^ k) ∘ (chartAt (H := ℂ) x).symm)
      ((chartAt (H := ℂ) x) x)

chartCoord_zpow_contMDiffAt

Real-smoothness of z_a^k (under the same hypotheses), via the chart-analytic → real-C^∞ bridge.

theorem chartCoord_zpow_contMDiffAt [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {a x : X} (k : ℤ)
    (hx : x ∈ (chartAt (H := ℂ) a).source) (h : x ≠ a ∨ 0 ≤ k) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (fun y => chartCoord a y ^ k) x

proj01_mfderiv_eq_zero_of_chart_analyticAt

∂̄ kills chart-analytic functions (the general form of holoFn_dbar_eq_zero): if h read in the chart at x is complex-analytic at the chart image, then proj01 (mfderiv 𝓘(ℝ,ℂ) h x) = 0.

theorem proj01_mfderiv_eq_zero_of_chart_analyticAt [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {h : X → ℂ} {x : X}
    (ha : AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)) :
    Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) h x) = 0

proj01_mfderiv_chartCoord_zpow_eq_zero

∂̄(z_a^k) = 0 at points where z_a^k is chart-analytic.

theorem proj01_mfderiv_chartCoord_zpow_eq_zero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {a x : X} (k : ℤ)
    (hx : x ∈ (chartAt (H := ℂ) a).source) (h : x ≠ a ∨ 0 ≤ k) :
    Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (fun y => chartCoord a y ^ k) x) = 0

WeakSolution

Weak solution of a divisor D (Forster 20.1, normalized): a function toFun together with, at every point a, a local unit unit a on an open chart-source neighbourhood nbhd a, smooth and nonvanishing there, with the normal form

toFun = unit a · (z_a)^{D a} on nbhd a

(z_a the centred chart coordinate). The normal form holds on ALL of nbhd a with zpow-junk conventions, so toFun vanishes at both zeros and poles of D and equals unit x x off supp D. Forster's f ∈ 𝓔(X_D) is the derived contMDiffAt_toFun.

structure WeakSolution (D : Divisor X) where

toFun_eq_unit_center

The normal form at the centre: f x = ψ_x(x) · 0^{D x}.

theorem toFun_eq_unit_center (F : WeakSolution D) (x : X) :
    F.toFun x = F.unit x x * (0 : ℂ) ^ (D x)

unit_contMDiffAt

The local unit is smooth at the centre.

theorem unit_contMDiffAt (F : WeakSolution D) (a : X) {x : X} (hx : x ∈ F.nbhd a) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (F.unit a) x

coeff_eq_zero_of_mem_nbhd

The local-unit neighbourhood meets the divisor support only at its centre: a forced consistency of the structure (at x ≠ a in nbhd a the normal form at a gives f x ≠ 0, while D x ≠ 0 would force f x = 0 by the centre form at x).

theorem coeff_eq_zero_of_mem_nbhd (F : WeakSolution D) {a x : X} (hx : x ∈ F.nbhd a)
    (hne : x ≠ a) : D x = 0

toFun_eq_unit_of_coeff_zero

Off the divisor support, f equals its local unit: f x = ψ_x(x) ≠ 0.

theorem toFun_eq_unit_of_coeff_zero (F : WeakSolution D) {x : X} (hD : D x = 0) :
    F.toFun x = F.unit x x

toFun_ne_zero_of_coeff_zero

Off the divisor support, f is nonvanishing.

theorem toFun_ne_zero_of_coeff_zero (F : WeakSolution D) {x : X} (hD : D x = 0) :
    F.toFun x ≠ 0

toFun_eq_zero_of_coeff_ne_zero

On the divisor support, f vanishes (the zpow-junk normalization).

theorem toFun_eq_zero_of_coeff_ne_zero (F : WeakSolution D) {x : X} (hD : D x ≠ 0) :
    F.toFun x = 0

toFun_eventuallyEq_unit

Off the divisor support, f agrees with its local unit on a whole neighbourhood.

theorem toFun_eventuallyEq_unit (F : WeakSolution D) {x : X} (hD : D x = 0) :
    F.toFun =ᶠ[𝓝 x] F.unit x

contMDiffAt_toFun

f ∈ 𝓔(X_D) (Forster 20.1): the weak solution is real-smooth at every point of X_D = {x | 0 ≤ D x}.

theorem contMDiffAt_toFun [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X]
    (F : WeakSolution D) {a : X} (ha : 0 ≤ D a) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) F.toFun a

recast

Transport a weak solution along an equality of divisors.

def recast (h : D₁ = D₂) (F : WeakSolution D₁) : WeakSolution D₂

recast_toFun

@[simp] theorem recast_toFun (h : D₁ = D₂) (F : WeakSolution D₁) :
    (F.recast h).toFun = F.toFun

contMDiffAt_inv_complex

z ↦ z⁻¹ is real-C^∞ at any nonzero complex number, over the real model 𝓘(ℝ,ℂ).

theorem contMDiffAt_inv_complex {c : ℂ} (hc : c ≠ 0) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (fun z : ℂ => z⁻¹) c

mul

Product of weak solutions (Forster 20.1): solves D₁ + D₂. The local-unit neighbourhood is shrunk to meet the supports only at the centre.

def mul [T2Space X] [CompactSpace X] (F₁ : WeakSolution D₁) (F₂ : WeakSolution D₂) :
    WeakSolution (D₁ + D₂) where

mul_toFun_of_coeff_zero

Off both supports, the product weak solution is the pointwise product.

theorem mul_toFun_of_coeff_zero [T2Space X] [CompactSpace X] (F₁ : WeakSolution D₁)
    (F₂ : WeakSolution D₂) {x : X}
    (h₁ : D₁ x = 0) (h₂ : D₂ x = 0) :
    (F₁.mul F₂).toFun x = F₁.toFun x * F₂.toFun x

inv

Inverse of a weak solution: solves −D.

def inv (F : WeakSolution D) : WeakSolution (-D) where

one

The constant function 1 is a weak solution of the zero divisor.

def one (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    WeakSolution (0 : Divisor X) where

pow

Natural powers of a weak solution: f^n solves n • D.

def pow [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (F : WeakSolution D) :
    (n : ℕ) → WeakSolution ((n : ℤ) • D)
  | 0 => (one X).recast (by rw [Nat.cast_zero, zero_smul])
  | n + 1 => ((F.pow n).mul F).recast
      (by rw [Nat.cast_add, Nat.cast_one, add_smul, one_smul])
/-- **Integer powers of a weak solution**: `f^n` solves `n • D` (negative powers via the
inverse). -/
def zpow [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (F : WeakSolution D)
    : (n : ℤ) → WeakSolution (n • D)
  | (n : ℕ) => F.pow n
  | Int.negSucc n => ((F.pow (n + 1)).inv).recast
      (by rw [Int.negSucc_eq, neg_smul, Nat.cast_add, Nat.cast_one])
end WeakSolution
end Jacobians