Documentation

Mathlib.CategoryTheory.Category.Pointed

The category of pointed types #

This defines Pointed, the category of pointed types.

TODO #

structure Pointed :
Type (u + 1)
  • X : Type u

    the underlying type

  • point : s.X

    the distinguished element

The category of pointed types.

Instances For
    def Pointed.of {X : Type u_3} (point : X) :

    Turns a point into a pointed type.

    Instances For
      @[simp]
      theorem Pointed.coe_of {X : Type u_3} (point : X) :
      (Pointed.of point).X = X
      def Prod.Pointed {X : Type u_3} (point : X) :

      Alias of Pointed.of.


      Turns a point into a pointed type.

      Instances For
        theorem Pointed.Hom.ext_iff {X : Pointed} {Y : Pointed} (x : Pointed.Hom X Y) (y : Pointed.Hom X Y) :
        x = y x.toFun = y.toFun
        theorem Pointed.Hom.ext {X : Pointed} {Y : Pointed} (x : Pointed.Hom X Y) (y : Pointed.Hom X Y) (toFun : x.toFun = y.toFun) :
        x = y
        structure Pointed.Hom (X : Pointed) (Y : Pointed) :
        • toFun : X.XY.X

          the underlying map

        • map_point : Pointed.Hom.toFun s X.point = Y.point

          compatibility with the distinguished points

        Morphisms in Pointed.

        Instances For
          @[simp]

          The identity morphism of X : Pointed.

          Instances For
            @[simp]
            theorem Pointed.Hom.comp_toFun {X : Pointed} {Y : Pointed} {Z : Pointed} (f : Pointed.Hom X Y) (g : Pointed.Hom Y Z) :
            ∀ (a : X.X), Pointed.Hom.toFun (Pointed.Hom.comp f g) a = (g.toFun f.toFun) a
            def Pointed.Hom.comp {X : Pointed} {Y : Pointed} {Z : Pointed} (f : Pointed.Hom X Y) (g : Pointed.Hom Y Z) :

            Composition of morphisms of Pointed.

            Instances For
              @[simp]
              theorem Pointed.Iso.mk_inv_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : β.X) :
              Pointed.Hom.toFun (Pointed.Iso.mk e he).inv a = e.symm a
              @[simp]
              theorem Pointed.Iso.mk_hom_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : α.X) :
              Pointed.Hom.toFun (Pointed.Iso.mk e he).hom a = e a
              def Pointed.Iso.mk {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) :
              α β

              Constructs an isomorphism between pointed types from an equivalence that preserves the point between them.

              Instances For
                @[simp]
                theorem typeToPointed_map_toFun :
                ∀ {X Y : Type u} (f : X Y) (a : Option X), Pointed.Hom.toFun (typeToPointed.map f) a = Option.map f a
                @[simp]
                theorem typeToPointed_obj_X (X : Type u) :
                (typeToPointed.obj X).X = Option X
                @[simp]
                theorem typeToPointed_obj_point (X : Type u) :
                (typeToPointed.obj X).point = none

                Option as a functor from types to pointed types. This is the free functor.

                Instances For