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
.
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
- TopCat.instCoeSortType = { coe := fun (X : TopCat) => ↑X }
Equations
- X.topologicalSpaceUnbundled = X.str
Equations
- ⋯ = ⋯
Equations
- X.topologicalSpace_coe = X.str
Equations
- X.topologicalSpace_forget = X.str
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)
.
Equations
- TopCat.inhabited = { default := TopCat.of Empty }
The discrete topology on any type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
The trivial topology on any type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any homeomorphisms induces an isomorphism in Top
.
Equations
- TopCat.isoOfHomeo f = { hom := ↑f, inv := ↑f.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Any isomorphism in Top
induces a homeomorphism.
Equations
- TopCat.homeoOfIso f = { toFun := ⇑f.hom, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Alias of TopCat.isOpenEmbedding_iff_comp_isIso
.
Alias of TopCat.isOpenEmbedding_iff_comp_isIso'
.
Alias of TopCat.isOpenEmbedding_iff_isIso_comp
.
Alias of TopCat.isOpenEmbedding_iff_isIso_comp'
.