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.

def TopCat :
Type (u + 1)

The category of topological spaces and continuous maps.

Instances For
    theorem TopCat.id_app (X : TopCat) (x : X) :
    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)

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

    Instances For
      @[simp]
      theorem TopCat.coe_of (X : Type u) [TopologicalSpace X] :
      ↑(TopCat.of X) = X
      theorem TopCat.hom_apply {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :

      The discrete topology on any type.

      Instances For

        The trivial topology on any type.

        Instances For
          @[simp]
          def TopCat.isoOfHomeo {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
          X Y

          Any homeomorphisms induces an isomorphism in Top.

          Instances For
            @[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
            @[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
            def TopCat.homeoOfIso {X : TopCat} {Y : TopCat} (f : X Y) :
            X ≃ₜ Y

            Any isomorphism in Top induces a homeomorphism.

            Instances For
              @[simp]
              theorem TopCat.of_isoOfHomeo {X : TopCat} {Y : TopCat} (f : X ≃ₜ Y) :
              @[simp]