16.6. Dbar.CechDiskAcyclicProof🔗

Jacobians.Dbar.CechDiskAcyclicProof — source

contDiff_dbar

DbarDisk.dbar f is C^∞ when f is. Proven WITHOUT stating ContDiff (fderiv ℝ f) — that form needs NormedAddCommGroup (ℂ →L[ℝ] ℂ), an instance broken by a diamond surfacing under CechDiskAcyclic's combined import (each constituent import resolves it; the combination does not). We route through ContDiff.contDiff_fderiv_apply, whose statement codomain is ℂ (the evaluated derivative), so the broken CLM-norm instance never appears in the goal.

theorem contDiff_dbar {f : ℂ → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f) :
    ContDiff ℝ (⊤ : ℕ∞) (DbarDisk.dbar f)

dbar_fun_sum

∂̄ distributes over a finite sum, at a point where each summand is real-differentiable.

theorem dbar_fun_sum {ι : Type*} (t : Finset ι) (f : ι → ℂ → ℂ) {z : ℂ}
    (hf : ∀ i ∈ t, DifferentiableAt ℝ (f i) z) :
    DbarDisk.dbar (fun x => ∑ i ∈ t, f i x) z = ∑ i ∈ t, DbarDisk.dbar (f i) z

chartHoloRep

The chart-image holomorphic representative of g ∈ OmegaDGerm 0 W, read in X's chart at y: the chart-pullback of the analytic representative holoFn hg. An honest analytic ℂ → ℂ.

noncomputable def chartHoloRep {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) (y : X) : ℂ → ℂ

chartHoloRep_analyticAt

Chart-transport bridge, holomorphy direction. The chart-image representative is AnalyticAt (hence DifferentiableAt ℂ) at the chart centre, for y ∈ W.

theorem chartHoloRep_analyticAt {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {y : X} (hy : y ∈ W) :
    AnalyticAt ℂ (chartHoloRep hg y) ((chartAt (H := ℂ) y) y)

chartHoloRep_dbar_eq_zero

Chart-transport bridge, ∂̄ direction. The chart-image representative satisfies DbarDisk.dbar (chartHoloRep) = 0 at the chart centre (chart-read ℂ-analytic ⟹ ℂ-differentiable ⟹ Wirtinger ∂̄ = 0). This is the holomorphy/∂̄ extension of CechH0's order-only chart bridge.

theorem chartHoloRep_dbar_eq_zero {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {y : X} (hy : y ∈ W) :
    DbarDisk.dbar (chartHoloRep hg y) ((chartAt (H := ℂ) y) y) = 0

ballSplit_pou

Function-level finite-cover ball Čech split (the n-set H¹(ball, 𝒪) = 0). Smooth h : ι → ℂ → ℂ whose ∂̄s all agree on ball c r (so all pairwise differences h_j − h_i are holomorphic there — the Čech 1-cocycle condition after PoU globalization) admit holomorphic correctors η : ι → ℂ → ℂ on the ball with η_j − η_i = h_j − h_i. Generalises ballSplit_two from 2 to n sets via a single ∂̄-solve (dbar_solvable_ball).

theorem ballSplit_pou {ι : Type*} [Nonempty ι] (c : ℂ) {r : ℝ} (hr : 0 < r)
    (h : ι → ℂ → ℂ) (hsmooth : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (h i))
    (hdbar : ∀ i j, ∀ z ∈ ball c r, DbarDisk.dbar (h i) z = DbarDisk.dbar (h j) z) :
    ∃ η : ι → ℂ → ℂ, (∀ i, DifferentiableOn ℂ (η i) (ball c r)) ∧
      ∀ i j, ∀ z ∈ ball c r, h j z - h i z = η j z - η i z

ballSplit_glued

Function-level ball Čech split with a glued ∂̄-datum (the form the partition-of-unity assembly actually produces). Smooth primitives h_i whose ∂̄ agrees on ball ∩ Ω_i with a SINGLE global smooth function ω (the glued ∂̄-datum ∂̄h_i-on-Ω_i, well-defined because the ∂̄h_i agree on overlaps) admit holomorphic correctors η_i = h_i − u on ball ∩ Ω_i, where ∂̄u = ω (dbar_solvable_ball), with η_j − η_i = h_j − h_i. This is the directly-assembly-usable shape: the remaining obligation is to BUILD h_i and the glued ω from the cocycle via PoU (OBSTRUCTION 3); the ∂̄-solve and holomorphic correction are then exactly this lemma.

theorem ballSplit_glued {ι : Type*} (c : ℂ) {r : ℝ} (hr : 0 < r)
    (Ω : ι → Set ℂ) (h : ι → ℂ → ℂ) (hsmooth : ∀ i, ContDiff ℝ (⊤ : ℕ∞) (h i))
    (dbarDatum : ℂ → ℂ) (hdatum : ContDiff ℝ (⊤ : ℕ∞) dbarDatum)
    (hagree : ∀ i, ∀ z ∈ ball c r ∩ Ω i, DbarDisk.dbar (h i) z = dbarDatum z) :
    ∃ η : ι → ℂ → ℂ, (∀ i, DifferentiableOn ℂ (η i) (ball c r ∩ Ω i)) ∧
      ∀ i j, ∀ z ∈ ball c r, h j z - h i z = η j z - η i z