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

• TopCat = CategoryTheory.Bundled TopologicalSpace

instance TopCat.bundledHom : CategoryTheory.BundledHom ContinuousMap

Equations

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

instance TopCat.concreteCategory : CategoryTheory.ConcreteCategory TopCat

Equations

• TopCat.concreteCategory = inferInstanceAs (CategoryTheory.ConcreteCategory (CategoryTheory.Bundled TopologicalSpace))

instance TopCat.instCoeSortType : CoeSort TopCat (Type u_1)

Equations

• TopCat.instCoeSortType = { coe := fun (X : TopCat) => ↑X }

instance TopCat.topologicalSpaceUnbundled (X : TopCat) : TopologicalSpace ↑X

Equations

• X.topologicalSpaceUnbundled = X.str

instance TopCat.instFunLike (X : TopCat) (Y : TopCat) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

• X.instFunLike Y = inferInstanceAs (FunLike C(↑X, ↑Y) ↑X ↑Y)

instance TopCat.instMonoidHomClass (X : TopCat) (Y : TopCat) : ContinuousMapClass (X ⟶ Y) ↑X ↑Y

Equations

• ⋯ = ⋯

theorem TopCat.id_app (X : TopCat) (x : ↑X) : (CategoryTheory.CategoryStruct.id X) x = x

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)

@[simp]

theorem TopCat.coe_id (X : TopCat) : ⇑(CategoryTheory.CategoryStruct.id X) = id

@[simp]

theorem TopCat.coe_comp {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑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) [TopologicalSpace X] : TopCat

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

Equations

• TopCat.of X = { α := X, str := inferInstance }

instance TopCat.topologicalSpace_coe (X : TopCat) : TopologicalSpace ↑X

Equations

• X.topologicalSpace_coe = X.str

@[reducible, inline]

instance TopCat.topologicalSpace_forget (X : TopCat) : TopologicalSpace ((CategoryTheory.forget TopCat).obj X)

Equations

• X.topologicalSpace_forget = X.str

@[simp]

theorem TopCat.coe_of (X : Type u) [TopologicalSpace X] : ↑(TopCat.of X) = X

@[simp]

theorem TopCat.coe_of_of {X : Type u} {Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {x : (CategoryTheory.forget TopCat).obj (TopCat.of X)} : 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 : Inhabited TopCat

Equations

• TopCat.inhabited = { default := TopCat.of Empty }

theorem TopCat.hom_apply {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) : f x = f.toFun x

def TopCat.discrete : CategoryTheory.Functor (Type u) TopCat

The discrete topology on any type.

Equations

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

instance TopCat.instDiscreteTopologyαTopologicalSpaceObjDiscrete {X : Type u} : DiscreteTopology ↑(TopCat.discrete.obj X)

Equations

• ⋯ = ⋯

def TopCat.trivial : CategoryTheory.Functor (Type u) TopCat

The trivial topology on any type.

Equations

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

@[simp]

theorem TopCat.isoOfHomeo_hom {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) : (TopCat.isoOfHomeo f).hom = f.toContinuousMap

@[simp]

theorem TopCat.isoOfHomeo_inv {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) : (TopCat.isoOfHomeo f).inv = f.symm.toContinuousMap

def TopCat.isoOfHomeo {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) : X ≅ Y

Any homeomorphisms induces an isomorphism in Top.

Equations

• TopCat.isoOfHomeo f = { hom := f.toContinuousMap, inv := f.symm.toContinuousMap, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TopCat.homeoOfIso_symm_apply {X : TopCat} {Y : TopCat} (f : X ≅ Y) (a : ↑Y) : (TopCat.homeoOfIso f).symm a = f.inv a

@[simp]

theorem TopCat.homeoOfIso_apply {X : TopCat} {Y : TopCat} (f : X ≅ Y) (a : ↑X) : (TopCat.homeoOfIso f) a = f.hom a

def TopCat.homeoOfIso {X : TopCat} {Y : TopCat} (f : X ≅ Y) : ↑X ≃ₜ ↑Y

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 := ⋯ }

@[simp]

theorem TopCat.of_isoOfHomeo {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) : TopCat.homeoOfIso (TopCat.isoOfHomeo f) = f

@[simp]

theorem TopCat.of_homeoOfIso {X : TopCat} {Y : TopCat} (f : X ≅ Y) : TopCat.isoOfHomeo (TopCat.homeoOfIso f) = f

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 f g) ↔ OpenEmbedding ⇑f

@[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] : OpenEmbedding ⇑(CategoryTheory.CategoryStruct.comp f g) ↔ OpenEmbedding ⇑g

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