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.