Documentation

Mathlib.CategoryTheory.Category.Pointed

The category of pointed types #

This defines Pointed, the category of pointed types.

TODO #

structure Pointed :
Type (u + 1)

The category of pointed types.

  • X : Type u

    the underlying type

  • point : self.X

    the distinguished element

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

    Turns a point into a pointed type.

    Equations
    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.

      Equations
      Instances For
        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
        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
        structure Pointed.Hom (X : Pointed) (Y : Pointed) :

        Morphisms in Pointed.

        • toFun : X.XY.X

          the underlying map

        • map_point : self.toFun X.point = Y.point

          compatibility with the distinguished points

        Instances For
          @[simp]
          theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) :
          (Pointed.Hom.id X).toFun a = id a

          The identity morphism of X : Pointed.

          Equations
          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.comp f g).toFun 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.

            Equations
            Instances For
              @[simp]
              theorem Pointed.Hom.comp_toFun' {X : Pointed} {Y : Pointed} {Z : Pointed} (f : X Y) (g : Y Z) :
              (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun f.toFun
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem Pointed.Iso.mk_inv_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : β.X) :
              (Pointed.Iso.mk e he).inv.toFun a = e.symm a
              @[simp]
              theorem Pointed.Iso.mk_hom_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : α.X) :
              (Pointed.Iso.mk e he).hom.toFun 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.

              Equations
              • Pointed.Iso.mk e he = { hom := { toFun := e, map_point := he }, inv := { toFun := e.symm, map_point := }, hom_inv_id := , inv_hom_id := }
              Instances For
                @[simp]
                theorem typeToPointed_map_toFun :
                ∀ {X Y : Type u} (f : X Y) (a : Option X), (typeToPointed.map f).toFun 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.

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

                  typeToPointed is the free functor.

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