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 #

theorem CategoryTheory.Pretopology.ext_iff {C : Type u} :
∀ {inst : } {inst_1 : } (x y : ), x = y x.coverings = y.coverings
theorem CategoryTheory.Pretopology.ext {C : Type u} :
∀ {inst : } {inst_1 : } (x y : ), x.coverings = y.coveringsx = y
structure CategoryTheory.Pretopology (C : Type u) :
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) →
• has_isos : ∀ ⦃X Y : C⦄ (f : Y X) [inst : ], self.coverings X
• pullbacks : ∀ ⦃X Y : C⦄ (f : Y X), Sself.coverings X, self.coverings Y
• transitive : ∀ ⦃X : C⦄ (S : ) (Ti : Y : C⦄ → (f : Y X) → S f), S self.coverings X(∀ ⦃Y : C⦄ (f : Y X) (H : S f), Ti f H self.coverings Y)S.bind Ti self.coverings X
Instances For
theorem CategoryTheory.Pretopology.has_isos {C : Type u} (self : ) ⦃X : C ⦃Y : C (f : Y X) :
self.coverings X
theorem CategoryTheory.Pretopology.pullbacks {C : Type u} (self : ) ⦃X : C ⦃Y : C (f : Y X) (S : ) :
S self.coverings X self.coverings Y
theorem CategoryTheory.Pretopology.transitive {C : Type u} (self : ) ⦃X : C (S : ) (Ti : Y : C⦄ → (f : Y X) → S f) :
S self.coverings X(∀ ⦃Y : C⦄ (f : Y X) (H : S f), Ti f H self.coverings Y)S.bind Ti self.coverings X
instance CategoryTheory.Pretopology.instCoeFunForallSetPresieve (C : Type u) :
CoeFun fun (x : ) => (X : C) →
Equations
• = { coe := CategoryTheory.Pretopology.coverings }
Equations
• CategoryTheory.Pretopology.LE = { le := fun (K₁ K₂ : ) => K₁.coverings K₂.coverings }
theorem CategoryTheory.Pretopology.le_def {C : Type u} {K₁ : } {K₂ : } :
K₁ K₂ K₁.coverings K₂.coverings
Equations
• = let __src := CategoryTheory.Pretopology.LE;
Equations
Equations
• = { default := }

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.
Instances For
theorem CategoryTheory.Pretopology.mem_toGrothendieck (C : Type u) (K : ) (X : C) (S : ) :
S .sieves X RK.coverings X, R S.arrows

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.
Instances For

We have a galois insertion from pretopologies to Grothendieck topologies.

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

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

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

The trivial pretopology induces the trivial grothendieck topology.