Grothendieck topologies #
Definition and lemmas about Grothendieck topologies.
A Grothendieck topology for a category
C is a set of sieves on each object
certain closure conditions.
Alternate versions of the axioms (in arrow form) are also described. Two explicit examples of Grothendieck topologies are given:
- The dense topology
- The atomic topology as well as the complete lattice structure on Grothendieck topologies (which gives two additional explicit topologies: the discrete and trivial topologies.)
A pretopology, or a basis for a topology is defined in
pretopology.lean. The topology associated
to a topological space is defined in
Grothendieck topology, coverage, pretopology, site
- [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM91]
Implementation notes #
We use the definition of [nlab] and [MM91](Chapter III, Section 2), where Grothendieck topologies are saturated collections of morphisms, rather than the notions of the Stacks project (00VG) and the Elephant, in which topologies are allowed to be unsaturated, and are then completed. TODO (BM): Add the definition from Stacks, as a pretopology, and complete to a topology.
This is so that we can produce a bijective correspondence between Grothendieck topologies on a small category and Lawvere-Tierney topologies on its presheaf topos, as well as the equivalence between Grothendieck topoi and left exact reflective subcategories of presheaf toposes.
- sieves : Π (X : C), set (category_theory.sieve X)
- top_mem' : ∀ (X : C), ⊤ ∈ self.sieves X
- pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : category_theory.sieve X⦄ (f : Y ⟶ X), S ∈ self.sieves X → category_theory.sieve.pullback f S ∈ self.sieves Y
- transitive' : ∀ ⦃X : C⦄ ⦃S : category_theory.sieve X⦄, S ∈ self.sieves X → ∀ (R : category_theory.sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑S f → category_theory.sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X
The definition of a Grothendieck topology: a set of sieves
J X on each object
- For every object
X, the maximal sieve is in
S ∈ J Xthen its pullback along any
h : Y ⟶ Xis in
S ∈ J Xand
Ris a sieve on
X, then provided that the pullback of
Ralong any arrow
f : Y ⟶ Xin
J Y, we have that
Ritself is in
X is referred to as
J-covering, (or just covering), if
S ∈ J X.
An extensionality lemma in terms of the coercion to a pi-type.
We prove this explicitly rather than deriving it so that it is in terms of the coercion rather than
S is a subset of
S is covering, then
R is covering as well.
The intersection of two covering sieves is covering.
J-covers an arrow
S.pullback f ∈ J Y.
This definition is an alternate way of presenting a Grothendieck topology.
The stability axiom in 'arrow' form: If
g ≫ f for any
The transitivity axiom in 'arrow' form: If
f and every arrow in
S is covered by
The trivial Grothendieck topology, in which only the maximal sieve is covering. This topology is also known as the indiscrete, coarse, or chaotic topology.
See [MM92] Chapter III, Section 2, example (a), or https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies
The discrete Grothendieck topology, in which every sieve is covering.
Construct a complete lattice from the
Inf, but make the trivial and discrete topologies
definitionally equal to the bottom and top respectively.
- category_theory.grothendieck_topology.complete_lattice = (complete_lattice_of_Inf (category_theory.grothendieck_topology C) category_theory.grothendieck_topology.is_glb_Inf).copy complete_lattice.le category_theory.grothendieck_topology.complete_lattice._proof_1 (category_theory.grothendieck_topology.discrete C) category_theory.grothendieck_topology.complete_lattice._proof_2 (category_theory.grothendieck_topology.trivial C) category_theory.grothendieck_topology.complete_lattice._proof_3 complete_lattice.sup category_theory.grothendieck_topology.complete_lattice._proof_4 complete_lattice.inf category_theory.grothendieck_topology.complete_lattice._proof_5 complete_lattice.Sup category_theory.grothendieck_topology.complete_lattice._proof_6 Inf category_theory.grothendieck_topology.complete_lattice._proof_7
The dense Grothendieck topology.
A category satisfies the right Ore condition if any span can be completed to a commutative square.
NB. Any category with pullbacks obviously satisfies the right Ore condition, see
The atomic Grothendieck topology: a sieve is covering iff it is nonempty. For the pullback stability condition, we need the right Ore condition to hold.