Grothendieck topology on a topological space #

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

Define the Grothendieck topology and the pretopology associated to a topological space, and show that the pretopology induces the topology.

The covering (pre)sieves on X are those for which the union of domains contains X.

Tags #

site, Grothendieck topology, space

References #

Implementation notes #

We define the two separately, rather than defining the Grothendieck topology as that generated by the pretopology for the purpose of having nice definitional properties for the sieves.

source

def opens.grothendieck_topology (T : Type u) [topological_space T] :

category_theory.grothendieck_topology (topological_space.opens T)

The Grothendieck topology associated to a topological space.

Equations

opens.grothendieck_topology T = {sieves := λ (X : topological_space.opens T) (S : category_theory.sieve X), ∀ (x : T), x ∈ X → (∃ (U : topological_space.opens T) (f : U ⟶ X), ⇑S f ∧ x ∈ U), top_mem' := _, pullback_stable' := _, transitive' := _}

source

def opens.pretopology (T : Type u) [topological_space T] :

category_theory.pretopology (topological_space.opens T)

The Grothendieck pretopology associated to a topological space.

Equations

opens.pretopology T = {coverings := λ (X : topological_space.opens T) (R : category_theory.presieve X), ∀ (x : T), x ∈ X → (∃ (U : topological_space.opens T) (f : U ⟶ X), R f ∧ x ∈ U), has_isos := _, pullbacks := _, transitive := _}

source

@[simp]

theorem opens.pretopology_of_grothendieck (T : Type u) [topological_space T] :

category_theory.pretopology.of_grothendieck (topological_space.opens T) (opens.grothendieck_topology T) = opens.pretopology T

The pretopology associated to a space is the largest pretopology that generates the Grothendieck topology associated to the space.

source

@[simp]

theorem opens.pretopology_to_grothendieck (T : Type u) [topological_space T] :

category_theory.pretopology.to_grothendieck (topological_space.opens T) (opens.pretopology T) = opens.grothendieck_topology T

The pretopology associated to a space induces the Grothendieck topology associated to the space.