Documentation

Mathlib.CategoryTheory.Category.Bipointed

The category of bipointed types #

This defines Bipointed, the category of bipointed types.

TODO #

Monoidal structure

source
structure Bipointed :
Type (u + 1)

The category of bipointed types.

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

    Turns a bipointing into a bipointed type.

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

      Alias of Bipointed.of.

      Turns a bipointing into a bipointed type.

      Instances For
        source
        instance Bipointed.instInhabitedBipointed :
        Inhabited Bipointed
        source
        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
        source
        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
        source
        structure Bipointed.Hom (X : Bipointed) (Y : Bipointed) :
        Type u

        Morphisms in Bipointed.

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

          The identity morphism of X : Bipointed.

          Instances For
            source
            instance Bipointed.Hom.instInhabitedHom (X : Bipointed) :
            Inhabited (Bipointed.Hom X X)
            source
            @[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
            source
            def Bipointed.Hom.comp {X : Bipointed} {Y : Bipointed} {Z : Bipointed} (f : Bipointed.Hom X Y) (g : Bipointed.Hom Y Z) :
            Bipointed.Hom X Z

            Composition of morphisms of Bipointed.

            Instances For
              source
              instance Bipointed.largeCategory :
              CategoryTheory.LargeCategory Bipointed
              source
              instance Bipointed.concreteCategory :
              CategoryTheory.ConcreteCategory Bipointed
              source
              @[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
              source
              @[simp]
              theorem Bipointed.swap_obj_X (X : Bipointed) :
              (Bipointed.swap.obj X).X = X.X
              source
              @[simp]
              theorem Bipointed.swap_obj_toProd (X : Bipointed) :
              (Bipointed.swap.obj X).toProd = Prod.swap X.toProd
              source
              def Bipointed.swap :
              CategoryTheory.Functor Bipointed Bipointed

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

              Instances For
                source
                @[simp]
                theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.functor.obj X).toProd = Prod.swap X.toProd
                source
                @[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)
                source
                @[simp]
                theorem Bipointed.swapEquiv_functor_map_toFun :
                ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swapEquiv.functor.map f) a = Bipointed.Hom.toFun f a
                source
                @[simp]
                theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :
                (Bipointed.swapEquiv.inverse.obj X).toProd = Prod.swap X.toProd
                source
                @[simp]
                theorem Bipointed.swapEquiv_functor_obj_X (X : Bipointed) :
                (Bipointed.swapEquiv.functor.obj X).X = X.X
                source
                @[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)
                source
                @[simp]
                theorem Bipointed.swapEquiv_counitIso_inv_app_toFun (X : Bipointed) (a : ((CategoryTheory.Functor.id Bipointed).obj X).X) :
                Bipointed.Hom.toFun (Bipointed.swapEquiv.counitIso.inv.app X) a = a
                source
                @[simp]
                theorem Bipointed.swapEquiv_counitIso_hom_app_toFun (X : Bipointed) (a : ((CategoryTheory.Functor.comp Bipointed.swap Bipointed.swap).obj X).X) :
                Bipointed.Hom.toFun (Bipointed.swapEquiv.counitIso.hom.app X) a = a
                source
                @[simp]
                theorem Bipointed.swapEquiv_inverse_map_toFun :
                ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), Bipointed.Hom.toFun (Bipointed.swapEquiv.inverse.map f) a = Bipointed.Hom.toFun f a
                source
                @[simp]
                theorem Bipointed.swapEquiv_inverse_obj_X (X : Bipointed) :
                (Bipointed.swapEquiv.inverse.obj X).X = X.X
                source
                def Bipointed.swapEquiv :
                Bipointed ≌ Bipointed

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

                Instances For
                  source
                  @[simp]
                  theorem Bipointed.swapEquiv_symm :
                  Bipointed.swapEquiv.symm = Bipointed.swapEquiv
                  source
                  def bipointedToPointedFst :
                  CategoryTheory.Functor Bipointed Pointed

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

                  Instances For
                    source
                    def bipointedToPointedSnd :
                    CategoryTheory.Functor Bipointed Pointed

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

                    Instances For
                      source
                      @[simp]
                      theorem bipointedToPointedFst_comp_forget :
                      CategoryTheory.Functor.comp bipointedToPointedFst (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed
                      source
                      @[simp]
                      theorem bipointedToPointedSnd_comp_forget :
                      CategoryTheory.Functor.comp bipointedToPointedSnd (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed
                      source
                      @[simp]
                      theorem swap_comp_bipointedToPointedFst :
                      CategoryTheory.Functor.comp Bipointed.swap bipointedToPointedFst = bipointedToPointedSnd
                      source
                      @[simp]
                      theorem swap_comp_bipointedToPointedSnd :
                      CategoryTheory.Functor.comp Bipointed.swap bipointedToPointedSnd = bipointedToPointedFst
                      source
                      def pointedToBipointed :
                      CategoryTheory.Functor Pointed Bipointed

                      The functor from Pointed to Bipointed which bipoints the point.

                      Instances For
                        source
                        def pointedToBipointedFst :
                        CategoryTheory.Functor Pointed Bipointed

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

                        Instances For
                          source
                          def pointedToBipointedSnd :
                          CategoryTheory.Functor Pointed Bipointed

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

                          Instances For
                            source
                            @[simp]
                            theorem pointedToBipointedFst_comp_swap :
                            CategoryTheory.Functor.comp pointedToBipointedFst Bipointed.swap = pointedToBipointedSnd
                            source
                            @[simp]
                            theorem pointedToBipointedSnd_comp_swap :
                            CategoryTheory.Functor.comp pointedToBipointedSnd Bipointed.swap = pointedToBipointedFst
                            source
                            @[simp]
                            theorem pointedToBipointedCompBipointedToPointedFst_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) :
                            Pointed.Hom.toFun (pointedToBipointedCompBipointedToPointedFst.inv.app X) a = a
                            source
                            @[simp]
                            theorem pointedToBipointedCompBipointedToPointedFst_hom_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedFst).obj X).X) :
                            Pointed.Hom.toFun (pointedToBipointedCompBipointedToPointedFst.hom.app X) a = a
                            source
                            def pointedToBipointedCompBipointedToPointedFst :
                            CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedFst ≅ CategoryTheory.Functor.id Pointed

                            BipointedToPointed_fst is inverse to PointedToBipointed.

                            Instances For
                              source
                              @[simp]
                              theorem pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedSnd).obj X).X) :
                              Pointed.Hom.toFun (pointedToBipointedCompBipointedToPointedSnd.hom.app X) a = a
                              source
                              @[simp]
                              theorem pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) :
                              Pointed.Hom.toFun (pointedToBipointedCompBipointedToPointedSnd.inv.app X) a = a
                              source
                              def pointedToBipointedCompBipointedToPointedSnd :
                              CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedSnd ≅ CategoryTheory.Functor.id Pointed

                              BipointedToPointed_snd is inverse to PointedToBipointed.

                              Instances For
                                source
                                def pointedToBipointedFstBipointedToPointedFstAdjunction :
                                pointedToBipointedFst ⊣ bipointedToPointedFst

                                The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

                                Instances For
                                  source
                                  def pointedToBipointedSndBipointedToPointedSndAdjunction :
                                  pointedToBipointedSnd ⊣ bipointedToPointedSnd

                                  The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

                                  Instances For