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
- P.precoverage = { coverings := fun (X : C) (S : CategoryTheory.Presieve X) => ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → P f }
Instances For
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 := ⋯ }
Instances For
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
.
Alias of CategoryTheory.MorphismProperty.pretopology_monotone
.