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
• Stacks, 00VG

structure CategoryTheory.Pretopology (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] extends CategoryTheory.Precoverage 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 [MLM92] Chapter III, Section 2, Definition 2.

• coverings (X : C) : Set (Presieve X)
• has_isos ⦃X Y : C⦄ (f : Y ⟶ X) [IsIso f] : Presieve.singleton f ∈ self.coverings X

  For all X : C, the coverings of X (sets of families of morphisms with target 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_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : Limits.HasPullbacks C} {x y : Pretopology C} : x = y ↔ x.coverings = y.coverings

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

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)

Equations

• CategoryTheory.Pretopology.instCoeFunForallSetPresieve C = { coe := fun (J : CategoryTheory.Pretopology C) => J.coverings }

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

Equations

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

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

Equations

• CategoryTheory.Pretopology.orderTop C = { top := { coverings := fun (x : C) => Set.univ, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }, le_top := ⋯ }

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

Equations

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

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 [MLM92] Chapter III, Section 2, Equation (2).

Equations

• K.toGrothendieck = { sieves := fun (X : C) (S : CategoryTheory.Sieve X) => ∃ R ∈ K.coverings X, R ≤ S.arrows, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

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

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

The largest pretopology generating the given Grothendieck topology.

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

Equations

• J.toPretopology = { coverings := fun (X : C) => {R : CategoryTheory.Presieve X | CategoryTheory.Sieve.generate R ∈ J X}, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }

@[deprecated CategoryTheory.GrothendieckTopology.toPretopology (since := "2025-09-19")]

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

Alias of CategoryTheory.GrothendieckTopology.toPretopology.

---

The largest pretopology generating the given Grothendieck topology.

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

Equations

• @CategoryTheory.Pretopology.ofGrothendieck = @CategoryTheory.GrothendieckTopology.toPretopology

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

We have a Galois insertion from pretopologies to Grothendieck topologies.

Equations

• CategoryTheory.Pretopology.gi C = { choice := fun (x : CategoryTheory.Pretopology C) (x_1 : x.toGrothendieck.toPretopology ≤ x) => x.toGrothendieck, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

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

@[deprecated CategoryTheory.GrothendieckTopology.mem_toPretopology (since := "2025-09-19")]

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

Alias of CategoryTheory.GrothendieckTopology.mem_toPretopology.

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.

Equations

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

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

Equations

• CategoryTheory.Pretopology.orderBot C = { bot := CategoryTheory.Pretopology.trivial C, bot_le := ⋯ }

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

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)

Equations

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

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)) : (sInf T).toPretopology = sInf (GrothendieckTopology.toPretopology '' 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 ⊓.

Equations

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

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

def CategoryTheory.Precoverage.toPretopology (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (J : Precoverage C) [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] : Pretopology C

If J is a precoverage that has isomorphisms and is stable under composition and base change, it defines a pretopology.

Equations

• CategoryTheory.Precoverage.toPretopology C J = { toPrecoverage := J, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }

@[simp]

theorem CategoryTheory.Precoverage.toPretopology_toPrecoverage (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] (J : Precoverage C) [J.HasIsos] [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] : (toPretopology C J).toPrecoverage = J