Form01 X: smooth (0,1)-forms as chart-coefficient families (Jacobian/Dbar/Form01.lean)

Unit: dbar-solvability (docs/design/dbar-solvability.md D5/D8, §4.6).

Per design D5, Form01 X is not a bundled ContMDiffSection (unlike Form1, CC1): there is no anti-linear Hom-bundle in mathlib at the pin, and the blueprint's restrictScalars ℂ→ℝ diamond warning rules out building one. Instead Form01 X is a plain structure: a chartAt-indexed family of coefficient functions (the coefficient of dz-bar), zero off chart targets (junk-normalized so ext is honest), smooth on targets, with the anti-holomorphic transition rule coeff_y = conj (deriv τ) * (coeff_x ∘ τ). This mirrors the frozen CC1 coeffIn philosophy (Jacobian/Forms/Coeffs.lean) with conj inserted, reusing analyticAt_trans/deriv_trans_comp from Jacobian/Forms/Analyticity.lean.

(Note: η, η' are used for Form01 variables rather than the more suggestive ω — ω is a reserved token in the ambient ContDiff scope's regularity level and cannot be reused as an ordinary identifier.)

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

A smooth (0,1)-form on X: a chartAt-indexed coefficient family for dz-bar, junk-zero off chart targets, smooth on targets, related on overlaps by the anti-holomorphic transition rule.

• coeffAt : X → ℂ → ℂ

  The coefficient function in the preferred chart at each point.

• coeffAt_zero_off (x : X) (z : ℂ) : z ∉ (chartAt ℂ x).target → self.coeffAt x z = 0
• contDiffOn_coeffAt (x : X) : ContDiffOn ℝ (↑⊤) (self.coeffAt x) (chartAt ℂ x).target
• compat (x y : X) (z : ℂ) : z ∈ ↑(chartAt ℂ y) '' ((chartAt ℂ x).source ∩ (chartAt ℂ y).source) → self.coeffAt y z = (starRingEnd ℂ) (deriv (↑(chartAt ℂ x) ∘ ↑(chartAt ℂ y).symm) z) * self.coeffAt x (↑(chartAt ℂ x) (↑(chartAt ℂ y).symm z))

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

A (0,1)-form is determined by its preferred-chart coefficients on chart targets.

theorem RS.Form01.ext_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η η' : Form01 X} : η = η' ↔ ∀ (x : X), ∀ z ∈ (chartAt ℂ x).target, η.coeffAt x z = η'.coeffAt x z

@[instance_reducible]

instance RS.Form01.instZero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Zero (Form01 X)

Equations

• RS.Form01.instZero = { zero := { coeffAt := fun (x : X) (x_1 : ℂ) => 0, coeffAt_zero_off := ⋯, contDiffOn_coeffAt := ⋯, compat := ⋯ } }

@[instance_reducible]

instance RS.Form01.instAdd {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Add (Form01 X)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance RS.Form01.instNeg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Neg (Form01 X)

Equations

• RS.Form01.instNeg = { neg := fun (η : RS.Form01 X) => { coeffAt := fun (x : X) (z : ℂ) => -η.coeffAt x z, coeffAt_zero_off := ⋯, contDiffOn_coeffAt := ⋯, compat := ⋯ } }

@[instance_reducible]

instance RS.Form01.instSub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Sub (Form01 X)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance RS.Form01.instSMulComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : SMul ℂ (Form01 X)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.Form01.coeffAt_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (z : ℂ) : coeffAt 0 x z = 0

@[simp]

theorem RS.Form01.coeffAt_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η η' : Form01 X) (x : X) (z : ℂ) : (η + η').coeffAt x z = η.coeffAt x z + η'.coeffAt x z

@[simp]

theorem RS.Form01.coeffAt_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form01 X) (x : X) (z : ℂ) : (-η).coeffAt x z = -η.coeffAt x z

@[simp]

theorem RS.Form01.coeffAt_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η η' : Form01 X) (x : X) (z : ℂ) : (η - η').coeffAt x z = η.coeffAt x z - η'.coeffAt x z

@[simp]

theorem RS.Form01.coeffAt_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (η : Form01 X) (x : X) (z : ℂ) : (c • η).coeffAt x z = c * η.coeffAt x z

@[instance_reducible]

instance RS.Form01.instAddCommGroup {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : AddCommGroup (Form01 X)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance RS.Form01.instModuleComplex {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module ℂ (Form01 X)

Equations

• RS.Form01.instModuleComplex = { toSMul := RS.Form01.instSMulComplex, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

Form01.ofCoeffs: constructing forms from compatible chart-coefficient data

Transcribed from Form1CoeffData/Form1.ofCoeffs (Jacobian/Forms/OfCoeffs.lean), with a starRingEnd ℂ (conj) inserted in the transition rule for the anti-holomorphic (0,1)-grading. Unlike Form1 (a bundled ContMDiffSection), Form01 is a raw chart-coefficient structure, so this construction is simpler than Form1.ofCoeffs: no covector/hom-bundle detour, just a direct X → ℂ → ℂ assembly via a chosen covering-chart index per point (idx), verified independent of the choice by the compat field + the transition chain rule (RS.deriv_trans_comp, RS.analyticAt_trans from Jacobian/Forms/Analyticity.lean). Added under dolbeault-comparison's authorization (needed by GlueForm01.lean's DbarGlueData.form constructor, design §6.1).

structure RS.Form01CoeffData (X : Type u_2) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (ι : Type u_3) : Type (max u_2 u_3)

Compatible smooth (0,1)-coefficient data over a covering family of ω-maximal-atlas charts: a real-smooth coefficient function on each chart target, related on overlaps by the conj-transition rule.

• chart : ι → OpenPartialHomeomorph X ℂ

  The covering chart family.

• mem_maximalAtlas (i : ι) : self.chart i ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X
• exists_mem (x : X) : ∃ (i : ι), x ∈ (self.chart i).source
• coeff : ι → ℂ → ℂ

  The coefficient functions, one per chart.

• contDiffOn (i : ι) : ContDiffOn ℝ (↑⊤) (self.coeff i) (self.chart i).target
• compat (i j : ι) (x : X) : x ∈ (self.chart i).source ∩ (self.chart j).source → self.coeff j (↑(self.chart j) x) = (starRingEnd ℂ) (deriv (↑(self.chart i) ∘ ↑(self.chart j).symm) (↑(self.chart j) x)) * self.coeff i (↑(self.chart i) x)

noncomputable def RS.Form01CoeffData.idx {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x : X) : ι

A chosen chart index for each point.

Equations

• Data.idx x = ⋯.choose

theorem RS.Form01CoeffData.mem_source_idx {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x : X) : x ∈ (Data.chart (Data.idx x)).source

noncomputable def RS.Form01CoeffData.rawCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x : X) (z : ℂ) : ℂ

The coefficient of the assembled (0,1)-form in the preferred chart at x, junk-0 off the chart target.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Form01CoeffData.rawCoeffAt_of_not_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) {x : X} {z : ℂ} (hz : z ∉ (chartAt ℂ x).target) : Data.rawCoeffAt x z = 0

theorem RS.Form01CoeffData.rawCoeffAt_of_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) {x : X} {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : Data.rawCoeffAt x z = (starRingEnd ℂ) (deriv (↑(Data.chart (Data.idx (↑(chartAt ℂ x).symm z))) ∘ ↑(chartAt ℂ x).symm) z) * Data.coeff (Data.idx (↑(chartAt ℂ x).symm z)) (↑(Data.chart (Data.idx (↑(chartAt ℂ x).symm z))) (↑(chartAt ℂ x).symm z))

theorem RS.Form01CoeffData.rawCoeffAt_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) {x : X} (i : ι) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) (hp : ↑(chartAt ℂ x).symm z ∈ (Data.chart i).source) : Data.rawCoeffAt x z = (starRingEnd ℂ) (deriv (↑(Data.chart i) ∘ ↑(chartAt ℂ x).symm) z) * Data.coeff i (↑(Data.chart i) (↑(chartAt ℂ x).symm z))

Master computation: in the preferred chart at x, at a target point z whose base point lies in the i-th data chart, the raw coefficient is the i-th coefficient transported by the conjugated transition derivative — independent of the internally chosen index.

theorem RS.Form01CoeffData.contDiffOn_rawCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x : X) : ContDiffOn ℝ (↑⊤) (Data.rawCoeffAt x) (chartAt ℂ x).target

The preferred-chart coefficient functions of Data.rawCoeffAt are real-smooth on chart targets.

theorem RS.Form01CoeffData.rawCoeffAt_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x y : X) {z : ℂ} (hz : z ∈ ↑(chartAt ℂ y) '' ((chartAt ℂ x).source ∩ (chartAt ℂ y).source)) : Data.rawCoeffAt y z = (starRingEnd ℂ) (deriv (↑(chartAt ℂ x) ∘ ↑(chartAt ℂ y).symm) z) * Data.rawCoeffAt x (↑(chartAt ℂ x) (↑(chartAt ℂ y).symm z))

The conj-transition rule for Data.rawCoeffAt between any two PREFERRED charts (not just data charts): the compat field of the assembled Form01.

noncomputable def RS.Form01.ofCoeffs {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) : Form01 X

A (0,1)-form assembled from compatible chart-coefficient data (transcription of the CC1 Form1.ofCoeffs constructor for the Form01 structure).

Equations

• RS.Form01.ofCoeffs Data = { coeffAt := Data.rawCoeffAt, coeffAt_zero_off := ⋯, contDiffOn_coeffAt := ⋯, compat := ⋯ }

@[simp]

theorem RS.Form01.coeffAt_ofCoeffs_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) (x : X) (z : ℂ) : (ofCoeffs Data).coeffAt x z = Data.rawCoeffAt x z

theorem RS.Form01.coeffAt_ofCoeffs {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (Data : Form01CoeffData X ι) {x : X} {i : ι} (hx : x ∈ (Data.chart i).source) : (ofCoeffs Data).coeffAt x (↑(chartAt ℂ x) x) = (starRingEnd ℂ) (deriv (↑(Data.chart i) ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)) * Data.coeff i (↑(Data.chart i) x)

The preferred-chart coefficient of Form01.ofCoeffs Data at the chart center of a point of the i-th data chart's source, via the conjugated transition derivative — the shape GlueForm01.lean consumes.