Positive-degree exactness of affine Cech complexes

This file proves that the Cech complex of the sheaf associated to an R-module is exact in positive degrees for a finite distinguished-open cover of Spec R.

The proof restricts the cover to each member D(f_i). There that member is terminal, so the Cech nerve has an extra degeneracy and its alternating coface complex is exact. The restriction maps on sections are localizations away from f_i; exactness therefore descends from the distinguished cover because its defining elements span the unit ideal.

This is a statement about the explicit Cech complex. It does not assert a comparison between Cech cohomology and derived-functor sheaf cohomology.

theorem TopologicalSpace.Opens.iicHasTerminal {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasTerminal ↑(Set.Iic V)

theorem TopologicalSpace.Opens.iicHasLimitPair {X : Type u_1} [TopologicalSpace X] (V : Opens X) {U W : ↑(Set.Iic V)} : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair U W)

theorem TopologicalSpace.Opens.iicHasBinaryProducts {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasBinaryProducts ↑(Set.Iic V)

theorem TopologicalSpace.Opens.iicHasFiniteProducts {X : Type u_1} [TopologicalSpace X] (V : Opens X) : CategoryTheory.Limits.HasFiniteProducts ↑(Set.Iic V)

theorem AlgebraicGeometry.tilde_cechComplex_exactAt_succ {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (n : ℕ) : HomologicalComplex.ExactAt ((CategoryTheory.cechComplexFunctor fun (i : ι) => PrimeSpectrum.basicOpen (f i)).obj (modulesSpecToSheaf.obj (tilde M)).presheaf) (n + 1)

The Cech complex of a module sheaf on a finite distinguished-open cover of Spec R is exact in every positive degree.

The hypothesis says that the elements defining the cover span the unit ideal.

theorem AlgebraicGeometry.tilde_cechComplex_exactAt_succ_of_eq_iSup {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (d : ↑R) (hcover : PrimeSpectrum.basicOpen d = ⨆ (i : ι), PrimeSpectrum.basicOpen (f i)) (M : ModuleCat ↑R) (n : ℕ) : HomologicalComplex.ExactAt ((CategoryTheory.cechComplexFunctor fun (i : ι) => PrimeSpectrum.basicOpen (f i)).obj (modulesSpecToSheaf.obj (tilde M)).presheaf) (n + 1)

The Cech complex of a module sheaf is exact in positive degrees on a finite distinguished-open cover of an arbitrary distinguished open D(d).

theorem AlgebraicGeometry.tilde_cechComplex_exactAt_of_pos {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (k : ℕ) (hk : 0 < k) : HomologicalComplex.ExactAt ((CategoryTheory.cechComplexFunctor fun (i : ι) => PrimeSpectrum.basicOpen (f i)).obj (modulesSpecToSheaf.obj (tilde M)).presheaf) k

Positive-degree form of tilde_cechComplex_exactAt_succ.