Grothendieck pretopologies #
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
- coverings : Π (X : C), set (category_theory.presieve X)
- has_isos : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [_inst_3 : category_theory.is_iso f], category_theory.presieve.singleton f ∈ self.coverings X
- pullbacks : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : category_theory.presieve X), S ∈ self.coverings X → category_theory.presieve.pullback_arrows f S ∈ self.coverings Y
- transitive : ∀ ⦃X : C⦄ (S : category_theory.presieve X) (Ti : Π ⦃Y : C⦄ (f : Y ⟶ X), S f → category_theory.presieve Y), S ∈ self.coverings X → (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ self.coverings Y) → S.bind Ti ∈ self.coverings X
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.
K can be completed to a Grothendieck topology
J by declaring a sieve to be
J-covering if it contains a family in
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.