Documentation

Mathlib.CategoryTheory.Category.Bipointed

The category of bipointed types #

This defines Bipointed, the category of bipointed types.

TODO #

Monoidal structure

structure Bipointed :
Type (u + 1)

The category of bipointed types.

  • X : Type u

    The underlying type of a bipointed type.

  • toProd : self.X × self.X

    The two points of a bipointed type, bundled together as a pair.

Instances For
    def Bipointed.of {X : Type u_3} (to_prod : X × X) :

    Turns a bipointing into a bipointed type.

    Equations
    Instances For
      @[simp]
      theorem Bipointed.coe_of {X : Type u_3} (to_prod : X × X) :
      (Bipointed.of to_prod).X = X
      def Prod.Bipointed {X : Type u_3} (to_prod : X × X) :

      Alias of Bipointed.of.


      Turns a bipointing into a bipointed type.

      Equations
      Instances For
        theorem Bipointed.Hom.ext_iff {X : Bipointed} {Y : Bipointed} (x : X.Hom Y) (y : X.Hom Y) :
        x = y x.toFun = y.toFun
        theorem Bipointed.Hom.ext {X : Bipointed} {Y : Bipointed} (x : X.Hom Y) (y : X.Hom Y) (toFun : x.toFun = y.toFun) :
        x = y
        structure Bipointed.Hom (X : Bipointed) (Y : Bipointed) :

        Morphisms in Bipointed.

        • toFun : X.XY.X

          The underlying function of a morphism of bipointed types.

        • map_fst : self.toFun X.toProd.1 = Y.toProd.1
        • map_snd : self.toFun X.toProd.2 = Y.toProd.2
        Instances For
          theorem Bipointed.Hom.map_fst {X : Bipointed} {Y : Bipointed} (self : X.Hom Y) :
          self.toFun X.toProd.1 = Y.toProd.1
          theorem Bipointed.Hom.map_snd {X : Bipointed} {Y : Bipointed} (self : X.Hom Y) :
          self.toFun X.toProd.2 = Y.toProd.2
          @[simp]
          theorem Bipointed.Hom.id_toFun (X : Bipointed) (a : X.X) :
          (Bipointed.Hom.id X).toFun a = id a
          def Bipointed.Hom.id (X : Bipointed) :
          X.Hom X

          The identity morphism of X : Bipointed.

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

            Composition of morphisms of Bipointed.

            Equations
            • f.comp g = { toFun := g.toFun f.toFun, map_fst := , map_snd := }
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem Bipointed.swap_map_toFun :
              ∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swap.map f).toFun a = f.toFun a
              @[simp]
              theorem Bipointed.swap_obj_X (X : Bipointed) :
              (Bipointed.swap.obj X).X = X.X
              @[simp]
              theorem Bipointed.swap_obj_toProd (X : Bipointed) :
              (Bipointed.swap.obj X).toProd = X.toProd.swap

              Swaps the pointed elements of a bipointed type. Prod.swap as a functor.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                @[simp]
                theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.functor.obj X).toProd = X.toProd.swap
                @[simp]
                theorem Bipointed.swapEquiv_inverse_map_toFun :
                ∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swapEquiv.inverse.map f).toFun a = f.toFun a
                @[simp]
                theorem Bipointed.swapEquiv_functor_map_toFun :
                ∀ {X Y : Bipointed} (f : X Y) (a : X.X), (Bipointed.swapEquiv.functor.map f).toFun a = f.toFun a
                @[simp]
                theorem Bipointed.swapEquiv_unitIso_hom_app_toFun (X : Bipointed) :
                ∀ (a : ((CategoryTheory.Functor.id Bipointed).obj X).X), (Bipointed.swapEquiv.unitIso.hom.app X).toFun a = (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun ((CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := , map_snd := } (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := , map_snd := }) (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := , map_snd := })))).toFun a)
                @[simp]
                theorem Bipointed.swapEquiv_counitIso_hom_app_toFun (X : Bipointed) (a : ((Bipointed.swap.comp Bipointed.swap).obj X).X) :
                (Bipointed.swapEquiv.counitIso.hom.app X).toFun a = a
                @[simp]
                @[simp]
                theorem Bipointed.swapEquiv_unitIso_inv_app_toFun (X : Bipointed) :
                ∀ (a : ((Bipointed.swap.comp Bipointed.swap).obj X).X), (Bipointed.swapEquiv.unitIso.inv.app X).toFun a = (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := , map_snd := })) (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := , map_snd := }) { toFun := id, map_fst := , map_snd := })).toFun ((CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun a)
                @[simp]
                @[simp]
                theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.inverse.obj X).toProd = X.toProd.swap

                The equivalence between Bipointed and itself induced by Prod.swap both ways.

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

                  The forgetful functor from Bipointed to Pointed which forgets about the second point.

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

                    The forgetful functor from Bipointed to Pointed which forgets about the first point.

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

                      The functor from Pointed to Bipointed which bipoints the point.

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

                        The functor from Pointed to Bipointed which adds a second point.

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

                          The functor from Pointed to Bipointed which adds a first point.

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

                            BipointedToPointed_fst is inverse to PointedToBipointed.

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

                              BipointedToPointed_snd is inverse to PointedToBipointed.

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

                                The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

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

                                  The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

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