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.

@[implicit_reducible]

instance Sequential.instInhabited : Inhabited Sequential

@[implicit_reducible]

instance Sequential.instCoeSortType : CoeSort Sequential (Type u_1)

@[implicit_reducible]

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

@[implicit_reducible]

instance Sequential.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory Sequential fun (x1 x2 : Sequential) => C(↑x1.toTop, ↑x2.toTop)

@[reducible, inline]

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

Constructor for objects of the category Sequential.

def Sequential.sequentialToTop : CategoryTheory.Functor Sequential TopCat

The fully faithful embedding of Sequential in TopCat.

@[simp]

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

@[simp]

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

def Sequential.fullyFaithfulSequentialToTop : sequentialToTop.FullyFaithful

The functor to TopCat is indeed fully faithful.

instance Sequential.instFullTopCatSequentialToTop : sequentialToTop.Full

instance Sequential.instFaithfulTopCatSequentialToTop : sequentialToTop.Faithful

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

Construct an isomorphism from a homeomorphism.

@[simp]

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

@[simp]

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

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

Construct a homeomorphism from an isomorphism.

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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