MForm X: meromorphic 1-forms as germ classes of chart-coefficient families (D1/D2/D4–D6)

Unit: canonical-forms (docs/design/canonical-forms.md, representational revision). This file is the CC3-pattern fix for the raw-representation flaw documented in the previous unit root: raw MFormData equality is too fine (meromorphic coefficients carry junk at poles, so "ord = ⊤ everywhere" does NOT force raw equality with 0). Exactly as ℳ X quotients raw meromorphic functions by codiscrete agreement (Jacobian/Meromorphic/GermSpace.lean), we set

• MFormData.Eqv θ η := ∀ x, θ.coeffAt x =ᶠ[𝓝[≠] (chartAt ℂ x x)] η.coeffAt x — germ agreement at every preferred-chart center. (By compat-transport this is equivalent to codiscrete agreement on every chart target; the center-germ form is chosen because every reading map of the unit — ord, resAt, laurentCoeffAt, divisor — is a germ-at-the-center functional, so descent is a one-line congruence.)
• MForm X := Quotient of MFormData X by Eqv, with AddCommGroup/Module ℂ descended pointwise from the raw instances.
• MForm.ord/resAt/laurentCoeffAt/divisor/degree: the D4/D6 exports, lifted.
• D5, the global zero-dichotomy MForm.eq_zero_or_forall_ord_ne_top: on the quotient this is the clopen argument of Jacobian/Meromorphic/CodiscreteBridge.lean run on {x | ord = ⊤} (open by eventually_ord_eq_top, closed because its complement is open by eventually_ord_eq_zero), and the S = univ ⇒ θ = 0 step — FALSE for raw families — is now the literal definition of the quotient relation via ord_eq_top_iff. Corollary: MForm.ord_ne_top.

def RS.MFormData.Eqv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MFormData X) : Prop

Codiscrete/germ agreement of raw chart-coefficient families: the preferred-chart coefficients agree on a punctured neighborhood of every chart center (CC3 pattern; see the module docstring for why this is the right granularity).

Equations

• θ.Eqv η = ∀ (x : X), θ.coeffAt x =ᶠ[nhdsWithin (↑(chartAt ℂ x) x) {↑(chartAt ℂ x) x}ᶜ] η.coeffAt x

theorem RS.MFormData.eqv_refl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) : θ.Eqv θ

theorem RS.MFormData.eqv_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ η : MFormData X} (h : θ.Eqv η) : η.Eqv θ

theorem RS.MFormData.eqv_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ η ζ : MFormData X} (h₁ : θ.Eqv η) (h₂ : η.Eqv ζ) : θ.Eqv ζ

@[instance_reducible]

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

Equations

• RS.MFormData.instSetoid = { r := RS.MFormData.Eqv, iseqv := ⋯ }

def RS.MForm (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Type u_1

D1 (revised): a meromorphic 1-form on X — the quotient of raw chart-coefficient families (MFormData X) by codiscrete/germ agreement, the same CC3 quotient pattern as ℳ X.

Equations

• RS.MForm X = Quotient RS.MFormData.instSetoid

def RS.MForm.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) : MForm X

The class of a raw chart-coefficient family.

Equations

• RS.MForm.mk θ = ⟦θ⟧

theorem RS.MForm.exists_rep {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ : MForm X) : ∃ (θ : MFormData X), mk θ = Θ

theorem RS.MForm.ind {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {motive : MForm X → Prop} (h : ∀ (θ : MFormData X), motive (mk θ)) (Θ : MForm X) : motive Θ

theorem RS.MForm.sound {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ η : MFormData X} (h : θ.Eqv η) : mk θ = mk η

theorem RS.MForm.mk_eq_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ η : MFormData X} : mk θ = mk η ↔ θ.Eqv η

ℂ-algebra structure, descended pointwise

@[instance_reducible]

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

Equations

• RS.MForm.instZero = { zero := RS.MForm.mk 0 }

@[instance_reducible]

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

Equations

• RS.MForm.instAdd = { add := Quotient.map₂ (fun (x1 x2 : RS.MFormData X) => x1 + x2) ⋯ }

@[instance_reducible]

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

Equations

• RS.MForm.instNeg = { neg := Quotient.map (fun (x : RS.MFormData X) => -x) ⋯ }

@[instance_reducible]

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

Equations

• RS.MForm.instSub = { sub := Quotient.map₂ (fun (x1 x2 : RS.MFormData X) => x1 - x2) ⋯ }

@[instance_reducible]

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

Equations

• RS.MForm.instSMulComplex = { smul := fun (c : ℂ) => Quotient.map (fun (x : RS.MFormData X) => c • x) ⋯ }

@[simp]

theorem RS.MForm.mk_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : mk 0 = 0

@[simp]

theorem RS.MForm.mk_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MFormData X) : mk θ + mk η = mk (θ + η)

@[simp]

theorem RS.MForm.mk_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) : -mk θ = mk (-θ)

@[simp]

theorem RS.MForm.mk_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MFormData X) : mk θ - mk η = mk (θ - η)

@[simp]

theorem RS.MForm.mk_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (θ : MFormData X) : c • mk θ = mk (c • θ)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

D3 on classes: assemble a meromorphic 1-form from compatible covering-chart-family data (MFormCoeffData, mirrors Form1CoeffData); the class of the raw assembly.

Equations

• RS.MForm.ofCoeffs D = RS.MForm.mk (RS.MFormData.ofCoeffs D)

ord, resAt, laurentCoeffAt (D4), lifted

noncomputable def RS.MForm.ord {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ : MForm X) (x : X) : WithTop ℤ

D4: the order of a meromorphic 1-form at x (read via the preferred chart at x; descends because meromorphicOrderAt is a germ functional).

Equations

• Θ.ord x = Quotient.liftOn Θ (fun (θ : RS.MFormData X) => θ.ord x) ⋯

@[simp]

theorem RS.MForm.ord_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (x : X) : (mk θ).ord x = θ.ord x

noncomputable def RS.MForm.resAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ : MForm X) (x : X) : ℂ

D4: the residue of a meromorphic 1-form at x.

Equations

• Θ.resAt x = Quotient.liftOn Θ (fun (θ : RS.MFormData X) => θ.resAt x) ⋯

@[simp]

theorem RS.MForm.resAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (x : X) : (mk θ).resAt x = θ.resAt x

noncomputable def RS.MForm.laurentCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ : MForm X) (x : X) (k : ℤ) : ℂ

The k-th Laurent coefficient of a meromorphic 1-form at x, read in the preferred chart (consumed by MLFormData.Realizes, D13).

Equations

• Θ.laurentCoeffAt x k = Quotient.liftOn Θ (fun (θ : RS.MFormData X) => RS.laurentCoeffAt (θ.coeffAt x) (↑(chartAt ℂ x) x) k) ⋯

@[simp]

theorem RS.MForm.laurentCoeffAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (x : X) (k : ℤ) : (mk θ).laurentCoeffAt x k = RS.laurentCoeffAt (θ.coeffAt x) (↑(chartAt ℂ x) x) k

theorem RS.MForm.resAt_eq_laurentCoeffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ : MForm X) (x : X) : Θ.resAt x = Θ.laurentCoeffAt x (-1)

@[simp]

theorem RS.MForm.ord_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : ord 0 x = ⊤

Order propagation and the divisor (D6), lifted

theorem RS.MForm.eventually_ord_eq_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] {Θ : MForm X} {x : X} (h : Θ.ord x = ⊤) : ∀ᶠ (y : X) in nhds x, Θ.ord y = ⊤

theorem RS.MForm.eventually_ord_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Θ : MForm X} {x : X} (h : Θ.ord x ≠ ⊤) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, Θ.ord y = 0

noncomputable def RS.MForm.divisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (Θ : MForm X) : Divisor X

D6: the divisor of a meromorphic 1-form (lifted from MFormData.divisor; well-defined since ord is).

Equations

• Θ.divisor = Quotient.liftOn Θ RS.MFormData.divisor ⋯

@[simp]

theorem RS.MForm.divisor_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (θ : MFormData X) : (mk θ).divisor = θ.divisor

@[simp]

theorem RS.MForm.divisor_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] (Θ : MForm X) (x : X) : Θ.divisor x = (Θ.ord x).untop₀

noncomputable def RS.MForm.degree {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [CompactSpace X] (Θ : MForm X) : ℤ

D6: the degree of the divisor.

Equations

• Θ.degree = Function.locallyFinsuppWithin.degree Θ.divisor

@[simp]

theorem RS.MForm.divisor_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] : divisor 0 = 0

D5: the global zero-dichotomy

The step that is FALSE for raw families — "ord = ⊤ everywhere forces the form to be zero" — is the literal definition of the quotient relation. The clopen skeleton is MeromorphicOnX.eventuallyEq_zero_or_forall_ordAtX_ne_top's (Jacobian/Meromorphic/CodiscreteBridge.lean); closedness of {ord = ⊤} is here even easier: its complement is open directly by eventually_ord_eq_zero.

theorem RS.MForm.eq_zero_or_forall_ord_ne_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] (Θ : MForm X) : Θ = 0 ∨ ∀ (x : X), Θ.ord x ≠ ⊤

D5: on a connected surface, a meromorphic 1-form is zero, or its order is finite everywhere.

theorem RS.MForm.ord_ne_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ : MForm X} (h : Θ ≠ 0) (x : X) : Θ.ord x ≠ ⊤

A nonzero meromorphic 1-form has finite order everywhere (D5 corollary; the input D8/D10/D11 consume).

theorem RS.MForm.eq_zero_iff_forall_ord_eq_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ : MForm X} : Θ = 0 ↔ ∀ (x : X), Θ.ord x = ⊤

The zero class is characterized by ord = ⊤ everywhere (junk-free, unlike the raw layer).