MFormData X: raw chart-coefficient families for meromorphic 1-forms (D1–D3, data layer)

Unit: canonical-forms (docs/design/canonical-forms.md §2 D1–D3, §4.1). Blueprint: "Meromorphic 1-form systems and the canonical divisor K."

MFormData X is the RAW DATA CARRIER for meromorphic 1-forms: the meromorphic analogue of Form1's chart-coefficient API (Jacobian/Forms/Coeffs.lean) and of dbar's Form01 (Jacobian/Dbar/Form01.lean) — a chartAt-indexed family of coefficient functions, junk-zero off the chart target, MeromorphicOn the target (mathlib's unconditional generalization of Form01's ContDiffOn/Form1's AnalyticOnNhd, allowing poles), related on chart overlaps by the CC1-style transition rule coeffAt y z = deriv (chartAt x ∘ (chartAt y).symm) z * coeffAt x (...) — no conjugate (a meromorphic 1-form is still type (1,0), unlike Form01's (0,1)-conjugate rule).

Raw equality on MFormData is too fine (meromorphic coefficient functions carry junk values at poles, so "ord = ⊤ everywhere" does not pin the raw values): the ACTUAL meromorphic-1-form type is the quotient RS.MForm X by codiscrete/germ agreement (Quotient.lean, the same CC3 pattern as ℳ X := MeroGermOn X univ). Everything in this file is the foundation the quotient descends from.

Main declarations:

• RS.MFormData X — the structure (D1); RS.MFormData.ext, Zero/Add/Neg/Sub/SMul ℂ/ AddCommGroup/Module ℂ instances (D2), pointwise on coeffAt.
• RS.MFormCoeffData X ι / RS.MFormData.ofCoeffs (D3) — the arbitrary-chart-family constructor, mirroring Form1CoeffData/Form1.ofCoeffs (Jacobian/Forms/OfCoeffs.lean) with AnalyticOnNhd ↦ MeromorphicOn; not used by MFormData.d/dlog (built directly against chartAt in Differential.lean), offered for future covering-family constructions (e.g. laurent-tails).

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

A meromorphic 1-form on X: the meromorphic analogue of Form1's coeffIn API and Form01's chart-family structure, generalized to allow poles (D1).

• 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
• meromorphicOn_coeffAt (x : X) : MeromorphicOn (self.coeffAt x) (chartAt ℂ x).target
• compat (x y : X) (z : ℂ) : z ∈ ↑(chartAt ℂ y) '' ((chartAt ℂ x).source ∩ (chartAt ℂ y).source) → self.coeffAt y z = deriv (↑(chartAt ℂ x) ∘ ↑(chartAt ℂ y).symm) z * self.coeffAt x (↑(chartAt ℂ x) (↑(chartAt ℂ y).symm z))

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

A meromorphic 1-form is determined by its preferred-chart coefficients on chart targets.

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• RS.MFormData.instNeg = { neg := fun (θ : RS.MFormData X) => { coeffAt := fun (x : X) (z : ℂ) => -θ.coeffAt x z, coeffAt_zero_off := ⋯, meromorphicOn_coeffAt := ⋯, compat := ⋯ } }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

D3: constructing MFormData from arbitrary compatible chart data

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

Compatible meromorphic coefficient data for a meromorphic 1-form, over a covering family of ω-maximal-atlas charts (mirrors Form1CoeffData, MeromorphicOn in place of AnalyticOnNhd).

• 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.

• meromorphicOn (i : ι) : MeromorphicOn (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.MFormCoeffData.idx {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : MFormCoeffData X ι) (x : X) : ι

A chosen chart index for each point.

Equations

• D.idx x = ⋯.choose

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

noncomputable def RS.MFormCoeffData.rawCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : MFormCoeffData X ι) (e' : OpenPartialHomeomorph X ℂ) (z : ℂ) : ℂ

The coefficient of the assembled family, read through an arbitrary maximal-atlas chart e', using the per-point chosen index (mirrors Form1CoeffData.toSection, without the bundle layer: MFormData has no covector-bundle backing, so this formula IS the assembled coefficient directly).

Equations

• D.rawCoeffAt e' z = deriv (↑(D.chart (D.idx (↑e'.symm z))) ∘ ↑e'.symm) z * D.coeff (D.idx (↑e'.symm z)) (↑(D.chart (D.idx (↑e'.symm z))) (↑e'.symm z))

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

Master computation: rawCoeffAt read through any maximal-atlas chart e', at a point whose base point lies in the i-th chart, equals the i-th coefficient transported by the transition derivative — independent of the internal idx choice, by compat.

theorem RS.MFormCoeffData.meromorphicAt_rawCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : MFormCoeffData X ι) (e' : OpenPartialHomeomorph X ℂ) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {z₀ : ℂ} (hz₀ : z₀ ∈ e'.target) : MeromorphicAt (D.rawCoeffAt e') z₀

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

Assemble an MFormData from compatible chart-coefficient data (D3, mirrors Form1.ofCoeffs).

Equations

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

theorem RS.MFormData.coeffAt_ofCoeffs {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (D : MFormCoeffData X ι) {x : X} {i : ι} (_hx : x ∈ (D.chart i).source) {z : ℂ} (hz : z ∈ ↑(chartAt ℂ x) '' ((D.chart i).source ∩ (chartAt ℂ x).source)) : (ofCoeffs D).coeffAt x z = deriv (↑(D.chart i) ∘ ↑(chartAt ℂ x).symm) z * D.coeff i (↑(D.chart i) (↑(chartAt ℂ x).symm z))

The coefficient of MFormData.ofCoeffs D in the i-th chart of the data, read at a point of the preferred chart at x, is the given coefficient transported by the transition derivative (mirrors Form1.coeffAt_ofCoeffs).