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 Spaces.lean.

Tags

coverage, pretopology, site

References

• nLab, Grothendieck pretopology
• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
• Stacks, 00VG

structure CategoryTheory.Pretopology (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : Type (max u v)

A (Grothendieck) pretopology on C consists of a collection of families of morphisms with a fixed target X for every object X in C, called "coverings" of X, which satisfies the following three axioms:

1. Every family consisting of a single isomorphism is a covering family.
2. The collection of covering families is stable under pullback.
3. 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 [MM92] Chapter III, Section 2, Definition 2.

• coverings (X : C) : Set (Presieve X)

  For all X : C, the coverings of X (sets of families of morphisms with target X)

• has_isos ⦃X Y : C⦄ (f : Y ⟶ X) [IsIso f] : Presieve.singleton f ∈ self.coverings X
• pullbacks ⦃X Y : C⦄ (f : Y ⟶ X) (S : Presieve X) : S ∈ self.coverings X → Presieve.pullbackArrows f S ∈ self.coverings Y
• transitive ⦃X : C⦄ (S : Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → 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

theorem CategoryTheory.Pretopology.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : Limits.HasPullbacks C} {x y : Pretopology C} (coverings : x.coverings = y.coverings) : x = y

theorem CategoryTheory.Pretopology.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : Limits.HasPullbacks C} {x y : Pretopology C} : x = y ↔ x.coverings = y.coverings

instance CategoryTheory.Pretopology.instCoeFunForallSetPresieve (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : CoeFun (Pretopology C) fun (x : Pretopology C) => (X : C) → Set (Presieve X)

instance CategoryTheory.Pretopology.LE {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] : _root_.LE (Pretopology C)

theorem CategoryTheory.Pretopology.le_def {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {K₁ K₂ : Pretopology C} : K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings

instance CategoryTheory.Pretopology.instPartialOrder (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : PartialOrder (Pretopology C)

instance CategoryTheory.Pretopology.orderTop (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : OrderTop (Pretopology C)

instance CategoryTheory.Pretopology.instInhabited (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : Inhabited (Pretopology C)

def CategoryTheory.Pretopology.toGrothendieck (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (K : Pretopology C) : GrothendieckTopology C

A pretopology K can be completed to a Grothendieck topology J by declaring a sieve to be J-covering if it contains a family in K.

See also [MM92] Chapter III, Section 2, Equation (2).

Stacks Tag 00ZC

theorem CategoryTheory.Pretopology.mem_toGrothendieck (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (K : Pretopology C) (X : C) (S : Sieve X) : S ∈ (toGrothendieck C K) X ↔ ∃ R ∈ K.coverings X, R ≤ S.arrows

def CategoryTheory.Pretopology.ofGrothendieck (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (J : GrothendieckTopology C) : Pretopology C

The largest pretopology generating the given Grothendieck topology.

See [MM92] Chapter III, Section 2, Equations (3,4).

def CategoryTheory.Pretopology.gi (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : GaloisInsertion (toGrothendieck C) (ofGrothendieck C)

We have a galois insertion from pretopologies to Grothendieck topologies.

theorem CategoryTheory.Pretopology.mem_ofGrothendieck (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (t : GrothendieckTopology C) {X : C} (S : Presieve X) : S ∈ (ofGrothendieck C t).coverings X ↔ Sieve.generate S ∈ t X

def CategoryTheory.Pretopology.trivial (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : Pretopology C

The trivial pretopology, in which the coverings are exactly singleton isomorphisms. This topology is also known as the indiscrete, coarse, or chaotic topology.

Stacks Tag 07GE

instance CategoryTheory.Pretopology.orderBot (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : OrderBot (Pretopology C)

theorem CategoryTheory.Pretopology.toGrothendieck_bot (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : toGrothendieck C ⊥ = ⊥

The trivial pretopology induces the trivial grothendieck topology.

instance CategoryTheory.Pretopology.instInfSet (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : InfSet (Pretopology C)

theorem CategoryTheory.Pretopology.mem_sInf (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (T : Set (Pretopology C)) {X : C} (S : Presieve X) : S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X

theorem CategoryTheory.Pretopology.sInf_ofGrothendieck (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (T : Set (GrothendieckTopology C)) : ofGrothendieck C (sInf T) = sInf (ofGrothendieck C '' T)

theorem CategoryTheory.Pretopology.isGLB_sInf (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (T : Set (Pretopology C)) : IsGLB T (sInf T)

instance CategoryTheory.Pretopology.instCompleteLattice (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : CompleteLattice (Pretopology C)

The complete lattice structure on pretopologies. This is induced by the InfSet instance, but with good definitional equalities for ⊥, ⊤ and ⊓.

theorem CategoryTheory.Pretopology.mem_inf (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (t₁ t₂ : Pretopology C) {X : C} (S : Presieve X) : S ∈ (t₁ ⊓ t₂).coverings X ↔ S ∈ t₁.coverings X ∧ S ∈ t₂.coverings X