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.precoverage {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) : Precoverage C

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

Equations

• P.precoverage = { coverings := fun (X : C) (S : CategoryTheory.Presieve X) => ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → P f }

@[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)

instance CategoryTheory.MorphismProperty.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.ContainsIdentities] [P.RespectsIso] : P.precoverage.HasIsos

instance CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] : P.precoverage.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.IsStableUnderComposition] : P.precoverage.IsStableUnderComposition

theorem CategoryTheory.MorphismProperty.precoverage_monotone {C : Type u_1} [Category.{u_2, u_1} C] {P Q : MorphismProperty C} (hPQ : P ≤ Q) : P.precoverage ≤ Q.precoverage

theorem CategoryTheory.MorphismProperty.precoverage_inf {C : Type u_1} [Category.{u_2, u_1} C] (P Q : MorphismProperty C) : (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage

def CategoryTheory.MorphismProperty.coverage {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.HasPullbacks] : Coverage C

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

Equations

• P.coverage = { toPrecoverage := P.precoverage, pullback := ⋯ }

@[simp]

theorem CategoryTheory.MorphismProperty.coverage_toPrecoverage {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.HasPullbacks] : P.coverage.toPrecoverage = P.precoverage

@[reducible, inline]

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

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

Equations

• P.grothendieckTopology = CategoryTheory.Coverage.toGrothendieck C P.coverage

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 = CategoryTheory.Precoverage.toPretopology C P.precoverage

@[simp]

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

theorem CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] [Limits.HasPullbacks C] [P.IsMultiplicative] : P.coverage = P.pretopology.toCoverage

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

theorem CategoryTheory.MorphismProperty.grothendieckTopology_eq_toGrothendieck_pretopology {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] [Limits.HasPullbacks C] [P.IsMultiplicative] : P.grothendieckTopology = Pretopology.toGrothendieck C P.pretopology

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

theorem CategoryTheory.MorphismProperty.pretopology_monotone {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

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

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

Alias of CategoryTheory.MorphismProperty.pretopology_monotone.

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