The Grothendieck topology on TopCat

In this file we define the standard Grothendieck topology on TopCat. This is the topology generated by families of jointly surjective open embeddings.

Main definitions and results

• TopCat.isOpenEmbedding: The morphism property in TopCat given by open embeddings.
• TopCat.grothendieckTopology: The Grothendieck topology generated by families of jointly surjective open embeddings.
• TopCat.subcanonical_grothendieckTopology: The Grothendieck topology on TopCat is subcanonical.

TODOs

• Define the étale precoverage on TopCat (replace open embedding by local homeomorphism in the definition of the Grothendieck topology) and show it induces the same Grothendieck topology.

def TopCat.isOpenEmbedding : CategoryTheory.MorphismProperty TopCat

The morphism property on the category of topological spaces given by open embeddings.

@[simp]

theorem TopCat.isOpenEmbedding_iff {X Y : TopCat} (f : X ⟶ Y) : isOpenEmbedding f ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

instance TopCat.instIsMultiplicativeIsOpenEmbedding : isOpenEmbedding.IsMultiplicative

instance TopCat.instRespectsIsoIsOpenEmbedding : isOpenEmbedding.RespectsIso

instance TopCat.instIsStableUnderBaseChangeIsOpenEmbedding : isOpenEmbedding.IsStableUnderBaseChange

def TopCat.precoverage : CategoryTheory.Precoverage TopCat

The precoverage on TopCat given by jointly surjective families of open embeddings.

instance TopCat.instHasIsosPrecoverage : precoverage.HasIsos

instance TopCat.instIsStableUnderBaseChangePrecoverage : precoverage.IsStableUnderBaseChange

instance TopCat.instIsStableUnderCompositionPrecoverage : precoverage.IsStableUnderComposition

@[reducible, inline]

abbrev TopCat.grothendieckTopology : CategoryTheory.GrothendieckTopology TopCat

The Grothendieck topology on the category of topological spaces is the topology given by jointly surjective open embeddings.

theorem TopCat.exists_mem_zeroHypercover_range {X : TopCat} (E : precoverage.ZeroHypercover X) (x : ↑X) : ∃ (i : E.I₀), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))

theorem TopCat.isOpenEmbedding_f_zeroHypercover {X : TopCat} (E : precoverage.ZeroHypercover X) (i : E.I₀) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))

instance TopCat.instSmallPrecoverage : precoverage.Small

instance TopCat.subcanonical_grothendieckTopology : grothendieckTopology.Subcanonical

The Grothendieck topology on TopCat is subcanonical.