The site induced by a morphism property

Let C be a category with pullbacks and P be a multiplicative morphism property which is stable under base change. Then P induces a pretopology, where coverings are given by presieves whose elements satisfy P.

Standard examples of pretopologies in algebraic geometry, such as the étale site, are obtained from this construction by intersecting with the pretopology of surjective families.

def CategoryTheory.MorphismProperty.pretopology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (P : MorphismProperty C) [P.IsMultiplicative] [P.IsStableUnderBaseChange] : Pretopology C

If P is a multiplicative morphism property which is stable under base change on a category C with pullbacks, then P induces a pretopology, where coverings are given by presieves whose elements satisfy P.

Equations

• P.pretopology = { coverings := fun (X : C) (S : CategoryTheory.Presieve X) => ∀ {Y : C} {f : Y ⟶ X}, S f → P f, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.grothendieckTopology {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (P : MorphismProperty C) [P.IsMultiplicative] [P.IsStableUnderBaseChange] : GrothendieckTopology C

To a morphism property P satisfying the conditions of MorphismProperty.pretopology, we associate the Grothendieck topology generated by P.pretopology.

Equations

• P.grothendieckTopology = CategoryTheory.Pretopology.toGrothendieck C P.pretopology

theorem CategoryTheory.MorphismProperty.pretopology_le {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {P Q : MorphismProperty C} [P.IsMultiplicative] [P.IsStableUnderBaseChange] [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) : P.pretopology ≤ Q.pretopology

theorem CategoryTheory.MorphismProperty.pretopology_inf {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (P Q : MorphismProperty C) [P.IsMultiplicative] [P.IsStableUnderBaseChange] [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] : (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology