20.7. CanonicalForms.MeromorphicOneFormSystem🔗

Jacobians.CanonicalForms.MeromorphicOneFormSystem — source

FormFiber

The cotangent fibre at x, the codomain of a 1-form section (matches HolomorphicOneForms).

abbrev FormFiber (X : Type*) [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) : Type _

formCoeff

The coordinate coefficient of a 1-form section σ in the canonical chart at x, read exactly as Montel.localRep: σ applied at (chart x).symm z to the unit coordinate tangent transported from the model space. Near x, σ = formCoeff σ x (z) · dz in z = chartAt ℂ x. For a *holomorphic* form this is Montel.localRep composed with chart.symm (= FormCoeff.coeffAt), hence analytic.

noncomputable def formCoeff (σ : ∀ x, FormFiber X x) (x : X) : ℂ → ℂ

IsMeromorphicOneForm

A section of the cotangent bundle is a meromorphic 1-form if its coordinate coefficient is MeromorphicAt at the chart image of every point — the 1-form analog of IsMeromorphic.

def IsMeromorphicOneForm (σ : ∀ x, FormFiber X x) : Prop

MeromorphicOneForm

The type of meromorphic 1-forms on X — the 1-form analog of MeromorphicFunction.

structure MeromorphicOneForm (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] : Type _ where

ext

Two meromorphic 1-forms are equal iff their underlying sections agree (the meromorphy field is a Prop).

@[ext] theorem ext {α β : MeromorphicOneForm X} (h : α.toFun = β.toFun) : α = β

toFun_injective

theorem toFun_injective :
    Function.Injective (MeromorphicOneForm.toFun : MeromorphicOneForm X → ∀ x, FormFiber X x)

formCoeff_add

formCoeff is additive in the section.

theorem formCoeff_add {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (σ τ : ∀ x, FormFiber X x) (x : X) :
    formCoeff (σ + τ) x = formCoeff σ x + formCoeff τ x

formCoeff_neg

formCoeff negates with the section.

theorem formCoeff_neg {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (σ : ∀ x, FormFiber X x) (x : X) :
    formCoeff (-σ) x = -formCoeff σ x

formCoeff_smul

formCoeff is ℂ-homogeneous in the section.

theorem formCoeff_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (c : ℂ) (σ : ∀ x, FormFiber X x) (x : X) :
    formCoeff (c • σ) x = c • formCoeff σ x

IsMeromorphicOneForm.add

theorem IsMeromorphicOneForm.add {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {σ τ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) (hτ : IsMeromorphicOneForm τ) :
    IsMeromorphicOneForm (σ + τ)

IsMeromorphicOneForm.neg

theorem IsMeromorphicOneForm.neg {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {σ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) :
    IsMeromorphicOneForm (-σ)

IsMeromorphicOneForm.sub

theorem IsMeromorphicOneForm.sub {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {σ τ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) (hτ : IsMeromorphicOneForm τ) :
    IsMeromorphicOneForm (σ - τ)

IsMeromorphicOneForm.const_smul

theorem IsMeromorphicOneForm.const_smul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (c : ℂ) {σ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) : IsMeromorphicOneForm (c • σ)

IsMeromorphicOneForm.zero

theorem IsMeromorphicOneForm.zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] :
    IsMeromorphicOneForm (0 : ∀ x, FormFiber X x)

IsMeromorphicOneForm.nsmul

theorem IsMeromorphicOneForm.nsmul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (n : ℕ) {σ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) : IsMeromorphicOneForm (n • σ)

IsMeromorphicOneForm.zsmul

theorem IsMeromorphicOneForm.zsmul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (n : ℤ) {σ : ∀ x, FormFiber X x}
    (hσ : IsMeromorphicOneForm σ) : IsMeromorphicOneForm (n • σ)

sub_toFun

@[simp] theorem sub_toFun (α β : MeromorphicOneForm X) :
    (α - β).toFun = α.toFun - β.toFun

toFunHom

The underlying-section homomorphism, used to transport the Module structure.

def toFunHom : MeromorphicOneForm X →+ (∀ x, FormFiber X x) where

formOrderW

The order of a meromorphic 1-form α at x, in WithTop ℤ: the meromorphicOrderAt of its coordinate coefficient in the canonical chart. It is ⊤ exactly when the form's coefficient vanishes in a punctured neighbourhood (so the zero form lies in every Ω_D). Chart-independent: under a holomorphic coordinate change the coefficient is multiplied by the non-vanishing Jacobian, which does not change meromorphicOrderAt. The 1-form analog of MeromorphicFunction.orderW.

noncomputable def formOrderW (α : MeromorphicOneForm X) (x : X) : WithTop ℤ

formOrderW_zero

theorem formOrderW_zero (x : X) : (0 : MeromorphicOneForm X).formOrderW x = ⊤

formOrderW_const_smul

Scaling a meromorphic 1-form by a nonzero constant does not change its order.

theorem formOrderW_const_smul {c : ℂ} (hc : c ≠ 0) (α : MeromorphicOneForm X) (x : X) :
    (c • α).formOrderW x = α.formOrderW x

min_formOrderW_le_add

The order of a sum is at least the min of the orders (mirror of meromorphicOrderAt_add), using formCoeff (α + β) = formCoeff α + formCoeff β.

theorem min_formOrderW_le_add (α β : MeromorphicOneForm X) (x : X) :
    min (α.formOrderW x) (β.formOrderW x) ≤ (α + β).formOrderW x

omegaD

The meromorphic-1-form linear system Ω_D (Forster's Ω_D): global meromorphic 1-forms α with div α ≥ −D, phrased on the WithTop ℤ order formOrderW (so the zero form is automatically a member). A Submodule ℂ of MeromorphicOneForm X — the 1-form analog of linearSystem D.

noncomputable def omegaD (D : Divisor X) : Submodule ℂ (MeromorphicOneForm X) where

formGermZeroSubmodule

Germ-zero "junk" 1-forms. The section toFun carries removable-singularity junk: a meromorphic 1-form whose coefficient germ is 0 everywhere can still be a nonzero element of MeromorphicOneForm X, and such forms lie in EVERY Ω_D. Quotienting them out makes omegaDim the genuine finite dimension — exactly the germZeroSubmodule fix for functions.

noncomputable def formGermZeroSubmodule : Submodule ℂ (MeromorphicOneForm X) where

omegaDim

omegaDim D = dim_ℂ (Ω_D ⧸ germ-zero junk) (Forster's dim H⁰(X, Ω_D)): the genuine dimension of the meromorphic-1-form linear system, with the toFun-junk quotiented out. The 1-form analog of lDim.

noncomputable def omegaDim (D : Divisor X) : ℕ

omegaDModule

The junk-free meromorphic-1-form module Ω_D (= H⁰(X, Ω_D)). By definition omegaDim D = finrank ℂ (omegaDModule D).

abbrev omegaDModule (D : Divisor X) : Type _

omegaDim_eq_finrank

theorem omegaDim_eq_finrank (D : Divisor X) :
    omegaDim (X := X) D = finrank ℂ (omegaDModule (X := X) D)

meroFormSMul

Multiplication of a meromorphic 1-form by a meromorphic function. (f · α)(x) := f(x) • α(x) (scalar-mult the covector). Meromorphic because its chart coefficient is the product (f.toFun ∘ chart⁻¹) · formCoeff α.

noncomputable def meroFormSMul (f : MeromorphicFunction X) (α : MeromorphicOneForm X) :
    MeromorphicOneForm X where

meroFormSMul_toFun

@[simp] theorem meroFormSMul_toFun (f : MeromorphicFunction X) (α : MeromorphicOneForm X) (x : X) :
    (meroFormSMul f α).toFun x = f.toFun x • α.toFun x

formCoeff_meroFormSMul

The chart coefficient of f · α is (f ∘ chart⁻¹) · formCoeff α.

theorem formCoeff_meroFormSMul (f : MeromorphicFunction X) (α : MeromorphicOneForm X) (x : X) :
    formCoeff (meroFormSMul f α).toFun x
      = (f.toFun ∘ (chartAt ℂ x).symm) * formCoeff α.toFun x

formOrderW_meroFormSMul

Order additivity (Forster 17.4): formOrderW (f · α) x = orderW f x + formOrderW α x.

theorem formOrderW_meroFormSMul (f : MeromorphicFunction X) (α : MeromorphicOneForm X) (x : X) :
    (meroFormSMul f α).formOrderW x = f.orderW x + α.formOrderW x

holToSection

The underlying section of a holomorphic 1-form, as a bare cotangent-bundle section. (Forgets smoothness; HolomorphicOneForms X = ContMDiffSection … coerces to its toFun.)

noncomputable def holToSection (α : HolomorphicOneForms X) : ∀ x, FormFiber X x

formCoeff_holToSection

The coordinate coefficient of a holomorphic form (via holToSection) is exactly the Montel / FormCoeff.coeffAt coefficient.

theorem formCoeff_holToSection (α : HolomorphicOneForms X) (x : X) :
    formCoeff (holToSection α) x = coeffAt α x

isMeromorphicOneForm_holToSection

A holomorphic 1-form is a meromorphic 1-form: its coordinate coefficient is analytic on the chart target (coeffAt_analyticOn), hence meromorphic at every chart image.

theorem isMeromorphicOneForm_holToSection (α : HolomorphicOneForms X) :
    IsMeromorphicOneForm (holToSection α)

holToMero

A holomorphic 1-form as a MeromorphicOneForm.

noncomputable def holToMero (α : HolomorphicOneForms X) : MeromorphicOneForm X

holToMero_toFun

@[simp] theorem holToMero_toFun (α : HolomorphicOneForms X) :
    (holToMero α).toFun = α.toFun

holToMero_mem_omegaD_zero

Ω_0 contains every holomorphic 1-form — the order of a holomorphic form is ≥ 0 everywhere (AnalyticAt.meromorphicOrderAt_nonneg).

theorem holToMero_mem_omegaD_zero (α : HolomorphicOneForms X) :
    holToMero α ∈ omegaD (X := X) 0

holToMero_eq_zero_of_germZero

A holomorphic form that is germ-zero everywhere is the zero form. At each a, the chart coefficient coeffAt α a is analytic and (by formOrderW = ⊤) vanishes on a punctured neighbourhood of chart a a, hence vanishes there too; so localRep α a a = 0 for all a, whence α = 0 (contrapositive of exists_localRep_self_ne_zero).

theorem holToMero_eq_zero_of_germZero (α : HolomorphicOneForms X)
    (h : ∀ x, (holToMero α).formOrderW x = ⊤) : α = 0

holInOmega0

The image of a holomorphic form under holToMeroₗ, as a member of the linear system Ω_0.

noncomputable def holInOmega0 (α : HolomorphicOneForms X) : ↥(omegaD (X := X) 0)

holToOmega0Module

The holomorphic-to-Ω_0-module linear map HolomorphicOneForms X → omegaDModule 0: holToMeroₗ landed in Ω_0, then projected to the junk-free quotient. The structure map of Forster §17.4 at D = 0; its injectivity gives genus X ≤ omegaDim 0.

noncomputable def holToOmega0Module : HolomorphicOneForms X →ₗ[ℂ] omegaDModule (X := X) 0 where

holToOmega0Module_injective

holToOmega0Module is injective: if [holToMero α] = [holToMero β] in the junk-free quotient, then holToMero (α − β) is germ-zero everywhere, so α − β = 0 by holToMero_eq_zero_of_germZero.

theorem holToOmega0Module_injective :
    Function.Injective (holToOmega0Module (X := X))

genus_le_omegaDim_zero

Soundness lower bound: genus X ≤ omegaDim 0 (when Ω_0 is finite-dimensional). The genus-dimensional holomorphic forms inject into omegaDModule 0 (holToOmega0Module_injective), so finrank is monotone: genus X ≤ omegaDim 0. This confirms Ω_0 is the genuine Forster §17.4 object H⁰(X, Ω), not a junk space. (Finite-dimensionality of Ω_0 is itself part of §17.4 — Ω_0 ≅ HolomorphicOneForms, which is finite-dim; the bound is stated under that hypothesis so it is unconditionally TRUE, avoiding the finrank = 0 junk value of an a-priori unbounded quotient.)

theorem genus_le_omegaDim_zero [FiniteDimensional ℂ (omegaDModule (X := X) 0)] :
    genus X ≤ omegaDim (X := X) 0

omegaDim_zero_eq_genus_of_le

Ω_0 ≅ HolomorphicOneForms (the full §17.4 soundness equality), conditional on the reverse bound. omegaDim 0 = genus X follows from the proven lower bound genus_le_omegaDim_zero together with the reverse omegaDim 0 ≤ genus X. The reverse is the *removable-singularity* direction: an order-≥ 0 meromorphic 1-form has an analytic chart coefficient, so (modulo the germ-junk it is quotiented by) it is a genuine holomorphic form — the analytic-to-smooth section bridge. This is the one isolated analytic input to the equality; the injection and the lower bound are proven above.

theorem omegaDim_zero_eq_genus_of_le [FiniteDimensional ℂ (omegaDModule (X := X) 0)]
    (hle : omegaDim (X := X) 0 ≤ genus X) :
    omegaDim (X := X) 0 = genus X