Affine Čech-to-derived comparison on the distinguished-open basis

This file combines the relative distinguished-open calculation with the generic compact-basis comparison theorem.

noncomputable def AlgebraicGeometry.Cohomology.affineBasicOpenBasis (R : CommRingCat) : CategoryTheory.Sheaf.CompactOpenBasis ↑(Spec R).toPresheafedSpace

The compact, finite-intersection-stable basis of distinguished opens of an affine spectrum.

Equations

• AlgebraicGeometry.Cohomology.affineBasicOpenBasis R = CategoryTheory.Sheaf.CompactOpenBasis.ofIsBasis (Set.range PrimeSpectrum.basicOpen) ⋯ ⋯ ⋯

theorem AlgebraicGeometry.Cohomology.top_mem_affineBasicOpenBasis (R : CommRingCat) : ⊤ ∈ (affineBasicOpenBasis R).carrier

The whole affine spectrum is the distinguished open D(1).

theorem AlgebraicGeometry.Cohomology.underlyingTilde_isCechAcyclicOnCompactBasis {R : CommRingCat} (M : ModuleCat ↑R) : CategoryTheory.Sheaf.IsCechAcyclicOnCompactBasis (affineBasicOpenBasis R) ((Scheme.Modules.toSheaf (Spec R)).obj (tilde M))

The underlying abelian sheaf of M̃ is Čech-acyclic on the distinguished-open basis.