Grothendieck pretopologies #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Definition and lemmas about Grothendieck pretopologies.
A Grothendieck pretopology for a category
C is a set of families of morphisms with fixed codomain,
satisfying certain closure conditions.
We show that a pretopology generates a genuine Grothendieck topology, and every topology has
a maximal pretopology which generates it.
The pretopology associated to a topological space is defined in
coverage, pretopology, site
A (Grothendieck) pretopology on
C consists of a collection of families of morphisms with a fixed
X for every object
C, called "coverings" of
X, which satisfies the following
- Every family consisting of a single isomorphism is a covering family.
- The collection of covering families is stable under pullback.
- Given a covering family, and a covering family on each domain of the former, the composition
is a covering family.
In some sense, a pretopology can be seen as Grothendieck topology with weaker saturation conditions,
in that each covering is not necessarily downward closed.
See: https://ncatlab.org/nlab/show/Grothendieck+pretopology, or
https://stacks.math.columbia.edu/tag/00VH, or [MM92] Chapter III, Section 2, Definition 2.
Note that Stacks calls a category together with a pretopology a site, and [MM92] calls this
a basis for a topology.
The largest pretopology generating the given Grothendieck topology.
See [MM92] Chapter III, Section 2, Equations (3,4).
We have a galois insertion from pretopologies to Grothendieck topologies.
The trivial pretopology, in which the coverings are exactly singleton isomorphisms. This topology is
also known as the indiscrete, coarse, or chaotic topology.
The trivial pretopology induces the trivial grothendieck topology.