Documentation

Mathlib.Topology.Category.TopCat.GrothendieckTopology

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.

Instances For

@[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.

Instances For

@[implicit_reducible]

instance TopCat.instHasIsosPrecoverage :

precoverage.HasIsos

@[implicit_reducible]

instance TopCat.instIsStableUnderBaseChangePrecoverage :

precoverage.IsStableUnderBaseChange

@[implicit_reducible]

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.

Instances For

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.

theorem TopCat.precoverage_le_comap_uliftFunctor :

precoverage ≤ CategoryTheory.Precoverage.comap uliftFunctor precoverage

instance TopCat.instIsContinuousUliftFunctorGrothendieckTopology :

uliftFunctor.IsContinuous grothendieckTopology grothendieckTopology