Documentation

Mathlib.Topology.Category.TopCat.Basic

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.

carrier : Type u
The underlying type.
str : TopologicalSpace ↑self

Instances For

instance TopCat.instCoeSortType :

CoeSort TopCat (Type u)

Equations

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

@[reducible, inline]

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

The object in TopCat associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of TopCat.

Equations

TopCat.of X = { carrier := X, str := inst✝ }

Instances For

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) :

The type of morphisms in TopCat.

hom' : C(↑X, ↑Y)
The underlying ContinuousMap.

Instances For

theorem TopCat.Hom.ext_iff {X Y : TopCat} {x y : X.Hom Y} :

x = y ↔ x.hom' = y.hom'

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

x = y

instance TopCat.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} TopCat

Equations

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

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

Instances For

@[reducible, inline]

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

Typecheck a ContinuousMap as a morphism in TopCat.

Equations

TopCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

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

Instances For

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

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

instance TopCat.inhabited :

Inhabited TopCat

Equations

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

@[deprecated "Simply remove this from the `simp`/`rw` set: the LHS and RHS are now identical." (since := "2025-01-30")]

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

(CategoryTheory.ConcreteCategory.hom f) x = (Hom.hom 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.

Instances For

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.

Instances For

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

Instances For

@[simp]

theorem TopCat.isoOfHomeo_hom {X Y : TopCat} (f : ↑X ≃ₜ ↑Y) :

(isoOfHomeo f).hom = ofHom ↑f

@[simp]

theorem TopCat.isoOfHomeo_inv {X Y : TopCat} (f : ↑X ≃ₜ ↑Y) :

(isoOfHomeo f).inv = ofHom ↑f.symm

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.

Instances For

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