Grothendieck topology on a topological space

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

• nLab, Grothendieck topology
• S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic

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.

def Opens.grothendieckTopology (T : Type u) [TopologicalSpace T] : CategoryTheory.GrothendieckTopology (TopologicalSpace.Opens T)

The Grothendieck topology associated to a topological space.

Equations

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

def Opens.pretopology (T : Type u) [TopologicalSpace T] : CategoryTheory.Pretopology (TopologicalSpace.Opens T)

The Grothendieck pretopology associated to a topological space.

Equations

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

@[simp]

theorem Opens.pretopology_ofGrothendieck (T : Type u) [TopologicalSpace T] : CategoryTheory.Pretopology.ofGrothendieck (TopologicalSpace.Opens T) (Opens.grothendieckTopology T) = Opens.pretopology T

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

@[simp]

theorem Opens.pretopology_toGrothendieck (T : Type u) [TopologicalSpace T] : CategoryTheory.Pretopology.toGrothendieck (TopologicalSpace.Opens T) (Opens.pretopology T) = Opens.grothendieckTopology T

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