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.

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

    Turns a bipointing into a bipointed type.

    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.

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

        Morphisms in Bipointed.

        Instances For

          The identity morphism of X : Bipointed.

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

            Composition of morphisms of Bipointed.

            Instances For
              @[simp]
              theorem Bipointed.swap_map_toFun :
              ∀ {X Y : Bipointed} (f : X Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swap.map f) a = Bipointed.Hom.toFun f 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 = Prod.swap X.toProd

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

              Instances For
                @[simp]
                theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.functor.obj X).toProd = Prod.swap X.toProd
                @[simp]
                theorem Bipointed.swapEquiv_unitIso_inv_app_toFun (X : Bipointed) :
                ∀ (a : ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).X), Bipointed.Hom.toFun (Bipointed.swapEquiv.unitIso.inv.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.fst = id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.snd = id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.snd) })) (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj (Bipointed.swap.obj X)).toProd.fst = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj (Bipointed.swap.obj X)).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj (Bipointed.swap.obj X)).toProd.snd = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj (Bipointed.swap.obj X)).toProd.snd) }) { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.fst = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.snd = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.snd) })) (Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))) a)
                @[simp]
                @[simp]
                theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.inverse.obj X).toProd = Prod.swap X.toProd
                @[simp]
                @[simp]
                theorem Bipointed.swapEquiv_unitIso_hom_app_toFun (X : Bipointed) :
                ∀ (a : ((CategoryTheory.Functor.id Bipointed).obj X).X), Bipointed.Hom.toFun (Bipointed.swapEquiv.unitIso.hom.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))) (Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.fst = id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.snd = id ((CategoryTheory.Functor.id Bipointed).obj X).toProd.snd) } (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.id Bipointed).obj (Bipointed.swap.obj X)).toProd.fst = id ((CategoryTheory.Functor.id Bipointed).obj (Bipointed.swap.obj X)).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.id Bipointed).obj (Bipointed.swap.obj X)).toProd.snd = id ((CategoryTheory.Functor.id Bipointed).obj (Bipointed.swap.obj X)).toProd.snd) }) (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.fst = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.fst), map_snd := (_ : id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.snd = id ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).toProd.snd) })))) a)
                @[simp]
                @[simp]

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

                Instances For

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

                  Instances For

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

                    Instances For

                      The functor from Pointed to Bipointed which bipoints the point.

                      Instances For

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

                        Instances For

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

                          Instances For

                            The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

                            Instances For

                              The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

                              Instances For