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 := { toTop := TopCat.of (ULift.{?u.2, 0} (Fin 37)), is_sequential := Sequential.instInhabited._proof_1 } }

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.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory Sequential fun (x1 x2 : Sequential) => C(↑x1.toTop, ↑x2.toTop)

Equations

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

@[reducible, inline]

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

Constructor for objects of the category Sequential.

Equations

• Sequential.of X = { toTop := TopCat.of X, is_sequential := inst✝ }

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_map {X✝ Y✝ : CategoryTheory.InducedCategory TopCat toTop} (f : X✝ ⟶ Y✝) : sequentialToTop.map f = f

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

Equations

• Sequential.fullyFaithfulSequentialToTop = CategoryTheory.fullyFaithfulInducedFunctor Sequential.toTop

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.

Equations

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

@[simp]

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

@[simp]

theorem Sequential.isoOfHomeo_inv {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (isoOfHomeo f).inv = TopCat.ofHom { 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

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

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

@[simp]

theorem Sequential.homeoOfIso_apply {X Y : Sequential} (f : X ≅ Y) (a : ↑X.toTop) : (homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom 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) : isoEquivHomeo f = homeoOfIso f

@[simp]

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