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.lean.

structure TopCat : Type (u + 1)

The category of topological spaces.

• of :: (
• carrier : Type u

  The underlying type.

• str : TopologicalSpace ↑self
• )

def TopCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents TopCat.of X being printed as { carrier := X, str := ... } by delabStructureInstance.

Equations

• TopCat.delabOf = Lean.PrettyPrinter.Delaborator.delabApp

@[implicit_reducible]

instance TopCat.instCoeSortType : CoeSort TopCat (Type u)

Equations

• TopCat.instCoeSortType = { coe := TopCat.carrier }

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

theorem TopCat.of_carrier (X : TopCat) : of ↑X = X

structure TopCat.Hom (X Y : TopCat) : Type u

The type of morphisms in TopCat.

• hom' : C(↑X, ↑Y)

  The underlying ContinuousMap.

theorem TopCat.Hom.ext {X Y : TopCat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

theorem TopCat.Hom.ext_iff {X Y : TopCat} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

instance TopCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} TopCat

Equations

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

@[implicit_reducible]

instance TopCat.instConcreteCategoryContinuousMapCarrier : CategoryTheory.ConcreteCategory TopCat fun (X Y : TopCat) => C(↑X, ↑Y)

Equations

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

@[reducible, inline]

abbrev TopCat.Hom.hom {X Y : TopCat} (f : X.Hom Y) : C(↑X, ↑Y)

Turn a morphism in TopCat back into a ContinuousMap.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev TopCat.ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : of X ⟶ of Y

Typecheck a ContinuousMap as a morphism in TopCat.

Equations

• TopCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def TopCat.Hom.Simps.hom (X Y : TopCat) (f : X.Hom Y) : C(↑X, ↑Y)

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• TopCat.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem TopCat.hom_id {X : TopCat} : Hom.hom (CategoryTheory.CategoryStruct.id X) = ContinuousMap.id ↑X

@[simp]

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

@[simp]

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

@[simp]

theorem TopCat.hom_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem TopCat.comp_app {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

@[simp]

theorem TopCat.coe_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem TopCat.hom_ext {X Y : TopCat} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem TopCat.hom_ext_iff {X Y : TopCat} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

theorem TopCat.ext {X Y : TopCat} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem TopCat.ext_iff {X Y : TopCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

@[simp]

theorem TopCat.hom_ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Hom.hom (ofHom f) = f

@[simp]

theorem TopCat.ofHom_hom {X Y : TopCat} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem TopCat.ofHom_id {X : Type u} [TopologicalSpace X] : ofHom (ContinuousMap.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem TopCat.ofHom_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem TopCat.ofHom_apply {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem TopCat.hom_inv_id_apply {X Y : TopCat} (f : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x

theorem TopCat.inv_hom_id_apply {X Y : TopCat} (f : X ≅ Y) (y : ↑Y) : (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) y) = y

def TopCat.Hom.equivContinuousMap (X Y : TopCat) : (X ⟶ Y) ≃ C(↑X, ↑Y)

Morphisms in TopCat are equivalent to continuous maps.

Equations

• TopCat.Hom.equivContinuousMap X Y = { toFun := fun (f : X ⟶ Y) => TopCat.Hom.hom f, invFun := fun (f : C(↑X, ↑Y)) => TopCat.ofHom f, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TopCat.Hom.equivContinuousMap_symm_apply (X Y : TopCat) (f : C(↑X, ↑Y)) : (equivContinuousMap X Y).symm f = ofHom f

@[simp]

theorem TopCat.Hom.equivContinuousMap_apply (X Y : TopCat) (f : X ⟶ Y) : (equivContinuousMap X Y) f = hom f

@[simp]

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

@[implicit_reducible]

instance TopCat.inhabited : Inhabited TopCat

Equations

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

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.instDiscreteTopologyCarrierObjDiscrete {X : Type u} : DiscreteTopology ↑(discrete.obj X)

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.

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

Any homeomorphisms induces an isomorphism in Top.

Equations

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

@[simp]

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

@[simp]

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

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

Any isomorphism in Top induces a homeomorphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem TopCat.isIso_of_bijective_of_isOpenMap {X Y : TopCat} (f : X ⟶ Y) (hfbij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfcl : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f

theorem TopCat.isIso_of_bijective_of_isClosedMap {X Y : TopCat} (f : X ⟶ Y) (hfbij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfcl : IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f

theorem TopCat.isIso_iff_isHomeomorph {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem TopCat.isOpenEmbedding_iff_comp_isIso {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem TopCat.isOpenEmbedding_iff_comp_isIso' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem TopCat.isOpenEmbedding_iff_isIso_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)

@[simp]

theorem TopCat.isOpenEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)