The category of sequential topological spaces

We define the category Sequential of sequential topological spaces. We follow the usual template for defining categories of topological spaces, by giving it the induced category structure from TopCat.

structure Sequential : Type (u + 1)

The type sequential topological spaces.

• toTop : TopCat

  The underlying topological space of an object of Sequential.

• is_sequential : SequentialSpace ↑self.toTop

  The underlying topological space is sequential.

theorem Sequential.is_sequential (self : Sequential) : SequentialSpace ↑self.toTop

The underlying topological space is sequential.

instance Sequential.instInhabited : Inhabited Sequential

Equations

• Sequential.instInhabited = { default := Sequential.mk { α := ULift.{u, 0} (Fin 37), str := inferInstance } }

instance Sequential.instCoeSortType : CoeSort Sequential (Type u_1)

Equations

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

instance Sequential.instCategory : CategoryTheory.Category.{u, u + 1} Sequential

Equations

• Sequential.instCategory = CategoryTheory.InducedCategory.category Sequential.toTop

instance Sequential.instConcreteCategory : CategoryTheory.ConcreteCategory Sequential

Equations

• Sequential.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory Sequential.toTop

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

Constructor for objects of the category Sequential.

Equations

• Sequential.of X = Sequential.mk (TopCat.of X)

@[simp]

theorem Sequential.sequentialToTop_obj (self : Sequential) : Sequential.sequentialToTop.obj self = self.toTop

@[simp]

theorem Sequential.sequentialToTop_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat Sequential.toTop} (f : X ⟶ Y), Sequential.sequentialToTop.map f = f

def Sequential.sequentialToTop : CategoryTheory.Functor Sequential TopCat

The fully faithful embedding of Sequential in TopCat.

Equations

• Sequential.sequentialToTop = CategoryTheory.inducedFunctor Sequential.toTop

def Sequential.fullyFaithfulSequentialToTop : Sequential.sequentialToTop.FullyFaithful

The functor to TopCat is indeed fully faithful.

Equations

• Sequential.fullyFaithfulSequentialToTop = CategoryTheory.fullyFaithfulInducedFunctor Sequential.toTop

instance Sequential.instFullTopCatSequentialToTop : Sequential.sequentialToTop.Full

Equations

• Sequential.instFullTopCatSequentialToTop = ⋯

instance Sequential.instFaithfulTopCatSequentialToTop : Sequential.sequentialToTop.Faithful

Equations

• Sequential.instFaithfulTopCatSequentialToTop = ⋯

@[simp]

theorem Sequential.isoOfHomeo_inv {X : Sequential} {Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (Sequential.isoOfHomeo f).inv = { toFun := ⇑f.symm, continuous_toFun := ⋯ }

@[simp]

theorem Sequential.isoOfHomeo_hom {X : Sequential} {Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (Sequential.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }

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

Construct an isomorphism from a homeomorphism.

Equations

• Sequential.isoOfHomeo f = { hom := { toFun := ⇑f, continuous_toFun := ⋯ }, inv := { toFun := ⇑f.symm, continuous_toFun := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Sequential.homeoOfIso_symm_apply {X : Sequential} {Y : Sequential} (f : X ≅ Y) (a : (CategoryTheory.forget Sequential).obj Y) : (Sequential.homeoOfIso f).symm a = f.inv a

@[simp]

theorem Sequential.homeoOfIso_apply {X : Sequential} {Y : Sequential} (f : X ≅ Y) (a : (CategoryTheory.forget Sequential).obj X) : (Sequential.homeoOfIso f) a = f.hom a

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

Construct a homeomorphism from an isomorphism.

Equations

• Sequential.homeoOfIso f = { toFun := ⇑f.hom, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Sequential.isoEquivHomeo_symm_apply {X : Sequential} {Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : Sequential.isoEquivHomeo.symm f = Sequential.isoOfHomeo f

@[simp]

theorem Sequential.isoEquivHomeo_apply {X : Sequential} {Y : Sequential} (f : X ≅ Y) : Sequential.isoEquivHomeo f = Sequential.homeoOfIso f

def Sequential.isoEquivHomeo {X : Sequential} {Y : Sequential} : (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)

The equivalence between isomorphisms in Sequential and homeomorphisms of topological spaces.

Equations

• Sequential.isoEquivHomeo = { toFun := Sequential.homeoOfIso, invFun := Sequential.isoOfHomeo, left_inv := ⋯, right_inv := ⋯ }