# Category instance for topological spaces #

We introduce the bundled category TopCat of topological spaces together with the functors TopCat.discrete and TopCat.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 Mathlib.Topology.Category.TopCat.Adjunctions.

def TopCat :
Type (u + 1)

The category of topological spaces and continuous maps.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• X.topologicalSpaceUnbundled = X.str
instance TopCat.instFunLike (X : TopCat) (Y : TopCat) :
FunLike (X Y) X Y
Equations
instance TopCat.instMonoidHomClass (X : TopCat) (Y : TopCat) :
ContinuousMapClass (X Y) X Y
Equations
• =
theorem TopCat.id_app (X : TopCat) (x : X) :
theorem TopCat.comp_app {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) (x : X) :
= g (f x)
@[simp]
theorem TopCat.coe_id (X : TopCat) :
@[simp]
theorem TopCat.coe_comp {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
= g f
@[simp]
theorem TopCat.hom_inv_id_apply {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :
f.inv (f.hom x) = x
@[simp]
theorem TopCat.inv_hom_id_apply {X : TopCat} {Y : TopCat} (f : X Y) (y : Y) :
f.hom (f.inv y) = y
def TopCat.of (X : Type u) [] :

Construct a bundled Top from the underlying type and the typeclass.

Equations
• = { α := X, str := inferInstance }
Instances For
Equations
• X.topologicalSpace_coe = X.str
@[reducible, inline]
Equations
• X.topologicalSpace_forget = X.str
@[simp]
theorem TopCat.coe_of (X : Type u) [] :
() = X
@[simp]
theorem TopCat.coe_of_of {X : Type u} {Y : Type u} [] [] {f : C(X, Y)} {x : .obj ()} :
f x = f x

Replace a function coercion for a morphism TopCat.of X ⟶ TopCat.of Y with the definitionally equal function coercion for a continuous map C(X, Y).

instance TopCat.inhabited :
Equations
theorem TopCat.hom_apply {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :
f x = f.toFun x

The discrete topology on any type.

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

The trivial topology on any type.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.isoOfHomeo_hom {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
.hom = f.toContinuousMap
@[simp]
theorem TopCat.isoOfHomeo_inv {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
.inv = f.symm.toContinuousMap
def TopCat.isoOfHomeo {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
X Y

Any homeomorphisms induces an isomorphism in Top.

Equations
• = { hom := f.toContinuousMap, inv := f.symm.toContinuousMap, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem TopCat.homeoOfIso_symm_apply {X : TopCat} {Y : TopCat} (f : X Y) (a : Y) :
.symm a = f.inv a
@[simp]
theorem TopCat.homeoOfIso_apply {X : TopCat} {Y : TopCat} (f : X Y) (a : X) :
a = f.hom a
def TopCat.homeoOfIso {X : TopCat} {Y : TopCat} (f : X Y) :
X ≃ₜ Y

Any isomorphism in Top induces a homeomorphism.

Equations
• = { toFun := f.hom, invFun := f.inv, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem TopCat.of_isoOfHomeo {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
@[simp]
theorem TopCat.of_homeoOfIso {X : TopCat} {Y : TopCat} (f : X Y) :
theorem TopCat.openEmbedding_iff_comp_isIso {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
@[simp]
theorem TopCat.openEmbedding_iff_comp_isIso' {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
theorem TopCat.openEmbedding_iff_isIso_comp {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :
@[simp]
theorem TopCat.openEmbedding_iff_isIso_comp' {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Y) (g : Y Z) :