Ω(D), the L(D+K) bridge, holomorphic forms, and ML form data (D11/D12/D13)

Unit: canonical-forms (docs/design/canonical-forms.md §2 D11–D13, §4.5, proof plan §5 P6).

• MForm.OmegaSpace D : Submodule ℂ (MForm X) (Miranda's L⁽¹⁾(D)/Forster's Γ(X,Ω_D)): meromorphic 1-forms with -D ≤ order everywhere, defined order-wise on the QUOTIENT (mirrors LinSys's primary definition); MForm.i D (index of speciality). Instance-free (the order-wise carrier needs no topology), strictly more general than the design's listing.
• D11 ΩIsoLinSys : OmegaSpace D ≃ₗ[ℂ] LinSys (D + canonicalDivisorOf θ₀) (Forster 17.4 / Miranda Ω_D ≅ O_{D+K}), via D8's one-dimensionality (LinearEquiv.ofBijective of h ↦ h • θ₀, membership transported by the pointwise smul_mem_omegaSpace_iff dictionary); i_eq_l_add_canonicalDivisorOf.
• D12 holomorphicMFormsEquiv : Form1 X ≃ₗ[ℂ] OmegaSpace (0 : Divisor X): forward is Form1.toMForm (analytic coefficients have 0 ≤ ord); injectivity is continuity at chart centers; surjectivity REPAIRS a representative via the mero unit's canonical holoRepr pattern — for a class with 0 ≤ ord everywhere, the chart-local coefficient germs MeroGermOn.mk (θ.coeffAt x ∘ chartAt ℂ x) have honest analytic holoReprs (ord_eq_meromorphicOrderAt_of_mem_source bridges center-orders to target-orders), whose chart reads assemble into a Form1CoeffData and a genuine Form1 via Form1.ofCoeffs. Needs NO topological instances (the design's [T1][T2][Compact] are unnecessary here). Corollary genus_eq_finrank_omegaSpace_zero (the cech-h1-genus/riemann-roch export).
• D13 MLFormData/Realizes (against MForm.laurentCoeffAt, on classes)/totalRes/ Realizes.resAt_eq: a thin X-level wrapper around residue-calculus's PrincipalPartData.

Order arithmetic (junk-robust; data layer, then descended)

theorem RS.MFormData.ord_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MFormData X) (x : X) : min (θ.ord x) (η.ord x) ≤ (θ + η).ord x

theorem RS.MFormData.ord_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {c : ℂ} (hc : c ≠ 0) (θ : MFormData X) (x : X) : (c • θ).ord x = θ.ord x

theorem RS.MForm.ord_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ H : MForm X) (x : X) : min (Θ.ord x) (H.ord x) ≤ (Θ + H).ord x

theorem RS.MForm.ord_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {c : ℂ} (hc : c ≠ 0) (Θ : MForm X) (x : X) : (c • Θ).ord x = Θ.ord x

MForm.OmegaSpace (D11)

def RS.MForm.OmegaSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) : Submodule ℂ (MForm X)

Meromorphic 1-forms with divisor ≥ -D (Miranda's L⁽¹⁾(D)/Forster's Γ(X, Ω_D)), defined order-wise on the quotient (mirrors LinSys's own primary definition).

Equations

• RS.MForm.OmegaSpace D = { carrier := {Θ : RS.MForm X | ∀ (x : X), ↑(-D x) ≤ Θ.ord x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RS.MForm.mem_omegaSpace_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D : Divisor X} {Θ : MForm X} : Θ ∈ OmegaSpace D ↔ ∀ (x : X), ↑(-D x) ≤ Θ.ord x

noncomputable def RS.MForm.i {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : Divisor X) : ℕ

Index of speciality: dim Ω(D).

Equations

• RS.MForm.i D = Module.finrank ℂ ↥(RS.MForm.OmegaSpace D)

D11: the Ω(D) ≅ L(D+K) bridge

theorem RS.MForm.smul_mem_omegaSpace_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) {h : Mero X} {D : Divisor X} : h • Θ₀ ∈ OmegaSpace D ↔ h ∈ LinSys (D + canonicalDivisorOf Θ₀)

The pointwise membership dictionary (Forster 17.4's computation): h • θ₀ has order ≥ -D everywhere iff h ∈ L(D + K), K := canonicalDivisorOf θ₀.

noncomputable def RS.linSysToOmega {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) (D : Divisor X) : ↥(LinSys (D + canonicalDivisorOf Θ₀)) →ₗ[ℂ] ↥(MForm.OmegaSpace D)

The forward leg of the D11 bridge: multiplication by θ₀, L(D+K) →ₗ Ω(D).

Equations

• RS.linSysToOmega h₀ D = { toFun := fun (h : ↥(RS.LinSys (D + RS.canonicalDivisorOf Θ₀))) => ⟨↑h • Θ₀, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RS.ΩIsoLinSys {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) (D : Divisor X) : ↥(MForm.OmegaSpace D) ≃ₗ[ℂ] ↥(LinSys (D + canonicalDivisorOf Θ₀))

D11 (Forster 17.4 / Miranda Ω_D ≅ O_{D+K}): multiplication by a fixed nonzero reference θ₀ (with K := canonicalDivisorOf θ₀) is a linear equivalence Ω(D) ≅ L(D+K).

Equations

• RS.ΩIsoLinSys h₀ D = (LinearEquiv.ofBijective (RS.linSysToOmega h₀ D) ⋯).symm

theorem RS.i_eq_l_add_canonicalDivisorOf {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [T2Space X] [ConnectedSpace X] {Θ₀ : MForm X} (h₀ : Θ₀ ≠ 0) (D : Divisor X) : MForm.i D = l (D + canonicalDivisorOf Θ₀)

D11's dimension dictionary: i(D) = l(D + K).

D12: Form1 ≃ₗ Ω(0) (the holomorphic forms bridge)

noncomputable def RS.form1ToOmega {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Form1 X →ₗ[ℂ] ↥(MForm.OmegaSpace 0)

The forward leg of D12: a holomorphic 1-form as an element of Ω(0).

Equations

• RS.form1ToOmega = { toFun := fun (η : RS.Form1 X) => ⟨RS.MForm.ofForm1 η, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.form1ToOmega_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Function.Surjective ⇑form1ToOmega

D12 surjectivity: any class of 0 ≤ ord everywhere is ofForm1 of a genuine Form1 — the representative is REPAIRED chart-by-chart through the mero unit's canonical holoRepr.

noncomputable def RS.holomorphicMFormsEquiv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Form1 X ≃ₗ[ℂ] ↥(MForm.OmegaSpace 0)

D12: holomorphic 1-forms ARE the meromorphic 1-forms of nonnegative divisor. (No topological instances needed — strictly more general than the design's listing.)

Equations

• RS.holomorphicMFormsEquiv = LinearEquiv.ofBijective RS.form1ToOmega ⋯

theorem RS.genus_eq_finrank_omegaSpace_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : genus X = Module.finrank ℂ ↥(MForm.OmegaSpace 0)

The genus counts meromorphic 1-forms of nonnegative divisor (the cech-h1-genus/riemann-roch export; l(K) = g becomes a one-line corollary of this + i_eq_l_add_canonicalDivisorOf once Serre duality lands downstream).

MLFormData (D13, Forster §17.1–17.2)

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

A form-level Mittag-Leffler datum: at finitely many points of X, a principal part read in the preferred chart. A thin wrapper around residue-calculus's already-built PrincipalPartData.

• pts : Finset X

  The finite set of points carrying prescribed principal parts.

• data (x : X) : x ∈ self.pts → PrincipalPartData (chartAt ℂ x).target

  The principal part prescribed at each marked point, read in that point's chart.

def RS.MLFormData.Realizes {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (μ : MLFormData X) (Θ : MForm X) : Prop

μ realizes the principal parts of Θ at every point of μ.pts (read in each point's own preferred chart; stated on classes via the lifted MForm.laurentCoeffAt).

Equations

• μ.Realizes Θ = ∀ (x : X) (hx : x ∈ μ.pts), ∀ k < 0, Θ.laurentCoeffAt x k = ((μ.data x hx).coeff (↑(chartAt ℂ x) x)) k

noncomputable def RS.MLFormData.totalRes {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (μ : MLFormData X) : ℂ

The total residue prescribed by the datum.

Equations

• μ.totalRes = ∑ x ∈ μ.pts.attach, ((μ.data ↑x ⋯).coeff (↑(chartAt ℂ ↑x) ↑x)) (-1)

theorem RS.MLFormData.Realizes.resAt_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {μ : MLFormData X} {Θ : MForm X} (h : μ.Realizes Θ) {x : X} (hx : x ∈ μ.pts) : Θ.resAt x = ((μ.data x hx).coeff (↑(chartAt ℂ x) x)) (-1)