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.

instance Sequential.instInhabited : Inhabited Sequential

Equations

• Sequential.instInhabited = { default := Sequential.mk { α := ULift.{?u.3, 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)

def Sequential.sequentialToTop : CategoryTheory.Functor Sequential TopCat

The fully faithful embedding of Sequential in TopCat.

Equations

• Sequential.sequentialToTop = CategoryTheory.inducedFunctor Sequential.toTop

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

instance Sequential.instFaithfulTopCatSequentialToTop : Sequential.sequentialToTop.Faithful

def Sequential.isoOfHomeo {X 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.isoOfHomeo_hom {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (Sequential.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }

@[simp]

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

def Sequential.homeoOfIso {X 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.homeoOfIso_symm_apply {X 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 Y : Sequential} (f : X ≅ Y) (a : (CategoryTheory.forget Sequential).obj X) : (Sequential.homeoOfIso f) a = f.hom a

def Sequential.isoEquivHomeo {X 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 := ⋯ }

@[simp]

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

@[simp]

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