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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.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 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.

• coverings : (X : C) → Set (CategoryTheory.Presieve X)
• has_isos : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [inst : CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ self.coverings X
• pullbacks : ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ self.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ self.coverings Y
• transitive : ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.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✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasPullbacks C} {x y : CategoryTheory.Pretopology C} (coverings : x.coverings = y.coverings) : x = y

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

Equations

• CategoryTheory.Pretopology.instCoeFunForallSetPresieve C = { coe := CategoryTheory.Pretopology.coverings }

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

Equations

• CategoryTheory.Pretopology.LE = { le := fun (K₁ K₂ : CategoryTheory.Pretopology C) => K₁.coverings ≤ K₂.coverings }

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

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

Equations

• CategoryTheory.Pretopology.instPartialOrder C = PartialOrder.mk ⋯

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

Equations

• CategoryTheory.Pretopology.orderTop C = OrderTop.mk ⋯

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

Equations

• CategoryTheory.Pretopology.instInhabited C = { default := ⊤ }

def CategoryTheory.Pretopology.toGrothendieck (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C) : CategoryTheory.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 https://stacks.math.columbia.edu/tag/00ZC, or [MM92] Chapter III, Section 2, Equation (2).

Equations

• One or more equations did not get rendered due to their size.

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

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

The largest pretopology generating the given Grothendieck topology.

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

Equations

• One or more equations did not get rendered due to their size.

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

We have a galois insertion from pretopologies to Grothendieck topologies.

Equations

• One or more equations did not get rendered due to their size.

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

def CategoryTheory.Pretopology.trivial (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.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.

See https://stacks.math.columbia.edu/tag/07GE

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Pretopology.orderBot C = OrderBot.mk ⋯

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

The trivial pretopology induces the trivial grothendieck topology.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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

Equations

• CategoryTheory.Pretopology.instCompleteLattice C = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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