Documentation

Mathlib.CategoryTheory.Category.Pointed

The category of pointed types #

This defines Pointed, the category of pointed types.

TODO #

source
structure Pointed :
Type (u + 1)

The category of pointed types.

  • X : Type u

    the underlying type

  • point : self.X

    the distinguished element

Instances For
    source
    @[implicit_reducible]
    instance Pointed.instCoeSortType :
    CoeSort Pointed (Type u_1)
    source
    @[reducible, inline]
    abbrev Pointed.of {X : Type u_1} (point : X) :
    Pointed

    Turns a point into a pointed type.

    Instances For
      source
      theorem Pointed.coe_of {X : Type u_1} (point : X) :
      (of point).X = X
      source
      def Prod.Pointed {X : Type u_1} (point : X) :
      _root_.Pointed

      Alias of Pointed.of.

      Turns a point into a pointed type.

      Instances For
        source
        @[implicit_reducible]
        instance Pointed.instInhabited :
        Inhabited Pointed
        source
        structure Pointed.Hom (X Y : Pointed) :
        Type u

        Morphisms in Pointed.

        • toFun : X.X → Y.X

          the underlying map

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

          compatibility with the distinguished points

        Instances For
          source
          theorem Pointed.Hom.ext {X Y : Pointed} {x y : X.Hom Y} (toFun : x.toFun = y.toFun) :
          x = y
          source
          theorem Pointed.Hom.ext_iff {X Y : Pointed} {x y : X.Hom Y} :
          x = y ↔ x.toFun = y.toFun
          source
          def Pointed.Hom.id (X : Pointed) :
          X.Hom X

          The identity morphism of X : Pointed.

          Instances For
            source
            @[simp]
            theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) :
            (id X).toFun a = _root_.id a
            source
            @[implicit_reducible]
            instance Pointed.Hom.instInhabited (X : Pointed) :
            Inhabited (X.Hom X)
            source
            def Pointed.Hom.comp {X Y Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) :
            X.Hom Z

            Composition of morphisms of Pointed.

            Instances For
              source
              @[simp]
              theorem Pointed.Hom.comp_toFun {X Y Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) (a✝ : X.X) :
              (f.comp g).toFun a✝ = (g.toFun ∘ f.toFun) a✝
              source
              @[implicit_reducible]
              instance Pointed.largeCategory :
              CategoryTheory.LargeCategory Pointed
              source
              @[simp]
              theorem Pointed.Hom.id_toFun' (X : Pointed) :
              (CategoryTheory.CategoryStruct.id X).toFun = _root_.id
              source
              @[simp]
              theorem Pointed.Hom.comp_toFun' {X Y Z : Pointed} (f : X ⟶ Y) (g : Y ⟶ Z) :
              (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun ∘ f.toFun
              source
              @[implicit_reducible]
              instance Pointed.instFunLikeSubtypeForallXEqPoint (X : Pointed) (Y : Pointed) :
              FunLike { f : X.X → Y.X // f X.point = Y.point } X.X Y.X
              source
              @[implicit_reducible]
              instance Pointed.hasForget :
              CategoryTheory.ConcreteCategory Pointed fun (X Y : Pointed) => { f : X.X → Y.X // f X.point = Y.point }
              source
              def Pointed.Iso.mk {α β : 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
                source
                @[simp]
                theorem Pointed.Iso.mk_hom_toFun {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : α.X) :
                (mk e he).hom.toFun a = e a
                source
                @[simp]
                theorem Pointed.Iso.mk_inv_toFun {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : β.X) :
                (mk e he).inv.toFun a = e.symm a
                source
                def typeToPointed :
                CategoryTheory.Functor (Type u) Pointed

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

                Instances For
                  source
                  @[simp]
                  theorem typeToPointed_obj_point (X : Type u) :
                  (typeToPointed.obj X).point = none
                  source
                  @[simp]
                  theorem typeToPointed_obj_X (X : Type u) :
                  (typeToPointed.obj X).X = Option X
                  source
                  @[simp]
                  theorem typeToPointed_map_toFun {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) (a✝ : Option X✝) :
                  (typeToPointed.map f).toFun a✝ = Option.map f a✝
                  source
                  def typeToPointedForgetAdjunction :
                  typeToPointed ⊣ CategoryTheory.forget Pointed

                  typeToPointed is the free functor.

                  Instances For