Constructing holomorphic 1-forms from coefficient data (CC1, design §2.3)

Unit: holomorphic-forms (docs/design/holomorphic-forms.md). RS.Form1CoeffData X ι packages a covering family of ω-maximal-atlas charts together with analytic coefficient functions on the chart targets satisfying the CC1 transition rule; RS.Form1.ofCoeffs assembles them into a holomorphic 1-form whose coeffIn in the i-th chart is the given i-th coefficient (RS.Form1.coeffIn_ofCoeffs).

The chart family is arbitrary (indexed by any ι), not just preferred charts: the finiteness argument (Jacobian/Forms/Finiteness.lean) instantiates it with charts restricted to shrunk cover sets, which stay in the maximal atlas.

Main declarations:

• RS.Form1CoeffData — the compatible-coefficient structure.
• RS.Form1CoeffData.coeffInFun_toSection — master computation: the raw coefficient of the assembled section in ANY maximal-atlas chart.
• RS.Form1.ofCoeffs, RS.Form1.coeffIn_ofCoeffs, RS.Form1.coeffAt_ofCoeffs.

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

Compatible analytic coefficient data for a holomorphic 1-form, over a covering family of ω-maximal-atlas charts: on each chart target an analytic coefficient function, related on overlaps by the CC1 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.

• analyticOnNhd (i : ι) : AnalyticOnNhd ℂ (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) = deriv (↑(self.chart i) ∘ ↑(self.chart j).symm) (↑(self.chart j) x) * self.coeff i (↑(self.chart i) x)

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

A chosen chart index for each point.

Equations

• D.idx x = ⋯.choose

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

noncomputable def RS.Form1CoeffData.toSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) (x : X) : TangentSpace (modelWithCornersSelf ℂ ℂ) x →L[ℂ] Bundle.Trivial X ℂ x

The underlying covector section: at x, the covector coeff · d(chart)ₓ read through the chosen chart (crossing the TangentSpace ↦ Bundle.Trivial defeq in the codomain).

Equations

• D.toSection x = D.coeff (D.idx x) (↑(D.chart (D.idx x)) x) • mfderiv% ↑(D.chart (D.idx x)) x

theorem RS.Form1CoeffData.evalC_toSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) (x : X) (w : ℂ) : evalC D.toSection x w = D.coeff (D.idx x) (↑(D.chart (D.idx x)) x) * tangentCoord ((mfderiv% ↑(D.chart (D.idx x)) x) w)

theorem RS.Form1CoeffData.coeffInFun_toSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) {e' : OpenPartialHomeomorph X ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (i : ι) {z : ℂ} (hz : z ∈ e'.target) (hp : ↑e'.symm z ∈ (D.chart i).source) : coeffInFun e' D.toSection z = deriv (↑(D.chart i) ∘ ↑e'.symm) z * D.coeff i (↑(D.chart i) (↑e'.symm z))

Master computation: in any maximal-atlas chart e', at a target point z whose base point lies in the i-th chart, the raw coefficient of D.toSection is the i-th coefficient transported by the transition derivative.

theorem RS.Form1CoeffData.analyticAt_coeffInFun_toSection {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) (x : X) : AnalyticAt ℂ (coeffInFun (chartAt ℂ x) D.toSection) (↑(chartAt ℂ x) x)

The preferred-chart coefficient functions of D.toSection are analytic (feeds the Form1.ofSectionAnalytic constructor).

noncomputable def RS.Form1.ofCoeffs {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) : Form1 X

A holomorphic 1-form assembled from compatible analytic coefficient data over a covering maximal-atlas chart family (CC1 constructor).

Equations

• RS.Form1.ofCoeffs D = RS.Form1.ofSectionAnalytic D.toSection ⋯

theorem RS.Form1.coeffIn_ofCoeffs {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : Form1CoeffData X ι) (i : ι) : Set.EqOn (coeffIn (D.chart i) (ofCoeffs D)) (D.coeff i) (D.chart i).target

The coefficients of Form1.ofCoeffs D in the i-th chart of the data are the given coefficients, on the whole chart target.

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

The preferred-chart coefficient of Form1.ofCoeffs D at a point of the i-th chart source, via the transition derivative (the form consumed by the finiteness argument).