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

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

theorem CategoryTheory.Pretopology.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasPullbacks C} (x y : CategoryTheory.Pretopology C), x = y ↔ x.coverings = y.coverings

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) → CategoryTheory.Presieve.bind S Ti ∈ self.coverings X

instance CategoryTheory.Pretopology.instCoeFunPretopologyForAllSetPresieve (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.instCoeFunPretopologyForAllSetPresieve 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₁ : CategoryTheory.Pretopology C} {K₂ : CategoryTheory.Pretopology C} : K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings

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

Equations

• CategoryTheory.Pretopology.instPartialOrderPretopology C = let src := CategoryTheory.Pretopology.LE; PartialOrder.mk (_ : ∀ (K₁ K₂ : CategoryTheory.Pretopology C), K₁ ≤ K₂ → K₂ ≤ K₁ → K₁ = K₂)

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

Equations

• CategoryTheory.Pretopology.instOrderTopPretopologyLE C = OrderTop.mk (_ : ∀ (x : CategoryTheory.Pretopology C) (x_1 : C), ∀ x_2 ∈ x.coverings x_1, x_2 ∈ Set.univ)

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

Equations

• CategoryTheory.Pretopology.instInhabitedPretopology 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 , 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).sieves 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.

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

Equations

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

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

Equations

• CategoryTheory.Pretopology.instOrderBotPretopologyLE C = OrderBot.mk (_ : ∀ (K : CategoryTheory.Pretopology C) (X : C), ∀ R ∈ ⊥.coverings X, R ∈ K.coverings X)

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.