19.8. Finiteness.CechFinitenessDtwist🔗

Jacobians.Finiteness.CechFinitenessDtwist — source

piSec

The 𝒪_D Pi-section submodule over a finite family of opens W : ι → Opens X: tuples of germs with each component a 𝒪_D-germ. Both sections0 D and sections1 D are instances of this (with W the cover-sets resp. the pairwise overlaps). Definitionally a Submodule of ∀ i, MGerm (W i).

def piSec {ι : Type*} (W : ι → Opens X) (D : Divisor X) : Submodule ℂ (∀ i, MGerm (W i)) where

piSec_coeff

The component coefficient functional piSec W (D+P) →ₗ[ℂ] ℂ at index i: the order-(−D(P)−1) principal-part coefficient at P on W i when P ∈ W i (coeffGermLin), and 0 otherwise. Its vanishing characterises 𝒪_D-membership of the i-component (piSec_coeff_eq_zero_iff).

noncomputable def piSec_coeff {ι : Type*} (W : ι → Opens X) (D : Divisor X) (P : X) (i : ι) :
    piSec W (D + Finsupp.single P 1) →ₗ[ℂ] ℂ

piSec_coeff_eq_zero_iff

The component coefficient vanishes iff the i-component is a 𝒪_D-germ. When P ∈ W i this is ker_coeffGermLin; when P ∉ W i the coefficient is 0 and the D / D+P section spaces coincide (OmegaDGerm_add_single_eq_of_not_mem), so membership is automatic.

theorem piSec_coeff_eq_zero_iff {ι : Type*} (W : ι → Opens X) (D : Divisor X) (P : X) (i : ι)
    (f : piSec W (D + Finsupp.single P 1)) :
    piSec_coeff W D P i f = 0 ↔ (f : ∀ i, MGerm (W i)) i ∈ OmegaDGerm D (W i)

finiteDimensional_piSec_quotient

The Pi-section skyscraper-correction quotient is finite-dimensional. Over a *finite* family W : ι → Opens X, the quotient piSec W (D+P) ⧸ piSec W D injects, via the tuple of component principal-part coefficients piSec_coeff, into the clean finite-dimensional ι → ℂ; the kernel of that tuple map is exactly piSec W D (piSec_coeff_eq_zero_iff), so the quotient is finite-dimensional. (Routing through ι → ℂ rather than the product of stalk quotients avoids the heavy Module-instance synthesis on the dependent product of OmegaDGerm-quotients.)

theorem finiteDimensional_piSec_quotient {ι : Type*} [Fintype ι] (W : ι → Opens X)
    (D : Divisor X) (P : X) :
    FiniteDimensional ℂ
      (piSec W (D + Finsupp.single P 1) ⧸
        (piSec W D).submoduleOf (piSec W (D + Finsupp.single P 1)))

finiteDimensional_inf_quotient

Finiteness through ⊓. For A ≤ B and any K, the quotient (K ⊓ B) ⧸ (K ⊓ A) injects into B ⧸ A (the inclusion K ⊓ B ↪ B), so it is finite-dimensional whenever B ⧸ A is. (Used for cocycles1 = ker δ¹ ⊓ sections1: K = ker δ¹, A/B = sections1 D / sections1 (D+P).)

theorem finiteDimensional_inf_quotient {M : Type*} [AddCommGroup M] [Module ℂ M]
    (K A B : Submodule ℂ M) (_hAB : A ≤ B)
    (hfin : FiniteDimensional ℂ (B ⧸ A.submoduleOf B)) :
    FiniteDimensional ℂ
      ((K ⊓ B : Submodule ℂ M) ⧸ (K ⊓ A).submoduleOf (K ⊓ B : Submodule ℂ M))

finiteDimensional_map_quotient

Finiteness through map. For A0 ≤ B0 and a linear map f, the quotient (map f B0) ⧸ (map f A0) is a quotient (surjective image) of B0 ⧸ A0 (via f descended), so it is finite-dimensional whenever B0 ⧸ A0 is. (Used for coboundaries1 = map δ⁰ sections0.)

theorem finiteDimensional_map_quotient {M N : Type*} [AddCommGroup M] [Module ℂ M]
    [AddCommGroup N] [Module ℂ N] (f : M →ₗ[ℂ] N) (A0 B0 : Submodule ℂ M) (_hAB : A0 ≤ B0)
    (hfin : FiniteDimensional ℂ (B0 ⧸ A0.submoduleOf B0)) :
    FiniteDimensional ℂ ((B0.map f) ⧸ (A0.map f).submoduleOf (B0.map f))

finiteDimensional_sections1_quotient

sections1 (D+P) ⧸ sections1 D is finite-dimensional: it injects into the finite product ∏ p, (OmegaDGerm (D+P) (U_p) ⧸ OmegaDGerm D (U_p)) of stalk quotients (each ≤ 1-dim, finitely many overlaps p : ι × ι).

theorem finiteDimensional_sections1_quotient :
    FiniteDimensional ℂ
      (𝔘.sections1 (D + Finsupp.single P 1) ⧸
        (𝔘.sections1 D).submoduleOf (𝔘.sections1 (D + Finsupp.single P 1)))

finiteDimensional_sections0_quotient

sections0 (D+P) ⧸ sections0 D is finite-dimensional (degree-0 analogue).

theorem finiteDimensional_sections0_quotient :
    FiniteDimensional ℂ
      (𝔘.sections0 (D + Finsupp.single P 1) ⧸
        (𝔘.sections0 D).submoduleOf (𝔘.sections0 (D + Finsupp.single P 1)))

finiteDimensional_cocycles1_quotient

cocycles1 (D+P) ⧸ cocycles1 D is finite-dimensional: the cocycle quotient injects into the section quotient sections1 (D+P) ⧸ sections1 D (cocycles1 = ker δ¹ ⊓ sections1).

theorem finiteDimensional_cocycles1_quotient :
    FiniteDimensional ℂ
      (𝔘.cocycles1 (D + Finsupp.single P 1) ⧸
        (𝔘.cocycles1 D).submoduleOf (𝔘.cocycles1 (D + Finsupp.single P 1)))

finiteDimensional_coboundaries1_quotient

coboundaries1 (D+P) ⧸ coboundaries1 D is finite-dimensional: it is a quotient of the degree-0 section quotient sections0 (D+P) ⧸ sections0 D (coboundaries1 = δ⁰(sections0)).

theorem finiteDimensional_coboundaries1_quotient :
    FiniteDimensional ℂ
      (𝔘.coboundaries1 (D + Finsupp.single P 1) ⧸
        (𝔘.coboundaries1 D).submoduleOf (𝔘.coboundaries1 (D + Finsupp.single P 1)))

h1Map_mk

h1Map on a cocycle class is the class of the cocycle inclusion: h1Map [c] = [incl c]. (The defining Submodule.mapQ computation.)

theorem h1Map_mk (c : 𝔘.cocycles1 D) :
    𝔘.h1Map D P (Submodule.Quotient.mk c)
      = Submodule.Quotient.mk (𝔘.cocyclesIncl D P c)

finiteDimensional_cechH1_add_single_of

Forward per-point step. H¹(𝒪_D) finite ⟹ H¹(𝒪_{D+P}) finite. range h1Map is finite (image of finite-dim H¹(𝒪_D)); coker h1Map is a quotient of cocycles1(D+P)/cocycles1(D) (finite, finiteDimensional_cocycles1_quotient); so H¹(𝒪_{D+P}) is the extension of two finite-dim spaces (Module.Finite.of_submodule_quotient).

theorem finiteDimensional_cechH1_add_single_of
    (h : FiniteDimensional ℂ (𝔘.cechH1 D)) :
    FiniteDimensional ℂ (𝔘.cechH1 (D + Finsupp.single P 1))

finiteDimensional_ker_h1Map

ker (h1Map D P) is finite-dimensional. An element is a D-cocycle class [c]_D whose (D+P)-class vanishes, i.e. c ∈ cocycles1 D ⊓ coboundaries1 (D+P); the H¹-class map surjects that intersection onto ker (h1Map D P) (killing cocycles1 D ⊓ coboundaries1 D), and the resulting domain quotient injects into the finite coboundaries1 (D+P)/coboundaries1 D (finiteDimensional_inf_quotient).

theorem finiteDimensional_ker_h1Map :
    FiniteDimensional ℂ (LinearMap.ker (𝔘.h1Map D P))

finiteDimensional_cechH1_of_add_single

Backward per-point step. H¹(𝒪_{D+P}) finite ⟹ H¹(𝒪_D) finite. ker (h1Map D P) is finite-dimensional (finiteDimensional_ker_h1Map), and H¹(𝒪\_D)/ker (h1Map) ≅ range (h1Map) ⊆ H¹(𝒪\_\{D+P\}) is finite; so H¹(𝒪\_D) is the extension of two finite-dim spaces (Module.Finite.of_submodule_quotient).

theorem finiteDimensional_cechH1_of_add_single
    (h : FiniteDimensional ℂ (𝔘.cechH1 (D + Finsupp.single P 1))) :
    FiniteDimensional ℂ (𝔘.cechH1 D)

finiteDimensional_cechH1_add_single_iff

The bidirectional per-point step. H¹(𝒪_{D+P}) is finite iff H¹(𝒪_D) is.

theorem finiteDimensional_cechH1_add_single_iff :
    FiniteDimensional ℂ (𝔘.cechH1 (D + Finsupp.single P 1)) ↔
      FiniteDimensional ℂ (𝔘.cechH1 D)

finiteDimensional_cechH1_add_singlePoint_iff

H¹(𝒪_{D + single P k}) is finite iff H¹(𝒪_D) is, for any integer k (induct on k via Int.induction_on; ±1 at a time is the per-point step).

theorem finiteDimensional_cechH1_add_singlePoint_iff (k : ℤ) :
    FiniteDimensional ℂ (𝔘.cechH1 (D + Finsupp.single P k)) ↔
      FiniteDimensional ℂ (𝔘.cechH1 D)

finiteDimensional_cechH1_of_zero

Finiteness of H¹(𝒪_D) for any divisor D, on a FIXED cover, from the D = 0 case (the divisor induction). Finsupp.induction on D adds one point at a time; each addition is the single-point step.

theorem finiteDimensional_cechH1_of_zero (h0 : FiniteDimensional ℂ (𝔘.cechH1 (0 : Divisor X)))
    (D : Divisor X) :
    FiniteDimensional ℂ (𝔘.cechH1 D)

finiteDimensional_cechH1_general

General-divisor Čech H¹ finiteness (Forster 14.9 + §16 skyscraper). For an arbitrary finite cover 𝔘 and an arbitrary divisor D, H¹(𝔘, 𝒪_D) is finite-dimensional. The D = 0 case (finiteDimensional_cechH1_zero) is climbed to general D one point at a time via the skyscraper stalk quotient (finiteDimensional_cechH1_of_zero).

theorem finiteDimensional_cechH1_general (𝔘 : FiniteCover X) (D : Divisor X) :
    FiniteDimensional ℂ (𝔘.cechH1 D)

exists_cechModel_general

exists_cechModel 𝔘 D — the full, general-divisor statement. Combines the general-divisor finiteness finiteDimensional_cechH1_general (this file) with the artificial single-point Montel model exists_cechModel_of_finiteDimensional (CechModelArtificial). This is exactly the statement of CechFinitenessWiring.exists_cechModel for an ARBITRARY divisor D — the finiteness node's keystone — with no remaining hypotheses. (The CechFinitenessWiring.exists_cechModel declaration itself is discharged by this term once the model-types import cycle is broken; see the project notes.)

theorem exists_cechModel_general (𝔘 : FiniteCover X) (D : Divisor X) :
    ∃ (d : DiskOverlapData) (c : Coboundaries d), Nonempty (𝔘.cechH1 D ≃ₗ[ℂ] c.supH1)