Documentation

Mathlib.CategoryTheory.Sites.MorphismProperty

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.

source
def CategoryTheory.MorphismProperty.pretopology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) [P.IsMultiplicative] (hPb : P.StableUnderBaseChange) :
CategoryTheory.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 hPb = { coverings := fun (X : C) (S : CategoryTheory.Presieve X) => ∀ {Y : C} {f : Y ⟶ X}, S f → P f, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }
Instances For
    source
    @[reducible, inline]
    abbrev CategoryTheory.MorphismProperty.grothendieckTopology {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) [P.IsMultiplicative] (hPb : P.StableUnderBaseChange) :
    CategoryTheory.GrothendieckTopology C

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

    Equations
    Instances For
      source
      theorem CategoryTheory.MorphismProperty.pretopology_le {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.IsMultiplicative] (hPb : P.StableUnderBaseChange) [Q.IsMultiplicative] (hQb : Q.StableUnderBaseChange) (hPQ : P ≤ Q) :
      P.pretopology hPb ≤ Q.pretopology hQb
      source
      theorem CategoryTheory.MorphismProperty.pretopology_inf {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) (Q : CategoryTheory.MorphismProperty C) [P.IsMultiplicative] (hPb : P.StableUnderBaseChange) [Q.IsMultiplicative] (hQb : Q.StableUnderBaseChange) :
      (P ⊓ Q).pretopology ⋯ = P.pretopology hPb ⊓ Q.pretopology hQb