Category instance for topological spaces #
We introduce the bundled category TopCat
of topological spaces together with the functors
discrete
and trivial
from the category of types to TopCat
which equip a type with the
corresponding discrete, resp. trivial, topology. For a proof that these functors are left,
resp. right adjoint to the forgetful functor, see topology.category.TopCat.adjunctions
.
theorem
TopCat.comp_app
{X : TopCat}
{Y : TopCat}
{Z : TopCat}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(x : ↑X)
:
↑(CategoryTheory.CategoryStruct.comp f g) x = ↑g (↑f x)
@[reducible]
instance
TopCat.topologicalSpace_forget
(X : TopCat)
:
TopologicalSpace ((CategoryTheory.forget TopCat).obj X)
theorem
TopCat.hom_apply
{X : TopCat}
{Y : TopCat}
(f : X ⟶ Y)
(x : ↑X)
:
↑f x = ContinuousMap.toFun f x
The discrete topology on any type.
Instances For
The trivial topology on any type.
Instances For
@[simp]
theorem
TopCat.isoOfHomeo_hom
{X : TopCat}
{Y : TopCat}
(f : ↑X ≃ₜ ↑Y)
:
(TopCat.isoOfHomeo f).hom = Homeomorph.toContinuousMap f
@[simp]
theorem
TopCat.isoOfHomeo_inv
{X : TopCat}
{Y : TopCat}
(f : ↑X ≃ₜ ↑Y)
:
(TopCat.isoOfHomeo f).inv = Homeomorph.toContinuousMap (Homeomorph.symm f)
@[simp]
theorem
TopCat.homeoOfIso_apply
{X : TopCat}
{Y : TopCat}
(f : X ≅ Y)
(a : (CategoryTheory.forget TopCat).obj X)
:
↑(TopCat.homeoOfIso f) a = ↑f.hom a
@[simp]
theorem
TopCat.homeoOfIso_symm_apply
{X : TopCat}
{Y : TopCat}
(f : X ≅ Y)
(a : (CategoryTheory.forget TopCat).obj Y)
:
↑(Homeomorph.symm (TopCat.homeoOfIso f)) a = ↑f.inv a
@[simp]
@[simp]
theorem
TopCat.openEmbedding_iff_comp_isIso
{X : TopCat}
{Y : TopCat}
{Z : TopCat}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
@[simp]
theorem
TopCat.openEmbedding_iff_comp_isIso'
{X : TopCat}
{Y : TopCat}
{Z : TopCat}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso g]
:
OpenEmbedding
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget TopCat).map f) ((CategoryTheory.forget TopCat).map g)) ↔ OpenEmbedding ↑f
theorem
TopCat.openEmbedding_iff_isIso_comp
{X : TopCat}
{Y : TopCat}
{Z : TopCat}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
@[simp]
theorem
TopCat.openEmbedding_iff_isIso_comp'
{X : TopCat}
{Y : TopCat}
{Z : TopCat}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
:
OpenEmbedding
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget TopCat).map f) ((CategoryTheory.forget TopCat).map g)) ↔ OpenEmbedding ↑g