A machine-checked solution to the Jacobians challenge

19.31. Finiteness.SkyscraperLESBase🔗

Jacobians.Finiteness.SkyscraperLESBase — source

divisor_le_add_single

Pointwise monotonicity of the divisor under adding an effective point: D x ≤ (D + P) x.

theorem divisor_le_add_single {X : Type*} (D : Divisor X) (P x : X) :
    (D : Divisor X) x ≤ (D + Finsupp.single P 1 : Divisor X) x

mem_OmegaD_add_single

The order bound for 𝒪_D implies that for 𝒪_{D+P} (the bound −(D+P) ≤ −D weakens).

theorem mem_OmegaD_add_single {D : Divisor X} {P : X} {U : Opens X} {f : U → ℂ}
    (hf : f ∈ OmegaD D U) : f ∈ OmegaD (D + Finsupp.single P 1) U

OmegaDGerm_le_add_single

Germ-class sections inherit the inclusion 𝒪_D(U) ⊆ 𝒪_{D+P}(U).

theorem OmegaDGerm_le_add_single (D : Divisor X) (P : X) (U : Opens X) :
    OmegaDGerm D U ≤ OmegaDGerm (D + Finsupp.single P 1) U

sections0_le_add_single

The 𝒪_D 0-sections are contained in the 𝒪_{D+P} 0-sections.

theorem sections0_le_add_single (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.sections0 D ≤ 𝔘.sections0 (D + Finsupp.single P 1)

globalSections_le_add_single

The global 𝒪_D-sections are contained in the global 𝒪_{D+P}-sections (same ker δ⁰, weaker sheaf condition). This is the underlying map of the long-exact-sequence arrow H⁰(D) → H⁰(D+P).

theorem globalSections_le_add_single (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.globalSections D ≤ 𝔘.globalSections (D + Finsupp.single P 1)

h0Incl

The canonical H⁰-inclusion H⁰(𝒪_D) ↪ H⁰(𝒪_{D+P}) (the order bound weakens, f₁ of the LES).

noncomputable def h0Incl (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    ↥(𝔘.globalSections D) →ₗ[ℂ] ↥(𝔘.globalSections (D + Finsupp.single P 1))

h0Incl_injective

theorem h0Incl_injective (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    Function.Injective (𝔘.h0Incl D P)

Skyscraper

The skyscraper space ℂ_P at P: the genuine 1-dimensional stalk of the skyscraper sheaf 𝒪_{D+P}/𝒪_D (the order-(−D(P)−1) principal-part coefficient at P), realised as ℂ.

Note (a soundness subtlety): the H⁰-cokernel H⁰(𝒪_{D+P}) ⧸ range f₁ would be the *wrong* middle term — at a base point of |D+P| that cokernel is 0-dimensional, so demanding finrank = 1 of it would be provably false. The genuine middle term of the cohomology LES of 0 → 𝒪_D → 𝒪_{D+P} → ℂ_P → 0 is H⁰(X, ℂ_P) = ℂ (always 1-dim); the coefficient arrow f₂ : H⁰(𝒪_{D+P}) → ℂ_P is not surjective in general (its image *is* the cokernel), so it lives — together with the exactness range f₁ = ker f₂ — as honest data in SkyscraperLES.

abbrev Skyscraper (_𝔘 : FiniteCover X) (_D : Divisor X) (_P : X) : Type

sections1_le_add_single

The 𝒪_D 1-sections are contained in the 𝒪_{D+P} 1-sections (order weakening).

theorem sections1_le_add_single (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.sections1 D ≤ 𝔘.sections1 (D + Finsupp.single P 1)

cocycles1_le_add_single

The 𝒪_D 1-cocycles are contained in the 𝒪_{D+P} 1-cocycles (same ker δ¹, weaker sheaf).

theorem cocycles1_le_add_single (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.cocycles1 D ≤ 𝔘.cocycles1 (D + Finsupp.single P 1)

coboundaries1_le_add_single

The 𝒪_D 1-coboundaries are contained in the 𝒪_{D+P} 1-coboundaries (δ⁰ of more sections).

theorem coboundaries1_le_add_single (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.coboundaries1 D ≤ 𝔘.coboundaries1 (D + Finsupp.single P 1)

cocyclesIncl

The 1-cocycle inclusion Z¹(𝒪_D) ↪ Z¹(𝒪_{D+P}).

noncomputable def cocyclesIncl (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    ↥(𝔘.cocycles1 D) →ₗ[ℂ] ↥(𝔘.cocycles1 (D + Finsupp.single P 1))

h1Map

The inclusion-induced arrow f₄ : H¹(𝒪_D) → H¹(𝒪_{D+P}). The cocycle inclusion sends 𝒪_D-coboundaries to 𝒪_{D+P}-coboundaries, so it descends to the H¹ quotients (Submodule.mapQ).

noncomputable def h1Map (𝔘 : FiniteCover X) (D : Divisor X) (P : X) :
    𝔘.cechH1 D →ₗ[ℂ] 𝔘.cechH1 (D + Finsupp.single P 1)

cechDelta0_sections

δ⁰ preserves the sections subcomplex. The Čech coboundary of 𝒪_D-0-sections is an 𝒪_D-1-section: each component (δ⁰f)_{ij} = f_j|_{ij} − f_i|_{ij} is a difference of restrictions of 𝒪_D-germs, hence an 𝒪_D-germ on the overlap (rawRestrictG_omegaDGerm). Equivalently B¹(𝒪_D) ⊆ C¹(𝒪_D).

theorem cechDelta0_sections (𝔘 : FiniteCover X) (D : Divisor X) :
    Submodule.map 𝔘.cechDelta0 (𝔘.sections0 D) ≤ 𝔘.sections1 D

SkyscraperLES

δ⁰ preserves the sections subcomplex. The Čech coboundary of 𝒪_D-0-sections is an 𝒪_D-1-section: each component (δ⁰f)_{ij} = f_j|_{ij} − f_i|_{ij} is a difference of restrictions of 𝒪_D-germs, hence an 𝒪_D-germ on the overlap (rawRestrictG_omegaDGerm). Equivalently B¹(𝒪_D) ⊆ C¹(𝒪_D). -/ theorem cechDelta0_sections (𝔘 : FiniteCover X) (D : Divisor X) : Submodule.map 𝔘.cechDelta0 (𝔘.sections0 D) ≤ 𝔘.sections1 D := by rintro _ ⟨f, hf, rfl⟩ p simp only [cechDelta0, LinearMap.pi_apply, LinearMap.sub_apply, LinearMap.comp_apply, LinearMap.proj_apply] exact sub_mem (rawRestrictG_omegaDGerm inf_le_right (hf p.2)) (rawRestrictG_omegaDGerm inf_le_left (hf p.1))

/-! ### The skyscraper long exact sequence structure (the genuine homological/analytic kernel)

The single-point χ-jump comes from the skyscraper short exact sequence of 𝒪_D-modules 0 → 𝒪_D → 𝒪_{D+P} → ℂ_P → 0 (ℂ_P = the 1-dimensional skyscraper at P). Its long exact sequence in Čech cohomology is 0 → H⁰(𝒪_D) →[f₁] H⁰(𝒪_{D+P}) →[f₂] ℂ_P →[f₃] H¹(𝒪_D) →[f₄] H¹(𝒪_{D+P}) → 0, the skyscraper having H^{≥1} = 0.

SkyscraperLES bundles the data not already provided above. The first arrow f₁ (h0Incl) and the last arrow f₄ (h1Map, the inclusion-induced map) are constructed above; the inclusion f₁ is injective (h0Incl_injective). The content isolated here is the coefficient arrow f₂ = h0ToSky with exact₁₂, the snake-lemma connecting map f₃ with exactness (exact₂, exact₃, surj₄), and finiteness of the cohomology groups (Forster 14.9).

structure SkyscraperLES (𝔘 : FiniteCover X) (D : Divisor X) (P : X) where