11.5. Meromorphic.LinearSystem🔗

Jacobians.Meromorphic.LinearSystem — source

ext

Two meromorphic functions are equal iff their underlying maps agree (the meromorphy field is a Prop, hence proof-irrelevant).

@[ext] theorem ext {f g : MeromorphicFunction X} (h : f.toFun = g.toFun) : f = g

toFun_injective

theorem toFun_injective :
    Function.Injective (MeromorphicFunction.toFun : MeromorphicFunction X → (X → ℂ))

IsMeromorphic.add

theorem IsMeromorphic.add {f g : X → ℂ} (hf : IsMeromorphic X f) (hg : IsMeromorphic X g) :
    IsMeromorphic X (f + g)

IsMeromorphic.neg

theorem IsMeromorphic.neg {f : X → ℂ} (hf : IsMeromorphic X f) :
    IsMeromorphic X (-f)

IsMeromorphic.sub

theorem IsMeromorphic.sub {f g : X → ℂ} (hf : IsMeromorphic X f) (hg : IsMeromorphic X g) :
    IsMeromorphic X (f - g)

IsMeromorphic.const_smul

theorem IsMeromorphic.const_smul (c : ℂ) {f : X → ℂ} (hf : IsMeromorphic X f) :
    IsMeromorphic X (c • f)

IsMeromorphic.nsmul

theorem IsMeromorphic.nsmul (n : ℕ) {f : X → ℂ} (hf : IsMeromorphic X f) :
    IsMeromorphic X (n • f)

IsMeromorphic.zsmul

theorem IsMeromorphic.zsmul (n : ℤ) {f : X → ℂ} (hf : IsMeromorphic X f) :
    IsMeromorphic X (n • f)

add_toFun

@[simp] theorem add_toFun (f g : MeromorphicFunction X) :
    (f + g).toFun = f.toFun + g.toFun

sub_toFun

@[simp] theorem sub_toFun (f g : MeromorphicFunction X) :
    (f - g).toFun = f.toFun - g.toFun

smul_toFun

@[simp] theorem smul_toFun (c : ℂ) (f : MeromorphicFunction X) :
    (c • f).toFun = c • f.toFun

toFunHom

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

def toFunHom : MeromorphicFunction X →+ (X → ℂ) where

orderW

The order of f at x as WithTop ℤ — the meromorphic order *before* the untop₀ that defines orderAtPoint. It is ⊤ exactly when f vanishes in a punctured neighbourhood of x; phrasing L(D) on this order makes the zero function a member of every L(D) automatically.

noncomputable def orderW (f : MeromorphicFunction X) (x : X) : WithTop ℤ

orderW_zero

theorem orderW_zero (x : X) : (0 : MeromorphicFunction X).orderW x = ⊤

eventually_comp_chart_iff

The chart is a local homeomorphism near y, so an eventually-property of g on the punctured neighbourhood 𝓝[≠] y transfers to the chart-pulled-back function on 𝓝[≠] (chart y).

theorem eventually_comp_chart_iff (g : X → ℂ) (y : X) (P : ℂ → Prop) :
    (∀ᶠ w in 𝓝[≠] ((chartAt (H := ℂ) y) y), P ((g ∘ (chartAt (H := ℂ) y).symm) w))
      ↔ ∀ᶠ z in 𝓝[≠] y, P (g z)

orderW_eq_top_iff

orderW f y = ⊤ (the germ vanishes) iff f.toFun vanishes throughout a punctured neighbourhood of y (intrinsic — the chart drops out).

theorem orderW_eq_top_iff (f : MeromorphicFunction X) (y : X) :
    f.orderW y = ⊤ ↔ ∀ᶠ z in 𝓝[≠] y, f.toFun z = 0

orderW_ne_top_iff

orderW f y ≠ ⊤ (the germ is nonzero) iff f.toFun is eventually nonzero on a punctured neighbourhood of y.

theorem orderW_ne_top_iff (f : MeromorphicFunction X) (y : X) :
    f.orderW y ≠ ⊤ ↔ ∀ᶠ z in 𝓝[≠] y, f.toFun z ≠ 0

orderW_ne_top_of_exists

Faithfulness / identity theorem. If the germ of f is nonzero at even one point, it is nonzero (orderW ≠ ⊤) at *every* point. The set {y | orderW f y = ⊤} and its complement are both open (via the two intrinsic characterizations above), so on the connected X it is empty.

theorem orderW_ne_top_of_exists [T2Space X] [ConnectedSpace X] (f : MeromorphicFunction X)
    (h₀ : ∃ x₀, f.orderW x₀ ≠ ⊤) (x : X) : f.orderW x ≠ ⊤

linearSystem

The complete linear system L(D) = meromorphic functions with div f ≥ −D, phrased on the WithTop ℤ order (so the zero function, order ⊤, is automatically a member). A Submodule ℂ.

noncomputable def linearSystem (D : Divisor X) : Submodule ℂ (MeromorphicFunction X) where

germZeroSubmodule

Germ-zero "junk" functions. MeromorphicFunction.toFun carries removable-singularity junk (cf. the toSphere note): e.g. the indicator of a single point is a *nonzero* meromorphic function whose germ is 0 everywhere (orderW ≡ ⊤). Such functions lie in *every* L(D), and point-indicators are linearly independent, so the naive finrank ℂ (L(D)) is wrong (the space is infinite-dimensional, forcing finrank = 0 for all D, which makes RR false). We quotient them out so l(D) is the genuine, finite dimension.

noncomputable def germZeroSubmodule : Submodule ℂ (MeromorphicFunction X) where

lDim

l(D) = dim_ℂ (L(D) ⧸ germ-zero junk) (Forster's h⁰(X, O_D)) — the genuine dimension of the linear system, with the toFun-junk quotiented out.

noncomputable def lDim (D : Divisor X) : ℕ

germ_eq_const_of_mem_linearSystem_zero

A function in L(0) is germ-constant (Liouville). With no pole (orderW ≥ 0), the limit-repair holoRepr is holomorphic (mdifferentiable_holoRepr), hence constant on the compact connected X (exists_eq_const_of_compactSpace); off-center the chart pullback equals that constant, so f.toFun agrees with it on every punctured neighbourhood (MeromorphicLiouville).

theorem germ_eq_const_of_mem_linearSystem_zero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X)
    (hf : f ∈ linearSystem (X := X) 0) : ∃ c : ℂ, ∀ x, ∀ᶠ z in 𝓝[≠] x, f.toFun z = c

lDim_zero_eq_one

l(0) = 1: L(0)/germZero ≅ ℂ (the constants). Spanned by the class of the constant 1 (nonzero, since its order is 0 ≠ ⊤), and every member is germ-constant by Liouville, hence a scalar multiple of it.

theorem lDim_zero_eq_one [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] :
    lDim (X := X) 0 = 1