28.6. H1Genus.CechH1Monotonicity🔗

Jacobians.H1Genus.CechH1Monotonicity — source

mem_OmegaD_mono

The order bound for 𝒪_D implies that for 𝒪_{D'} whenever D ≤ D' (the bound −D' ≤ −D weakens). Generalises mem_OmegaD_add_single.

theorem mem_OmegaD_mono {D D' : Divisor X} (h : D ≤ D') {U : Opens X} {f : U → ℂ}
    (hf : f ∈ OmegaD D U) : f ∈ OmegaD D' U

OmegaDGerm_mono

Germ-class sections inherit the inclusion 𝒪_D(U) ⊆ 𝒪_{D'}(U) for D ≤ D'.

theorem OmegaDGerm_mono {D D' : Divisor X} (h : D ≤ D') (U : Opens X) :
    OmegaDGerm D U ≤ OmegaDGerm D' U

sections0_mono

The 𝒪_D 0-sections are contained in the 𝒪_{D'} 0-sections for D ≤ D'.

theorem sections0_mono {D D' : Divisor X} (h : D ≤ D') :
    𝔘.sections0 D ≤ 𝔘.sections0 D'

sections1_mono

The 𝒪_D 1-sections are contained in the 𝒪_{D'} 1-sections for D ≤ D'.

theorem sections1_mono {D D' : Divisor X} (h : D ≤ D') :
    𝔘.sections1 D ≤ 𝔘.sections1 D'

cocycles1_mono

The 𝒪_D 1-cocycles are contained in the 𝒪_{D'} 1-cocycles for D ≤ D'.

theorem cocycles1_mono {D D' : Divisor X} (h : D ≤ D') :
    𝔘.cocycles1 D ≤ 𝔘.cocycles1 D'

coboundaries1_mono

The 𝒪_D 1-coboundaries are contained in the 𝒪_{D'} 1-coboundaries for D ≤ D'.

theorem coboundaries1_mono {D D' : Divisor X} (h : D ≤ D') :
    𝔘.coboundaries1 D ≤ 𝔘.coboundaries1 D'

cocyclesInclMono

The 1-cocycle inclusion Z¹(𝒪_D) ↪ Z¹(𝒪_{D'}) for D ≤ D'.

noncomputable def cocyclesInclMono {D D' : Divisor X} (h : D ≤ D') :
    ↥(𝔘.cocycles1 D) →ₗ[ℂ] ↥(𝔘.cocycles1 D')

h1Incl

The inclusion-induced arrow H¹(𝒪_D) → H¹(𝒪_{D'}) for D ≤ D' (generalising the single-point h1Map): the cocycle inclusion descends through the Z¹/B¹ quotients.

noncomputable def h1Incl {D D' : Divisor X} (h : D ≤ D') :
    𝔘.cechH1 D →ₗ[ℂ] 𝔘.cechH1 D'

h1Incl_mk

@[simp] theorem h1Incl_mk {D D' : Divisor X} (h : D ≤ D') (c : ↥(𝔘.cocycles1 D)) :
    𝔘.h1Incl h (Submodule.Quotient.mk c)
      = Submodule.Quotient.mk (𝔘.cocyclesInclMono h c)

h1Incl_refl

h1Incl along D ≤ D is the identity.

theorem h1Incl_refl (D : Divisor X) (h : D ≤ D) :
    𝔘.h1Incl h = LinearMap.id

h1Incl_comp

Functoriality: h1Incl (D₂ ≤ D₃) ∘ h1Incl (D₁ ≤ D₂) = h1Incl (D₁ ≤ D₃).

theorem h1Incl_comp {D₁ D₂ D₃ : Divisor X} (h₁ : D₁ ≤ D₂) (h₂ : D₂ ≤ D₃) (x : 𝔘.cechH1 D₁) :
    𝔘.h1Incl h₂ (𝔘.h1Incl h₁ x) = 𝔘.h1Incl (h₁.trans h₂) x

h1Incl_eq_h1Map

The general inclusion arrow at a single-point step agrees with h1Map (same underlying Submodule.inclusion).

theorem h1Incl_eq_h1Map (D : Divisor X) (P : X)
    (h : D ≤ D + Finsupp.single P 1) :
    𝔘.h1Incl h = 𝔘.h1Map D P

h1Incl_surjective_single

Single-point surjectivity, with the target divisor given by an equation D' = D + P (so the statement composes cleanly in the degree induction): the inclusion-induced H¹(𝒪_D) → H¹(𝒪_{D'}) is onto, by the skyscraper long exact sequence.

theorem h1Incl_surjective_single (hR : 𝔘.LocallyRealizable) {D D' : Divisor X} {P : X}
    (hD' : D' = D + Finsupp.single P 1) (h : D ≤ D') :
    Function.Surjective (𝔘.h1Incl h)

exists_pos_of_effective_ne_zero

A nonzero effective divisor has a point with a positive coefficient.

theorem exists_pos_of_effective_ne_zero {X : Type*} {E : Divisor X} (hE : 0 ≤ E)
    (hne : E ≠ 0) :
    ∃ P : X, 1 ≤ E P

deg_nonneg_of_effective

The degree of an effective divisor is nonnegative.

theorem deg_nonneg_of_effective {X : Type*} {E : Divisor X} (hE : 0 ≤ E) :
    0 ≤ Divisor.deg X E

eq_zero_of_effective_deg_zero

An effective divisor of degree 0 is 0.

theorem eq_zero_of_effective_deg_zero {X : Type*} {E : Divisor X} (hE : 0 ≤ E)
    (hdeg : Divisor.deg X E = 0) : E = 0

h1Incl_surjective

Surjectivity of the inclusion-induced H¹ map (Forster 16.8). For a locally realizable cover and D ≤ D', the map H¹(𝒪_D) → H¹(𝒪_{D'}) is onto: induct on the degree of the effective difference D' − D, peeling one point per step via the skyscraper LES.

theorem h1Incl_surjective (hR : 𝔘.LocallyRealizable) {D D' : Divisor X} (h : D ≤ D') :
    Function.Surjective (𝔘.h1Incl h)