PoU splitting of a Čech 0-cocycle (Jacobian/DolbeaultComparison/Splitting.lean)

Unit: dolbeault-comparison (docs/design/dolbeault-comparison.md §4.3/§6.2/§6.3). Builds the Forster 12.6 "smooth splitting" of a D = 0 Čech cocycle by a partition of unity, and packages each splitting's PDE data as a DbarGlueData (via GlueForm01.lean), whose glued form dolbForm h𝒰 f is independent of the chosen splitting modulo range dbar — the input to Comparison.lean's Čech → Dolbeault map.

• Z1.repr: pointwise holomorphic representatives of a D = 0 cocycle's components.
• Z1.repr_cocycle/Z1.repr_add/Z1.repr_smul: pointwise algebraic identities on pair-meets.
• SmoothSplitting, exists_smoothSplitting (D5 formula, via RS.exists_smoothPartitionOfUnity).
• SmoothSplitting.glueData, dolbForm.
• Independence lemmas, all reducing to DbarGlueData.form_unique (sub_mem_range_dbar_of_splittings, dolbForm_add_sub_mem, dolbForm_smul_sub_mem, dolbForm_mem_range_of_mem_B1, dolbForm_res_sub_mem).

Z1.repr: pointwise holomorphic representatives

noncomputable def RS.Dolb.Z1.repr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} (f : ↥(Cech.Z1 0 𝒰)) (p : Fin 𝒰.n × Fin 𝒰.n) : X → ℂ

Pointwise holomorphic representative of a component of a D = 0 cocycle.

Equations

• RS.Dolb.Z1.repr f p = (↑(↑f p)).holoRepr

theorem RS.Dolb.Z1.repr_contMDiffOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} (f : ↥(Cech.Z1 0 𝒰)) (p : Fin 𝒰.n × Fin 𝒰.n) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (repr f p) (↑(𝒰.U p.1) ⊓ ↑(𝒰.U p.2))

theorem RS.Dolb.Z1.repr_cocycle {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} (f : ↥(Cech.Z1 0 𝒰)) {a b c : Fin 𝒰.n} {x : X} (hx : x ∈ 𝒰.U a ⊓ 𝒰.U b ⊓ 𝒰.U c) : repr f (b, c) x - repr f (a, c) x + repr f (a, b) x = 0

Pointwise cocycle identity (via evalAt rigidity; same pattern as dbar DiskAcyclic's member-splitting computation).

theorem RS.Dolb.Z1.repr_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝒰 : Cech.FinCover ⊤} (f f' : ↥(Cech.Z1 0 𝒰)) (p : Fin 𝒰.n × Fin 𝒰.n) {x : X} (hx : x ∈ 𝒰.U p.1 ⊓ 𝒰.U p.2) : repr (f + f') p x = repr f p x + repr f' p x

theorem RS.Dolb.Z1.repr_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} (c : ℂ) (f : ↥(Cech.Z1 0 𝒰)) (p : Fin 𝒰.n × Fin 𝒰.n) {x : X} (hx : x ∈ 𝒰.U p.1 ⊓ 𝒰.U p.2) : repr (c • f) p x = c * repr f p x

Extension-by-zero smul lemma

theorem RS.Dolb.contMDiffOn_smul_of_tsupport_subset {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {ψ : X → ℝ} {F : X → ℂ} {W U : TopologicalSpace.Opens X} (hψ : ContMDiff (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℝ) (↑⊤) ψ) (hsupp : tsupport ψ ⊆ ↑W) (hF : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) F (↑W ⊓ ↑U)) : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (fun (x : X) => ψ x • F x) ↑U

Extension-by-zero workhorse: ψ globally smooth with tsupport ψ ⊆ W, F smooth on W ⊓ U ⇒ fun x => ψ x • F x is smooth on U (values off W are junk-irrelevant: ψ vanishes there).

SmoothSplitting and its existence

structure RS.Dolb.SmoothSplitting {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (𝒰 : Cech.FinCover ⊤) (f : ↥(Cech.Z1 0 𝒰)) : Type u_1

A smooth splitting of a D = 0 cocycle (Forster 12.6 output, D5's frozen sign convention).

• g : Fin 𝒰.n → X → ℂ

  The member-wise functions realizing the splitting.

• smoothOn (i : Fin 𝒰.n) : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (self.g i) ↑(𝒰.U i)
• split (i j : Fin 𝒰.n) (x : X) : x ∈ 𝒰.U i ⊓ 𝒰.U j → Z1.repr f (i, j) x = self.g j x - self.g i x

theorem RS.Dolb.exists_smoothSplitting {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (𝒰 : Cech.FinCover ⊤) (f : ↥(Cech.Z1 0 𝒰)) : Nonempty (SmoothSplitting 𝒰 f)

SmoothSplitting.glueData, dolbForm

noncomputable def RS.Dolb.SmoothSplitting.glueData {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) {f : ↥(Cech.Z1 0 𝒰)} (s : SmoothSplitting 𝒰 f) : DbarGlueData X

The glue data of a splitting on a GOOD cover, and its glued form (design §6.2).

Equations

• RS.Dolb.SmoothSplitting.glueData h𝒰 s = { n := 𝒰.n, V := 𝒰.U, covers := ⋯, center := fun (i : Fin 𝒰.n) => Exists.choose ⋯, subChart := ⋯, u := s.g, smoothOn := ⋯, holoSub := ⋯ }

noncomputable def RS.Dolb.dolbForm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) (f : ↥(Cech.Z1 0 𝒰)) : Form01 X

The glued form of a chosen splitting of f on a good cover: the comparison map's core per-cover output (design §6.2).

Equations

• RS.Dolb.dolbForm h𝒰 f = (RS.Dolb.SmoothSplitting.glueData h𝒰 ⋯.some).form

Compat: IsDbarOn.add/IsDbarOn.congr

theorem RS.Dolb.IsDbarOn.add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {u v : X → ℂ} {θ η : Form01 X} {s : Set X} (hs : IsOpen s) (hu : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) u s) (hv : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) v s) (h1 : IsDbarOn u θ s) (h2 : IsDbarOn v η s) : IsDbarOn (u + v) (θ + η) s

theorem RS.Dolb.IsDbarOn.congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {u₁ u₂ : X → ℂ} {θ : Form01 X} {s : Set X} (hs : IsOpen s) (h : Set.EqOn u₁ u₂ s) (hu : IsDbarOn u₁ θ s) : IsDbarOn u₂ θ s

Independence lemmas: everything reduces to DbarGlueData.form_unique

theorem RS.Dolb.sub_mem_range_dbar_of_splittings {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) {f : ↥(Cech.Z1 0 𝒰)} (s s' : SmoothSplitting 𝒰 f) : (SmoothSplitting.glueData h𝒰 s).form - (SmoothSplitting.glueData h𝒰 s').form ∈ dbar.range

Two splittings of the same cocycle glue to forms differing by range dbar.

theorem RS.Dolb.dolbForm_mem_range_of_mem_B1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) {f : ↥(Cech.Z1 0 𝒰)} (hf : ↑f ∈ Cech.B1 0 𝒰) : dolbForm h𝒰 f ∈ dbar.range

dolbForm kills coboundaries.

theorem RS.Dolb.dolbForm_add_sub_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) (f f' : ↥(Cech.Z1 0 𝒰)) : dolbForm h𝒰 (f + f') - dolbForm h𝒰 f - dolbForm h𝒰 f' ∈ dbar.range

Additivity mod range.

theorem RS.Dolb.dolbForm_smul_sub_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) (c : ℂ) (f : ↥(Cech.Z1 0 𝒰)) : dolbForm h𝒰 (c • f) - c • dolbForm h𝒰 f ∈ dbar.range

Homogeneity mod range.

theorem RS.Dolb.dolbForm_res_sub_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] {𝒰 𝒱 : Cech.FinCover ⊤} (h𝒰 : 𝒰.IsGood) (h𝒱 : 𝒱.IsGood) (τ : Fin 𝒱.n → Fin 𝒰.n) (hτ : Cech.IsRefIdx 𝒰 𝒱 τ) (f : ↥(Cech.Z1 0 𝒰)) : dolbForm h𝒱 ((Cech.resZ1 0 τ hτ) f) - dolbForm h𝒰 f ∈ dbar.range

Refinement compatibility mod range (good-to-good).