Sheaves for the quasi-compact topology

In this file we show that a presheaf is a sheaf in the AlgebraicGeometry.Scheme.propQCTopology if and only if it is a sheaf in the Zariski topology and a sheaf on single object P-coverings of affine schemes.

theorem AlgebraicGeometry.isSheaf_type_propQCTopology_iff {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] (F : CategoryTheory.Functor Schemeᵒᵖ (Type u_1)) [IsZariskiLocalAtSource P] : CategoryTheory.Presieve.IsSheaf (Scheme.propQCTopology P) F ↔ CategoryTheory.Presieve.IsSheaf Scheme.zariskiTopology F ∧ ∀ {R S : CommRingCat} (f : R ⟶ S), P (Spec.map f) → Surjective (Spec.map f) → CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton (Spec.map f))

A presheaf of types is a sheaf for the P-qc topology if and only if it is a sheaf for the Zariski topology and satisfies the sheaf property for all single object coverings { f : Spec S ⟶ Spec R } where f satisfies P.

theorem AlgebraicGeometry.isSheaf_propQCTopology_iff {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] [P.IsMultiplicative] (F : CategoryTheory.Functor Schemeᵒᵖ A) [IsZariskiLocalAtSource P] : CategoryTheory.Presheaf.IsSheaf (Scheme.propQCTopology P) F ↔ CategoryTheory.Presheaf.IsSheaf Scheme.zariskiTopology F ∧ ∀ {R S : CommRingCat} (f : R ⟶ S), P (Spec.map f) → Surjective (Spec.map f) → ∀ (M : A), CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M))) (CategoryTheory.Presieve.singleton (Spec.map f))

A presheaf is a sheaf for the P-qc topology if and only if it is a sheaf for the Zariski topology and satisfies the sheaf property for all single object coverings { f : Spec S ⟶ Spec R } where f satisfies P.