20.8. CanonicalForms.SerreOmega0🔗

Jacobians.CanonicalForms.SerreOmega0 — source

constOneMero

The constant meromorphic function 1 (order 0 everywhere).

noncomputable def constOneMero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] :
    MeromorphicFunction X

constOneMero_orderW

theorem constOneMero_orderW {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    (constOneMero (X := X)).orderW x = 0

constOneMero_mem_linearSystem

The constant 1 lies in L(D) for any divisor D with all coefficients ≥ 0 (0 ≤ D x): its order is 0 ≥ -(D x).

theorem constOneMero_mem_linearSystem {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {D : Divisor X} (hD : ∀ x, 0 ≤ D x) :
    constOneMero (X := X) ∈ linearSystem (X := X) D

constOneMero_class_ne_zero

The class of the constant 1 in the linear-system quotient lSysModule D is nonzero (its order is 0 ≠ ⊤, so it is not germ-zero).

theorem constOneMero_class_ne_zero {X : Type*} [TopologicalSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] {D : Divisor X} (hD : ∀ x, 0 ≤ D x) :
    (Submodule.Quotient.mk ⟨constOneMero (X := X), constOneMero_mem_linearSystem hD⟩ :
      lSysModule (X := X) D) ≠ 0

riemannRoch_inequality

Riemann–Roch inequality (Forster §16). For a locally-realizable cover 𝔘 and any divisor D, the cohomological RR equality gives, dropping the (nonnegative) h¹(D) term,

deg D + 1 − h¹(0) ≤ lDim D.

(h⁰(D) = lDim D by h0Dim_eq_lDim; h1Dim D ≥ 0 is Int.natCast_nonneg.)

theorem riemannRoch_inequality {𝔘 : FiniteCover X} (hR : 𝔘.LocallyRealizable) (D : Divisor X) :
    Divisor.deg X D + 1 - (𝔘.h1Dim 0 : ℤ) ≤ (lDim (X := X) D : ℤ)

two_le_lDim_largeEffective

2 ≤ lDim D for D = (h¹(0)+1)·P. Taking the effective divisor of degree h¹(0)+1 concentrated at a single point P makes the RR lower bound deg D + 1 − h¹(0) = 2.

theorem two_le_lDim_largeEffective {𝔘 : FiniteCover X} (hR : 𝔘.LocallyRealizable) (P : X) :
    2 ≤ lDim (X := X) (Finsupp.single P ((𝔘.h1Dim 0 : ℤ) + 1))

IsGermConstant

A meromorphic function f is germ-constant if it agrees, on a punctured neighbourhood of every point, with one fixed scalar c. Negation of this is the working notion of "nonconstant" (matching germ_eq_const_of_mem_linearSystem_zero, the Liouville statement).

def IsGermConstant (f : MeromorphicFunction X) : Prop

exists_nonconstant_meromorphic

Existence of a nonconstant meromorphic function.

On a compact connected Riemann surface X there is a nonconstant meromorphic function: a f : MeromorphicFunction X lying in some complete linear system L(D) whose germ is not constant (¬ IsGermConstant f).

Proof: pick a point P and a locally-realizable (Leray) cover (exists_realizableLerayCover). The Riemann–Roch inequality gives 2 ≤ lDim D for D = (h¹(0)+1)·P (two_le_lDim_largeEffective), so the quotient lSysModule D has finrank ≥ 2. By exists_linearIndependent_pair_of_one_lt_finrank applied to the nonzero class of the constant 1, there is a class [g] linearly independent from [1]. Its representative g ∈ L(D) cannot be germ-constant: a germ-constant function in L(D) is germ-equal to c·1, hence [g] = c·[1], contradicting linear independence of ![[1], [g]].

theorem exists_nonconstant_meromorphic :
    ∃ (D : Divisor X) (f : MeromorphicFunction X),
      f ∈ linearSystem (X := X) D ∧ ¬ IsGermConstant f

exists_nonconstant_meromorphicFunction

Headline form. A compact connected Riemann surface carries a nonconstant meromorphic function (its germ is not constant). This is the existence underlying ω₀ = df — the nonzero meromorphic 1-form whose canonical divisor is K = div ω₀. A direct corollary of exists_nonconstant_meromorphic.

theorem exists_nonconstant_meromorphicFunction :
    ∃ f : MeromorphicFunction X, ¬ IsGermConstant f