Grothendieck topologies #
Definition and lemmas about Grothendieck topologies.
A Grothendieck topology for a category C
is a set of sieves on each object X
satisfying
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 spaces.lean
.
Tags #
Grothendieck topology, coverage, pretopology, site
References #
Implementation notes #
We use the definition of [nlab] and [MM92][] (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 X
satisfying
three axioms:
- For every object
X
, the maximal sieve is inJ X
. - If
S ∈ J X
then its pullback along anyh : Y ⟶ X
is inJ Y
. - If
S ∈ J X
andR
is a sieve onX
, then provided that the pullback ofR
along any arrowf : Y ⟶ X
inS
is inJ Y
, we have thatR
itself is inJ X
.
A sieve S
on X
is referred to as J
-covering, (or just covering), if S ∈ J X
.
See https://stacks.math.columbia.edu/tag/00Z4, or [nlab], or [MM92][] Chapter III, Section 2, Definition 1.
Instances for category_theory.grothendieck_topology
- category_theory.grothendieck_topology.has_sizeof_inst
- category_theory.grothendieck_topology.has_coe_to_fun
- category_theory.grothendieck_topology.has_le
- category_theory.grothendieck_topology.partial_order
- category_theory.grothendieck_topology.has_Inf
- category_theory.grothendieck_topology.complete_lattice
- category_theory.grothendieck_topology.inhabited
Equations
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
the projection .sieves
.
If S
is a subset of R
, and S
is covering, then R
is covering as well.
See https://stacks.math.columbia.edu/tag/00Z5 (2), or discussion after [MM92] Chapter III, Section 2, Definition 1.
The intersection of two covering sieves is covering.
See https://stacks.math.columbia.edu/tag/00Z5 (1), or [MM92] Chapter III, Section 2, Definition 1 (iv).
The sieve S
on X
J
-covers an arrow f
to X
if S.pullback f ∈ J Y
.
This definition is an alternate way of presenting a Grothendieck topology.
Equations
- J.covers S f = (category_theory.sieve.pullback f S ∈ ⇑J Y)
The maximality axiom in 'arrow' form: Any arrow f
in S
is covered by S
.
The stability axiom in 'arrow' form: If S
covers f
then S
covers g ≫ f
for any g
.
The transitivity axiom in 'arrow' form: If S
covers f
and every arrow in S
is covered by
R
, then R
covers f
.
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
Equations
- category_theory.grothendieck_topology.trivial C = {sieves := λ (X : C), {⊤}, top_mem' := _, pullback_stable' := _, transitive' := _}
The discrete Grothendieck topology, in which every sieve is covering.
See https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies.
Equations
- category_theory.grothendieck_topology.discrete C = {sieves := λ (X : C), set.univ, top_mem' := _, pullback_stable' := _, transitive' := _}
See https://stacks.math.columbia.edu/tag/00Z6
Equations
- category_theory.grothendieck_topology.has_le = {le := λ (J₁ J₂ : category_theory.grothendieck_topology C), ⇑J₁ ≤ ⇑J₂}
See https://stacks.math.columbia.edu/tag/00Z6
Equations
- category_theory.grothendieck_topology.partial_order = {le := has_le.le category_theory.grothendieck_topology.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
See https://stacks.math.columbia.edu/tag/00Z7
Equations
- category_theory.grothendieck_topology.has_Inf = {Inf := λ (T : set (category_theory.grothendieck_topology C)), {sieves := has_Inf.Inf (category_theory.grothendieck_topology.sieves '' T), top_mem' := _, pullback_stable' := _, transitive' := _}}
Construct a complete lattice from the Inf
, but make the trivial and discrete topologies
definitionally equal to the bottom and top respectively.
Equations
- 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 has_Inf.Inf category_theory.grothendieck_topology.complete_lattice._proof_7
Equations
The dense Grothendieck topology.
See https://ncatlab.org/nlab/show/dense+topology, or [MM92] Chapter III, Section 2, example (e).
Equations
- category_theory.grothendieck_topology.dense = {sieves := λ (X : C) (S : category_theory.sieve X), ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), ⇑S (g ≫ f), top_mem' := _, pullback_stable' := _, transitive' := _}
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
right_ore_of_pullbacks
.
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.
See https://ncatlab.org/nlab/show/atomic+site, or [MM92] Chapter III, Section 2, example (f).
Equations
- category_theory.grothendieck_topology.atomic hro = {sieves := λ (X : C) (S : category_theory.sieve X), ∃ (Y : C) (f : Y ⟶ X), ⇑S f, top_mem' := _, pullback_stable' := _, transitive' := _}
J.cover X
denotes the poset of covers of X
with respect to the
Grothendieck topology J
.
Instances for category_theory.grothendieck_topology.cover
- category_theory.grothendieck_topology.cover.preorder
- category_theory.grothendieck_topology.cover.category_theory.sieve.has_coe
- category_theory.grothendieck_topology.cover.has_coe_to_fun
- category_theory.grothendieck_topology.cover.order_top
- category_theory.grothendieck_topology.cover.semilattice_inf
- category_theory.grothendieck_topology.cover.inhabited
- category_theory.grothendieck_topology.cover.is_cofiltered
Equations
- category_theory.grothendieck_topology.cover.semilattice_inf = {inf := λ (S T : J.cover X), ⟨↑S ⊓ ↑T, _⟩, le := preorder.le infer_instance, lt := preorder.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
An auxiliary structure, used to define S.index
in plus.lean
.
Instances for category_theory.grothendieck_topology.cover.arrow
- category_theory.grothendieck_topology.cover.arrow.has_sizeof_inst
- Y₁ : C
- Y₂ : C
- Z : C
- g₁ : self.Z ⟶ self.Y₁
- g₂ : self.Z ⟶ self.Y₂
- f₁ : self.Y₁ ⟶ X
- f₂ : self.Y₂ ⟶ X
- h₁ : ⇑S self.f₁
- h₂ : ⇑S self.f₂
- w : self.g₁ ≫ self.f₁ = self.g₂ ≫ self.f₂
An auxiliary structure, used to define S.index
in plus.lean
.
Instances for category_theory.grothendieck_topology.cover.relation
- category_theory.grothendieck_topology.cover.relation.has_sizeof_inst
Map a arrow
along a refinement S ⟶ T
.
Map a relation
along a refinement S ⟶ T
.
The first arrow
associated to a relation
.
Used in defining index
in plus.lean
.
The second arrow
associated to a relation
.
Used in defining index
in plus.lean
.
Pull back a cover along a morphism.
Equations
- S.pullback f = ⟨category_theory.sieve.pullback f ↑S, _⟩
An arrow of S.pullback f
gives rise to an arrow of S
.
A relation of S.pullback f
gives rise to a relation of S
.
The isomorphism between S
and the pullback of S
w.r.t. the identity.
Equations
Pulling back with respect to a composition is the composition of the pullbacks.
Equations
- S.pullback_comp f g = category_theory.eq_to_iso _
Combine a family of covers over a cover.
The canonical moprhism from S.bind T
to T
.
Equations
An arrow in bind has the form A ⟶ B ⟶ X
where A ⟶ B
is an arrow in T I
for some I
.
and B ⟶ X
is an arrow of S
. This is the object B
.
Equations
- I.middle = Exists.some _
An arrow in bind has the form A ⟶ B ⟶ X
where A ⟶ B
is an arrow in T I
for some I
.
and B ⟶ X
is an arrow of S
. This is the hom A ⟶ B
.
Equations
An arrow in bind has the form A ⟶ B ⟶ X
where A ⟶ B
is an arrow in T I
for some I
.
and B ⟶ X
is an arrow of S
. This is the hom B ⟶ X
.
Equations
An arrow in bind has the form A ⟶ B ⟶ X
where A ⟶ B
is an arrow in T I
for some I
.
and B ⟶ X
is an arrow of S
. This is the hom B ⟶ X
, as an arrow.
Equations
- I.from_middle = {Y := I.middle, f := I.from_middle_hom, hf := _}
An arrow in bind has the form A ⟶ B ⟶ X
where A ⟶ B
is an arrow in T I
for some I
.
and B ⟶ X
is an arrow of S
. This is the hom A ⟶ B
, as an arrow.
To every S : J.cover X
and presheaf P
, associate a multicospan_index
.
Equations
- S.index P = {L := S.arrow, R := S.relation, fst_to := λ (I : S.relation), I.fst, snd_to := λ (I : S.relation), I.snd, left := λ (I : S.arrow), P.obj (opposite.op I.Y), right := λ (I : S.relation), P.obj (opposite.op I.Z), fst := λ (I : S.relation), P.map I.g₁.op, snd := λ (I : S.relation), P.map I.g₂.op}
The natural multifork associated to S : J.cover X
for a presheaf P
.
Saying that this multifork is a limit is essentially equivalent to the sheaf condition at the
given object for the given covering sieve. See sheaf.lean
for an equivalent sheaf condition
using this.
The canonical map from P.obj (op X)
to the multiequalizer associated to a covering sieve,
assuming such a multiequalizer exists. This will be used in sheaf.lean
to provide an equivalent
sheaf condition in terms of multiequalizers.
Pull back a cover along a morphism.
Pulling back along the identity is naturally isomorphic to the identity functor.
Equations
- J.pullback_id X = category_theory.nat_iso.of_components (λ (S : J.cover X), S.pullback_id) _
Pulling back along a composition is naturally isomorphic to the composition of the pullbacks.
Equations
- J.pullback_comp f g = category_theory.nat_iso.of_components (λ (S : J.cover Z), S.pullback_comp f g) _