Documentation

Mathlib.Topology.Category.Sequential

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.

source
structure Sequential :
Type (u + 1)

The type sequential topological spaces.

Instances For
    source
    @[implicit_reducible]
    instance Sequential.instInhabited :
    Inhabited Sequential
    source
    @[implicit_reducible]
    instance Sequential.instCoeSortType :
    CoeSort Sequential (Type u_1)
    source
    @[implicit_reducible]
    instance Sequential.instCategory :
    CategoryTheory.Category.{u, u + 1} Sequential
    source
    @[implicit_reducible]
    instance Sequential.instConcreteCategoryContinuousMapCarrierToTop :
    CategoryTheory.ConcreteCategory Sequential fun (x1 x2 : Sequential) => C(↑x1.toTop, ↑x2.toTop)
    source
    @[reducible, inline]
    abbrev Sequential.of (X : Type u) [TopologicalSpace X] [SequentialSpace X] :
    Sequential

    Constructor for objects of the category Sequential.

    Instances For
      source
      def Sequential.sequentialToTop :
      CategoryTheory.Functor Sequential TopCat

      The fully faithful embedding of Sequential in TopCat.

      Instances For
        source
        @[simp]
        theorem Sequential.sequentialToTop_map {X✝ Y✝ : CategoryTheory.InducedCategory TopCat toTop} (f : X✝ ⟶ Y✝) :
        sequentialToTop.map f = f.hom
        source
        @[simp]
        theorem Sequential.sequentialToTop_obj (self : Sequential) :
        sequentialToTop.obj self = self.toTop
        source
        def Sequential.fullyFaithfulSequentialToTop :
        sequentialToTop.FullyFaithful

        The functor to TopCat is indeed fully faithful.

        Instances For
          source
          instance Sequential.instFullTopCatSequentialToTop :
          sequentialToTop.Full
          source
          instance Sequential.instFaithfulTopCatSequentialToTop :
          sequentialToTop.Faithful
          source
          def Sequential.isoOfHomeo {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) :
          X ≅ Y

          Construct an isomorphism from a homeomorphism.

          Instances For
            source
            @[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 := ⋯ })
            source
            @[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 := ⋯ })
            source
            def Sequential.homeoOfIso {X Y : Sequential} (f : X ≅ Y) :
            ↑X.toTop ≃ₜ ↑Y.toTop

            Construct a homeomorphism from an isomorphism.

            Instances For
              source
              @[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
              source
              @[simp]
              theorem Sequential.homeoOfIso_apply {X Y : Sequential} (f : X ≅ Y) (a : ↑X.toTop) :
              (homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
              source
              def Sequential.isoEquivHomeo {X Y : Sequential} :
              (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)

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

              Instances For
                source
                @[simp]
                theorem Sequential.isoEquivHomeo_apply {X Y : Sequential} (f : X ≅ Y) :
                isoEquivHomeo f = homeoOfIso f
                source
                @[simp]
                theorem Sequential.isoEquivHomeo_symm_apply {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop) :
                isoEquivHomeo.symm f = isoOfHomeo f