Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isSheaf_type_propQCTopology_iff

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

Defined in

Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Cited by

1 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicativeAlgebraicGeometry.IsZariskiLocalAtSource