30.5. Abel.AbelEngineMeromorphic🔗

Jacobians.Abel.AbelEngineMeromorphic — source

dbar_holo_comp

The ∂̄ chain rule for a holomorphic OUTER map: ∂̄(f∘g) = f′(g)·∂̄g.

theorem dbar_holo_comp {f g : ℂ → ℂ} {w : ℂ} (hf : DifferentiableAt ℂ f (g w))
    (hg : DifferentiableAt ℝ g w) :
    DbarDisk.dbar (f ∘ g) w = deriv f (g w) * DbarDisk.dbar g w

dbar_neg

∂̄(−g) = −∂̄g.

theorem dbar_neg {g : ℂ → ℂ} (w : ℂ) :
    DbarDisk.dbar (fun z => -(g z)) w = -DbarDisk.dbar g w

exists_meromorphic_of_oneChain

The Abel engine (Forster 20.7, sufficiency): a 1-chain whose basis periods all vanish bounds a principal divisor — there is a meromorphic function with div f = ∂c, together with its centred local normal form f̂ = H·(w − w₀)^{∂c(a)} (analytic nonvanishing H) at every point — the Laurent data the discreteness argument reads residues from.

theorem exists_meromorphic_of_oneChain (c : OneChain X)
    (hper : ∀ i : Fin (genus X), c.period (periodBasisForm X i) = 0) :
    ∃ f : MeromorphicFunction X, f.div = c.boundary ∧
      ∀ a : X, ∃ H : ℂ → ℂ,
        AnalyticAt ℂ H ((chartAt (H := ℂ) a) a) ∧ H ((chartAt (H := ℂ) a) a) ≠ 0 ∧
        (f.toFun ∘ (chartAt (H := ℂ) a).symm) =ᶠ[𝓝 ((chartAt (H := ℂ) a) a)]
          fun w => H w * (w - (chartAt (H := ℂ) a) a) ^ (c.boundary a)