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

• TopCat.bundledHom = CategoryTheory.BundledHom.mk (@ContinuousMap.toFun) ContinuousMap.id @ContinuousMap.comp

instance TopCat.concreteCategory : CategoryTheory.ConcreteCategory TopCat

Equations

• TopCat.concreteCategory = id inferInstance

instance TopCat.instCoeSortTopCatType : CoeSort TopCat (Type u_1)

Equations

• TopCat.instCoeSortTopCatType = CategoryTheory.Bundled.coeSort

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

Equations

• TopCat.topologicalSpaceUnbundled x = x.str

instance TopCat.instCoeFunHomTopCatToQuiverToCategoryStructInstTopCatLargeCategoryForAllαTopologicalSpace (X : TopCat) (Y : TopCat) : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y

Equations

• TopCat.instCoeFunHomTopCatToQuiverToCategoryStructInstTopCatLargeCategoryForAllαTopologicalSpace X Y = { coe := fun (f : X ⟶ Y) => ⇑f }

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)

def TopCat.of (X : Type u) [TopologicalSpace X] : TopCat

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

Equations

• TopCat.of X = CategoryTheory.Bundled.mk X

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

Equations

• TopCat.topologicalSpace_coe X = X.str

@[reducible]

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

Equations

• TopCat.topologicalSpace_forget X = X.str

@[simp]

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

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

• TopCat.discrete = CategoryTheory.Functor.mk { obj := fun (X : Type u) => CategoryTheory.Bundled.mk X, map := fun {X Y : Type u} (f : X ⟶ Y) => ContinuousMap.mk f }

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

Equations

• (_ : DiscreteTopology ↑(TopCat.discrete.toPrefunctor.obj X)) = (_ : DiscreteTopology ↑(TopCat.discrete.toPrefunctor.obj X))

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

The trivial topology on any type.

Equations

• TopCat.trivial = CategoryTheory.Functor.mk { obj := fun (X : Type u) => CategoryTheory.Bundled.mk X, map := fun {X Y : Type u} (f : X ⟶ Y) => ContinuousMap.mk f }

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

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

Any homeomorphisms induces an isomorphism in Top.

Equations

• TopCat.isoOfHomeo f = CategoryTheory.Iso.mk (Homeomorph.toContinuousMap f) (Homeomorph.toContinuousMap (Homeomorph.symm f))

@[simp]

theorem TopCat.homeoOfIso_apply {X : TopCat} {Y : TopCat} (f : X ≅ Y) (a : (CategoryTheory.forget TopCat).toPrefunctor.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).toPrefunctor.obj Y) : (Homeomorph.symm (TopCat.homeoOfIso f)) a = f.inv a

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

Any isomorphism in Top induces a homeomorphism.

Equations

• TopCat.homeoOfIso f = Homeomorph.mk { toFun := ⇑f.hom, invFun := ⇑f.inv, left_inv := (_ : ∀ (x : ↑X), f.2 (f.1 x) = x), right_inv := (_ : ∀ (x : ↑Y), f.1 (f.2 x) = x) }

@[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).toPrefunctor.map f) ((CategoryTheory.forget TopCat).toPrefunctor.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).toPrefunctor.map f) ((CategoryTheory.forget TopCat).toPrefunctor.map g)) ↔ OpenEmbedding ⇑g