Grothendieck pretopologies #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source

theorem category_theory.pretopology.ext {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_pullbacks C} (x y : category_theory.pretopology C) (h : x.coverings = y.coverings) :

x = y

source

theorem category_theory.pretopology.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.limits.has_pullbacks C} (x y : category_theory.pretopology C) :

x = y ↔ x.coverings = y.coverings

source

@[ext]

structure category_theory.pretopology (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

Type (max u v)

coverings : Π (X : C), set (category_theory.presieve X)
has_isos : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [_inst_3 : category_theory.is_iso f], category_theory.presieve.singleton f ∈ self.coverings X
pullbacks : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : category_theory.presieve X), S ∈ self.coverings X → category_theory.presieve.pullback_arrows f S ∈ self.coverings Y
transitive : ∀ ⦃X : C⦄ (S : category_theory.presieve X) (Ti : Π ⦃Y : C⦄ (f : Y ⟶ X), S f → category_theory.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

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:

Every family consisting of a single isomorphism is a covering family.
The collection of covering families is stable under pullback.
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.

Instances for category_theory.pretopology

category_theory.pretopology.has_sizeof_inst
category_theory.pretopology.has_coe_to_fun
category_theory.pretopology.has_le
category_theory.pretopology.partial_order
category_theory.pretopology.order_top
category_theory.pretopology.inhabited
category_theory.pretopology.order_bot

source

@[protected, instance]

def category_theory.pretopology.has_coe_to_fun (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

has_coe_to_fun (category_theory.pretopology C) (λ (_x : category_theory.pretopology C), Π (X : C), set (category_theory.presieve X))

Equations

category_theory.pretopology.has_coe_to_fun C = {coe := category_theory.pretopology.coverings _inst_2}

source

@[protected, instance]

def category_theory.pretopology.has_le {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] :

has_le (category_theory.pretopology C)

Equations

category_theory.pretopology.has_le = {le := λ (K₁ K₂ : category_theory.pretopology C), ⇑K₁ ≤ ⇑K₂}

source

theorem category_theory.pretopology.le_def {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {K₁ K₂ : category_theory.pretopology C} :

K₁ ≤ K₂ ↔ ⇑K₁ ≤ ⇑K₂

source

@[protected, instance]

def category_theory.pretopology.partial_order (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

partial_order (category_theory.pretopology C)

Equations

category_theory.pretopology.partial_order C = {le := has_le.le category_theory.pretopology.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def category_theory.pretopology.order_top (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

order_top (category_theory.pretopology C)

Equations

category_theory.pretopology.order_top C = {top := {coverings := λ (_x : C), set.univ, has_isos := _, pullbacks := _, transitive := _}, le_top := _}

source

@[protected, instance]

def category_theory.pretopology.inhabited (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

inhabited (category_theory.pretopology C)

Equations

category_theory.pretopology.inhabited C = {default := ⊤}

source

def category_theory.pretopology.to_grothendieck (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] (K : category_theory.pretopology C) :

category_theory.grothendieck_topology 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

category_theory.pretopology.to_grothendieck C K = {sieves := λ (X : C) (S : category_theory.sieve X), ∃ (R : category_theory.presieve X) (H : R ∈ ⇑K X), R ≤ ⇑S, top_mem' := _, pullback_stable' := _, transitive' := _}

source

theorem category_theory.pretopology.mem_to_grothendieck (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] (K : category_theory.pretopology C) (X : C) (S : category_theory.sieve X) :

S ∈ ⇑(category_theory.pretopology.to_grothendieck C K) X ↔ ∃ (R : category_theory.presieve X) (H : R ∈ ⇑K X), R ≤ ⇑S

source

def category_theory.pretopology.of_grothendieck (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] (J : category_theory.grothendieck_topology C) :

category_theory.pretopology C

The largest pretopology generating the given Grothendieck topology.

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

Equations

category_theory.pretopology.of_grothendieck C J = {coverings := λ (X : C) (R : category_theory.presieve X), category_theory.sieve.generate R ∈ ⇑J X, has_isos := _, pullbacks := _, transitive := _}

source

def category_theory.pretopology.gi (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

galois_insertion (category_theory.pretopology.to_grothendieck C) (category_theory.pretopology.of_grothendieck C)

We have a galois insertion from pretopologies to Grothendieck topologies.

Equations

category_theory.pretopology.gi C = {choice := λ (x : category_theory.pretopology C) (hx : category_theory.pretopology.of_grothendieck C (category_theory.pretopology.to_grothendieck C x) ≤ x), category_theory.pretopology.to_grothendieck C x, gc := _, le_l_u := _, choice_eq := _}

source

def category_theory.pretopology.trivial (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

category_theory.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

category_theory.pretopology.trivial C = {coverings := λ (X : C) (S : category_theory.presieve X), ∃ (Y : C) (f : Y ⟶ X) (h : category_theory.is_iso f), S = category_theory.presieve.singleton f, has_isos := _, pullbacks := _, transitive := _}

source

@[protected, instance]

def category_theory.pretopology.order_bot (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

order_bot (category_theory.pretopology C)

Equations

category_theory.pretopology.order_bot C = {bot := category_theory.pretopology.trivial C _inst_2, bot_le := _}

source

theorem category_theory.pretopology.to_grothendieck_bot (C : Type u) [category_theory.category C] [category_theory.limits.has_pullbacks C] :

category_theory.pretopology.to_grothendieck C ⊥ = ⊥

The trivial pretopology induces the trivial grothendieck topology.