Planar Cousin: cocycle splittings (Jacobian/Dbar/PlanarCousin.lean) #
Unit: dbar-solvability (docs/design/dbar-solvability.md §4.5, §7.2). Mathlib-only, planar,
project-independent (design D10).
exists_smooth_splitting: H¹(finite cover of open V, sheaf of smooth functions) = 0
(Forster 12.6, planar) — PoU-weighted average splits any smooth additive cocycle.
exists_holo_splitting_ball: Forster 13.4 (disk Cousin I) — correct the smooth splitting by a
dbar-solution (13.2/SolveDisk) to make it holomorphic.
Cocycle convention matched to cech's d0 ((d0 h)_{ij} = h_j − h_i) and Z1.rel_res
(f_{jk} − f_{ik} + f_{ij} = 0, i.e. f i k = f i j + f j k).
theorem
RS.exists_smooth_splitting
{n : ℕ}
{W : Fin n → Set ℂ}
{f : Fin n → Fin n → ℂ → ℂ}
{V : Set ℂ}
(hV : IsOpen V)
(hWo : ∀ (i : Fin n), IsOpen (W i))
(hWV : ∀ (i : Fin n), W i ⊆ V)
(hcov : V ⊆ ⋃ (i : Fin n), W i)
(hf : ∀ (i j : Fin n), ContDiffOn ℝ (↑⊤) (f i j) (W i ∩ W j))
(hcoc : ∀ (i j k : Fin n), ∀ z ∈ W i ∩ W j ∩ W k, f i k z = f i j z + f j k z)
:
Smooth splitting: H¹(finite cover of open V, ℰ) = 0 (Forster 12.6 planar).
theorem
RS.exists_holo_splitting_ball
{n : ℕ}
{W : Fin n → Set ℂ}
{f : Fin n → Fin n → ℂ → ℂ}
{c : ℂ}
{R : ℝ}
(hR : 0 < R)
(hWo : ∀ (i : Fin n), IsOpen (W i))
(hWb : ∀ (i : Fin n), W i ⊆ Metric.ball c R)
(hcov : Metric.ball c R ⊆ ⋃ (i : Fin n), W i)
(hf : ∀ (i j : Fin n), DifferentiableOn ℂ (f i j) (W i ∩ W j))
(hcoc : ∀ (i j k : Fin n), ∀ z ∈ W i ∩ W j ∩ W k, f i k z = f i j z + f j k z)
:
Holomorphic splitting on a ball (Forster 13.4, planar core; = disk Cousin I).