Basic facts about colimits in TopCat #
The initial object of TopCat is empty, through Mathlib's isomorphism TopCat.initialIsoPEmpty.
As an instance, this makes the separation properties of the empty space, such as being Hausdorff,
available for it by instance search. It is the base of every CW complex in Mathlib's categorical
sense, TopCat.CWComplex X, which is a relative CW complex over the map out of ⊥_ TopCat.
A directed colimit in TopCat along injective transition maps has injective colimit maps
(TauCeti.TopCat.injective_ι_of_isColimit), since the forgetful functor to types preserves it.
theorem
TauCeti.TopCat.injective_ι_of_isColimit
{J : Type w}
[Preorder J]
[IsDirectedOrder J]
{F : CategoryTheory.Functor J TopCat}
(hF :
∀ ⦃i j : J⦄ (hij : i ≤ j),
Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij))))
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
(i : J)
:
If all transition maps of a directed diagram in TopCat are injective, then so are the maps
from the objects of the diagram to its colimit.