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.

of :: (

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

)

Instances For

def TopCat.delabOf :

Lean.PrettyPrinter.Delaborator.Delab

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

Instances For

@[implicit_reducible]

instance TopCat.instCoeSortType :

CoeSort TopCat (Type u)

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

@[implicit_reducible]

instance TopCat.instCategory :

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

@[implicit_reducible]

instance TopCat.instConcreteCategoryContinuousMapCarrier :

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

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

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.

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.

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

def TopCat.Hom.equivContinuousMap (X Y : TopCat) :

(X ⟶ Y) ≃ C(↑X, ↑Y)

Morphisms in TopCat are equivalent to continuous maps.

Instances For

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

def TopCat.discrete :

CategoryTheory.Functor (Type u) TopCat

The discrete topology on any type.

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.

Instances For

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

X ≅ Y

Any homeomorphisms induces an isomorphism in Top.

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.

Instances For

@[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.homeoOfIso_apply {X Y : TopCat} (f : X ≅ Y) (a : ↑X) :

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

def TopCat.const {X Y : TopCat} (y : ↑Y) :

X ⟶ Y

The constant morphism X ⟶ Y in TopCat given by y : Y.

Instances For

@[simp]

theorem TopCat.const_apply {X Y : TopCat} (y : ↑Y) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom (const y)) x = y