28.4. H1Genus.CechH1CupKill🔗

Jacobians.H1Genus.CechH1CupKill — source

IsMeromorphic.const

Constant functions are meromorphic (chart pullbacks of constants are constant).

theorem IsMeromorphic.const {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (c : ℂ) :
    IsMeromorphic X fun _ => c

MeromorphicFunction.one_toFun

@[simp] theorem MeromorphicFunction.one_toFun {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] :
    (1 : MeromorphicFunction X).toFun = fun _ => (1 : ℂ)

MeromorphicFunction.orderW_one

The constant 1 has germ-order 0 at every point.

theorem MeromorphicFunction.orderW_one {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    (1 : MeromorphicFunction X).orderW x = 0

MeromorphicFunction.orderW_mul

Order is additive in products: orderW (f·g) = orderW f + orderW g (Mathlib meromorphicOrderAt_mul, read in the chart at each point).

theorem MeromorphicFunction.orderW_mul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f g : MeromorphicFunction X) (x : X) :
    (f * g).orderW x = f.orderW x + g.orderW x

mul_mem_linearSystem

Products multiply linear systems: L(E)·L(E') ⊆ L(E + E').

theorem mul_mem_linearSystem {E E' : Divisor X} {f g : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) E) (hg : g ∈ linearSystem (X := X) E') :
    f * g ∈ linearSystem (X := X) (E + E')

one_mem_linearSystem

The constant 1 lies in L(E) for every effective E.

theorem one_mem_linearSystem {E : Divisor X} (hE : 0 ≤ E) :
    (1 : MeromorphicFunction X) ∈ linearSystem (X := X) E

linearSystem_congr

Transport of linear-system membership along an equality of divisors (the divisor appears in dependent positions at call sites, so a plain rw can fail the motive check; this helper rewrites at the statement level, where f is opaque).

theorem linearSystem_congr {E E' : Divisor X} (h : E = E') {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) E) : f ∈ linearSystem (X := X) E'

orderW_inv_mul_sub_one

f⁻¹·f − 1 is germ-zero for a non-germ-zero f: off the (isolated) zeros of f.toFun the product is exactly 1.

theorem orderW_inv_mul_sub_one {f : MeromorphicFunction X} (hne : ∀ x, f.orderW x ≠ ⊤) (x : X) :
    (f⁻¹ * f - 1).orderW x = ⊤

MeromorphicFunction.div_apply_eq_untop₀

The divisor div f reads the germ-order: at every point (div f) x = untop₀ (orderW f x).

theorem MeromorphicFunction.div_apply_eq_untop₀ (f : MeromorphicFunction X) (x : X) :
    MeromorphicFunction.div X f x = (f.orderW x).untop₀

MeromorphicFunction.orderW_eq_div

For a non-germ-zero f, the order at every point is the (finite) divisor coefficient.

theorem MeromorphicFunction.orderW_eq_div {f : MeromorphicFunction X}
    (hne : ∀ x, f.orderW x ≠ ⊤) (x : X) :
    f.orderW x = ((MeromorphicFunction.div X f x : ℤ) : WithTop ℤ)

inv_mem_linearSystem_div

The reciprocal lies in L(div f): orderW (f⁻¹) = −orderW f = −div f ≥ −div f.

theorem inv_mem_linearSystem_div {f : MeromorphicFunction X} (hne : ∀ x, f.orderW x ≠ ⊤) :
    f⁻¹ ∈ linearSystem (X := X) (MeromorphicFunction.div X f)

effective_add_div

For f ∈ L(E) (non-germ-zero), the divisor E + div f is effective.

theorem effective_add_div {E : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) E) (hne : ∀ x, f.orderW x ≠ ⊤) :
    0 ≤ E + MeromorphicFunction.div X f

globalGerm_mul

globalGerm is multiplicative in the meromorphic function.

theorem globalGerm_mul {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f g : MeromorphicFunction X) (U : Opens X) :
    globalGerm (f * g) U = globalGerm f U * globalGerm g U

globalGerm_one

globalGerm of the constant 1 is the unit germ.

theorem globalGerm_one {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (U : Opens X) :
    globalGerm (1 : MeromorphicFunction X) U = 1

globalGerm_sub

globalGerm is subtractive in the meromorphic function.

theorem globalGerm_sub {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (f g : MeromorphicFunction X) (U : Opens X) :
    globalGerm (f - g) U = globalGerm f U - globalGerm g U

cupH1_mul

The cup action is multiplicative: g ⌣ (f ⌣ ξ) = (g·f) ⌣ ξ (germ multiplication is associative).

theorem cupH1_mul {D K K' : Divisor X} {f g : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (hg : g ∈ linearSystem (X := X) (K' - K))
    (hgf : g * f ∈ linearSystem (X := X) (K' - D)) (ξ : 𝔘.cechH1 D) :
    cupH1 hg (cupH1 hf ξ) = cupH1 hgf ξ

cupH1_one_eq_h1Incl

Cup with the constant 1 is the inclusion-induced map h1Incl.

theorem cupH1_one_eq_h1Incl {𝔘 : FiniteCover X} {D K : Divisor X} (hDK : D ≤ K)
    (h1m : (1 : MeromorphicFunction X) ∈ linearSystem (X := X) (K - D)) (ξ : 𝔘.cechH1 D) :
    cupH1 h1m ξ = 𝔘.h1Incl hDK ξ

cupH1_congr_germ

The cup action only sees the germ: germ-equal multipliers give equal cup actions.

theorem cupH1_congr_germ {D K : Divisor X} {f f' : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (K - D)) (hf' : f' ∈ linearSystem (X := X) (K - D))
    (h : ∀ x, (f - f').orderW x = ⊤) (ξ : 𝔘.cechH1 D) :
    cupH1 hf ξ = cupH1 hf' ξ

exists_effective_h1Incl_eq_zero

The kill lemma (Miranda Ch. X §2 / the Forster §16–17 pigeonhole). For a locally realizable cover, every class ξ ∈ H¹(𝔘, 𝒪) has an effective divisor A (depending on ξ) whose inclusion-induced map kills it: H¹(𝒪) → H¹(𝒪_A), ξ ↦ 0.

A = h¹(0)·P + div f where f ∈ L(h¹(0)·P) is a pigeonhole kernel element of the cup action f ↦ f ⌣ ξ (which exists since l(h¹(0)·P) > h¹(h¹(0)·P) by cohomological Riemann–Roch).

theorem exists_effective_h1Incl_eq_zero (𝔘 : FiniteCover X) (hR : 𝔘.LocallyRealizable)
    (ξ : 𝔘.cechH1 (0 : Divisor X)) :
    ∃ (A : Divisor X) (h0A : (0 : Divisor X) ≤ A), 𝔘.h1Incl h0A ξ = 0