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.

This is the precoverage on C where covering presieves are those where every morphism satisfies P.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.MorphismProperty.ofArrows_mem_precoverage {C : Type u_1} [Category.{u_3, u_1} C] {P : MorphismProperty C} {X : C} {ι : Type u_2} {Y : ιC} {f : (i : ι) → Y i X} :
    Presieve.ofArrows Y f P.precoverage.coverings X ∀ (i : ι), P (f i)

    If P is stable under base change, this is the coverage on C where covering presieves are those where every morphism satisfies P.

    Equations
    Instances For
      @[reducible, inline]

      If P is stable under base change, it induces a Grothendieck topology: the one associated to coverage P.

      Equations
      Instances For

        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
        Instances For

          If P is also multiplicative, the coverage induced by P is the pretopology induced by P.

          If P is also multiplicative, the topology induced by P is the topology induced by the pretopology induced by P.

          @[deprecated CategoryTheory.MorphismProperty.pretopology_monotone (since := "2025-08-28")]

          Alias of CategoryTheory.MorphismProperty.pretopology_monotone.