DbarGlueData: the Mittag-Leffler-style gluing atom

(Jacobian/DolbeaultComparison/GlueForm01.lean)

Unit: dolbeault-comparison (docs/design/dolbeault-comparison.md §4.2/§6.1). The reusable gluing atom of the comparison: local smooth functions with holomorphic discrepancies on a chart-subordinate cover determine a UNIQUE global Form01 solving dbaru_i = ω on each piece.

• Form01.ext_center [Compat]: a Form01 is determined by its center-coefficients.
• DbarGlueData: the gluing data (member cover, per-member center/local solution, holomorphic discrepancies on overlaps).
• DbarGlueData.form: the glued (0,1)-form (via Form01.ofCoeffs/Form01CoeffData).
• DbarGlueData.isDbarOn_form, DbarGlueData.form_unique.

Form01.ext_center (Compat, D4)

theorem RS.Form01.ext_center {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form01 X} (h : ∀ (x : X), η.coeffAt x (↑(chartAt ℂ x) x) = η'.coeffAt x (↑(chartAt ℂ x) x)) : η = η'

Compat (candidate for upstreaming to dbar): a Form01 is determined by its center-coefficients. From the compat field applied at the pair (p, x) (p the base point of z in x's preferred chart) and Form01.ext.

Compat: a local repeat of Jacobian.Dbar.Operator's private

contDiffOn_comp_chartAt_symm_of_contMDiffOn (needed here too, and not exported there).

DbarGlueData

structure RS.DbarGlueData (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Type u_2

Local dbar-data: smooth local functions, a chart-subordinate cover, holomorphic discrepancies. The single gluing atom of the comparison (D4).

• n : ℕ

  The number of members.

• V : Fin self.n → TopologicalSpace.Opens X

  The cover members.

• covers (x : X) : ∃ (i : Fin self.n), x ∈ self.V i
• center : Fin self.n → X

  The chart center for each member.

• subChart (i : Fin self.n) : ↑(self.V i) ⊆ (chartAt ℂ (self.center i)).source
• u : Fin self.n → X → ℂ

  The local dbar-solution on each member.

• smoothOn (i : Fin self.n) : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (self.u i) ↑(self.V i)
• holoSub (i j : Fin self.n) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (self.u i - self.u j) ↑(self.V i ⊓ self.V j)

noncomputable def RS.DbarGlueData.chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : OpenPartialHomeomorph X ℂ

The data chart at member i: the preferred chart at the center, restricted to the member.

Equations

• d.chart i = (chartAt ℂ (d.center i)).restr ↑(d.V i)

theorem RS.DbarGlueData.chart_mem_maximalAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : d.chart i ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X

theorem RS.DbarGlueData.chart_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : (d.chart i).source = ↑(d.V i)

theorem RS.DbarGlueData.coe_chart {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : ↑(d.chart i) = ↑(chartAt ℂ (d.center i))

theorem RS.DbarGlueData.coe_chart_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : ↑(d.chart i).symm = ↑(chartAt ℂ (d.center i)).symm

theorem RS.DbarGlueData.mem_chart_source_of_mem_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) {i : Fin d.n} {x : X} (hx : x ∈ d.V i) : x ∈ (d.chart i).source

theorem RS.DbarGlueData.contDiffAt_u_comp_chart_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) {x : X} (hx : x ∈ d.V i) : ContDiffAt ℝ (↑⊤) (d.u i ∘ ↑(d.chart i).symm) (↑(d.chart i) x)

Real-smoothness of the chart representative of u i, at the data chart's own point.

theorem RS.DbarGlueData.differentiableAt_u_comp_chart_symm_transition {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) {x : X} (hx : x ∈ d.V i) (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hex : x ∈ e.source) : DifferentiableAt ℝ (d.u i ∘ ↑e.symm) (↑e x)

Real-differentiability of u i's chart-i representative, transported through the transition to ANY other maximal-atlas chart e whose source contains the point.

theorem RS.DbarGlueData.wirtingerDbar_u_transport {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) {x : X} (hx : x ∈ d.V i) (e : OpenPartialHomeomorph X ℂ) (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hex : x ∈ e.source) : wirtingerDbar (d.u i ∘ ↑e.symm) (↑e x) = (starRingEnd ℂ) (deriv (↑(d.chart i) ∘ ↑e.symm) (↑e x)) * wirtingerDbar (d.u i ∘ ↑(d.chart i).symm) (↑(d.chart i) x)

The (0,1)-transport identity: wirtingerDbar of u i's representative in ANY maximal-atlas chart e (whose source contains the point) is the conj-transition of its value in the data chart i. Used both for Form01CoeffData.compat (e := chart j) and isDbarOn_form (e := chartAt x).

noncomputable def RS.DbarGlueData.coeffData {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) : Form01CoeffData X (Fin d.n)

The Form01CoeffData underlying the glued form (design §6.1).

Equations

• d.coeffData = { chart := d.chart, mem_maximalAtlas := ⋯, exists_mem := ⋯, coeff := fun (i : Fin d.n) => RS.wirtingerDbar (d.u i ∘ ↑(d.chart i).symm), contDiffOn := ⋯, compat := ⋯ }

noncomputable def RS.DbarGlueData.form {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) : Form01 X

The glued global (0,1)-form: ω|V i = dbar(u i) (design §6.1).

Equations

• d.form = RS.Form01.ofCoeffs d.coeffData

theorem RS.DbarGlueData.isDbarOn_form {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) (i : Fin d.n) : IsDbarOn (d.u i) d.form ↑(d.V i)

theorem RS.DbarGlueData.form_unique {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (d : DbarGlueData X) {η : Form01 X} (h : ∀ (i : Fin d.n), IsDbarOn (d.u i) η ↑(d.V i)) : η = d.form

Uniqueness — every well-definedness question of the comparison reduces to this.