Documentation

Mathlib.Topology.Category.TopCat.Basic

Category instance for topological spaces #

We introduce the bundled category TopCat of topological spaces together with the functors discrete and trivial from the category of types to TopCat which equip a type with the corresponding discrete, resp. trivial, topology. For a proof that these functors are left, resp. right adjoint to the forgetful functor, see topology.category.TopCat.adjunctions.

source
def TopCat :
Type (u + 1)

The category of topological spaces and continuous maps.

Instances For
    source
    instance TopCat.bundledHom :
    CategoryTheory.BundledHom ContinuousMap
    source
    instance TopCat.concreteCategory :
    CategoryTheory.ConcreteCategory TopCat
    source
    instance TopCat.instCoeSortTopCatType :
    CoeSort TopCat (Type u_1)
    source
    instance TopCat.topologicalSpaceUnbundled (x : TopCat) :
    TopologicalSpace ↑x
    source
    instance TopCat.instCoeFunHomTopCatToQuiverToCategoryStructInstTopCatLargeCategoryForAllαTopologicalSpace (X : TopCat) (Y : TopCat) :
    CoeFun (X ⟶ Y) fun x => ↑X → ↑Y
    source
    theorem TopCat.id_app (X : TopCat) (x : ↑X) :
    ↑(CategoryTheory.CategoryStruct.id X) x = x
    source
    theorem TopCat.comp_app {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :
    ↑(CategoryTheory.CategoryStruct.comp f g) x = ↑g (↑f x)
    source
    def TopCat.of (X : Type u) [TopologicalSpace X] :
    TopCat

    Construct a bundled Top from the underlying type and the typeclass.

    Instances For
      source
      instance TopCat.topologicalSpace_coe (X : TopCat) :
      TopologicalSpace ↑X
      source
      @[reducible]
      instance TopCat.topologicalSpace_forget (X : TopCat) :
      TopologicalSpace ((CategoryTheory.forget TopCat).obj X)
      source
      @[simp]
      theorem TopCat.coe_of (X : Type u) [TopologicalSpace X] :
      ↑(TopCat.of X) = X
      source
      instance TopCat.inhabited :
      Inhabited TopCat
      source
      theorem TopCat.hom_apply {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) :
      ↑f x = ContinuousMap.toFun f x
      source
      def TopCat.discrete :
      CategoryTheory.Functor (Type u) TopCat

      The discrete topology on any type.

      Instances For
        source
        instance TopCat.instDiscreteTopologyαTopologicalSpaceObjTypeToQuiverToCategoryStructTypesTopCatInstTopCatLargeCategoryToPrefunctorDiscreteTopologicalSpace_coe {X : Type u} :
        DiscreteTopology ↑(TopCat.discrete.obj X)
        source
        def TopCat.trivial :
        CategoryTheory.Functor (Type u) TopCat

        The trivial topology on any type.

        Instances For
          source
          @[simp]
          theorem TopCat.isoOfHomeo_hom {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) :
          (TopCat.isoOfHomeo f).hom = Homeomorph.toContinuousMap f
          source
          @[simp]
          theorem TopCat.isoOfHomeo_inv {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) :
          (TopCat.isoOfHomeo f).inv = Homeomorph.toContinuousMap (Homeomorph.symm f)
          source
          def TopCat.isoOfHomeo {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) :
          X ≅ Y

          Any homeomorphisms induces an isomorphism in Top.

          Instances For
            source
            @[simp]
            theorem TopCat.homeoOfIso_apply {X : TopCat} {Y : TopCat} (f : X ≅ Y) (a : (CategoryTheory.forget TopCat).obj X) :
            ↑(TopCat.homeoOfIso f) a = ↑f.hom a
            source
            @[simp]
            theorem TopCat.homeoOfIso_symm_apply {X : TopCat} {Y : TopCat} (f : X ≅ Y) (a : (CategoryTheory.forget TopCat).obj Y) :
            ↑(Homeomorph.symm (TopCat.homeoOfIso f)) a = ↑f.inv a
            source
            def TopCat.homeoOfIso {X : TopCat} {Y : TopCat} (f : X ≅ Y) :
            ↑X ≃ₜ ↑Y

            Any isomorphism in Top induces a homeomorphism.

            Instances For
              source
              @[simp]
              theorem TopCat.of_isoOfHomeo {X : TopCat} {Y : TopCat} (f : ↑X ≃ₜ ↑Y) :
              TopCat.homeoOfIso (TopCat.isoOfHomeo f) = f
              source
              @[simp]
              theorem TopCat.of_homeoOfIso {X : TopCat} {Y : TopCat} (f : X ≅ Y) :
              TopCat.isoOfHomeo (TopCat.homeoOfIso f) = f
              source
              theorem TopCat.openEmbedding_iff_comp_isIso {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] :
              OpenEmbedding ↑(CategoryTheory.CategoryStruct.comp f g) ↔ OpenEmbedding ↑f
              source
              @[simp]
              theorem TopCat.openEmbedding_iff_comp_isIso' {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] :
              OpenEmbedding (CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget TopCat).map f) ((CategoryTheory.forget TopCat).map g)) ↔ OpenEmbedding ↑f
              source
              theorem TopCat.openEmbedding_iff_isIso_comp {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :
              OpenEmbedding ↑(CategoryTheory.CategoryStruct.comp f g) ↔ OpenEmbedding ↑g
              source
              @[simp]
              theorem TopCat.openEmbedding_iff_isIso_comp' {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] :
              OpenEmbedding (CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget TopCat).map f) ((CategoryTheory.forget TopCat).map g)) ↔ OpenEmbedding ↑g