Documentation

Mathlib.CategoryTheory.Category.TwoP

The category of two-pointed types #

This defines TwoP, the category of two-pointed types.

References #

structure TwoP :
Type (u + 1)

The category of two-pointed types.

Instances For
    def TwoP.of {X : Type u_3} (toTwoPointing : TwoPointing X) :

    Turns a two-pointing into a two-pointed type.

    Instances For
      @[simp]
      theorem TwoP.coe_of {X : Type u_3} (toTwoPointing : TwoPointing X) :
      (TwoP.of toTwoPointing).X = X
      def TwoPointing.TwoP {X : Type u_3} (toTwoPointing : TwoPointing X) :

      Alias of TwoP.of.


      Turns a two-pointing into a two-pointed type.

      Instances For
        noncomputable def TwoP.toBipointed (X : TwoP) :

        Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.

        Instances For
          @[simp]
          theorem TwoP.coe_toBipointed (X : TwoP) :
          @[simp]
          theorem TwoP.swap_obj_X (X : TwoP) :
          (TwoP.swap.obj X).X = X.X
          @[simp]
          theorem TwoP.swap_map_toFun :
          ∀ {X Y : TwoP} (f : X Y) (a : (TwoP.toBipointed X).X), Bipointed.Hom.toFun (TwoP.swap.map f) a = Bipointed.Hom.toFun f a
          @[simp]
          theorem TwoP.swap_obj_toTwoPointing (X : TwoP) :
          (TwoP.swap.obj X).toTwoPointing = TwoPointing.swap X.toTwoPointing

          Swaps the pointed elements of a two-pointed type. TwoPointing.swap as a functor.

          Instances For
            @[simp]
            theorem TwoP.swapEquiv_functor_obj_toTwoPointing_toProd (X : TwoP) :
            (TwoP.swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.snd, X.toTwoPointing.fst)
            @[simp]
            theorem TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd (X : TwoP) :
            (TwoP.swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.snd, X.toTwoPointing.fst)
            @[simp]
            theorem TwoP.swapEquiv_functor_obj_X (X : TwoP) :
            (TwoP.swapEquiv.functor.obj X).X = X.X
            @[simp]
            theorem TwoP.swapEquiv_inverse_obj_X (X : TwoP) :
            (TwoP.swapEquiv.inverse.obj X).X = X.X
            @[simp]
            theorem TwoP.swapEquiv_inverse_map_toFun :
            ∀ {X Y : TwoP} (f : X Y) (a : (TwoP.toBipointed X).X), Bipointed.Hom.toFun (TwoP.swapEquiv.inverse.map f) a = Bipointed.Hom.toFun f a
            @[simp]
            theorem TwoP.swapEquiv_unitIso_inv_app_toFun (X : TwoP) :
            ∀ (a : (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).X), Bipointed.Hom.toFun (TwoP.swapEquiv.unitIso.inv.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.snd) })) (CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj (TwoP.swap.obj X))).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj (TwoP.swap.obj X))).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj (TwoP.swap.obj X))).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj (TwoP.swap.obj X))).toProd.snd) }) { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.snd) })) (Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))) a)
            @[simp]
            theorem TwoP.swapEquiv_unitIso_hom_app_toFun (X : TwoP) :
            ∀ (a : (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).X), Bipointed.Hom.toFun (TwoP.swapEquiv.unitIso.hom.app X) a = Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))) (Bipointed.Hom.toFun (CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).toProd.snd) } (CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj (TwoP.swap.obj X))).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj (TwoP.swap.obj X))).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj (TwoP.swap.obj X))).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj (TwoP.swap.obj X))).toProd.snd) }) (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.fst = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.fst), map_snd := (_ : id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.snd = id (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).toProd.snd) })))) a)
            @[simp]
            theorem TwoP.swapEquiv_functor_map_toFun :
            ∀ {X Y : TwoP} (f : X Y) (a : (TwoP.toBipointed X).X), Bipointed.Hom.toFun (TwoP.swapEquiv.functor.map f) a = Bipointed.Hom.toFun f a
            noncomputable def TwoP.swapEquiv :

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

            Instances For
              @[simp]
              @[simp]
              theorem pointedToTwoPFst_obj_toTwoPointing_toProd (X : Pointed) :
              (pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)
              @[simp]
              theorem pointedToTwoPFst_map_toFun :
              ∀ {X Y : Pointed} (f : X Y) (a : Option X.X), Bipointed.Hom.toFun (pointedToTwoPFst.map f) a = Option.map f.toFun a

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

              Instances For
                @[simp]
                @[simp]
                theorem pointedToTwoPSnd_map_toFun :
                ∀ {X Y : Pointed} (f : X Y) (a : Option X.X), Bipointed.Hom.toFun (pointedToTwoPSnd.map f) a = Option.map f.toFun a
                @[simp]
                theorem pointedToTwoPSnd_obj_toTwoPointing_toProd (X : Pointed) :
                (pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)

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

                Instances For