Documentation

Mathlib.CategoryTheory.Category.TwoP

The category of two-pointed types #

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

References #

source
🔶 coverage
structure TwoP :
Type (u + 1)

The category of two-pointed types.

  • X : Type u

    The underlying type of a two-pointed type.

  • toTwoPointing : TwoPointing self.X

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

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance TwoP.instCoeSortType :
    CoeSort TwoP (Type u_3)
    source
    🔸 coverage
    @[reducible, inline]
    abbrev TwoP.of {X : Type u_3} (toTwoPointing : TwoPointing X) :
    TwoP

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

    Instances For
      source
      📐 coverage
      theorem TwoP.coe_of {X : Type u_3} (toTwoPointing : TwoPointing X) :
      (of toTwoPointing).X = X
      source
      🔸 coverage
      def TwoPointing.TwoP {X : Type u_3} (toTwoPointing : TwoPointing X) :
      _root_.TwoP

      Alias of TwoP.of.

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

      Instances For
        source
        🔸 coverage
        @[implicit_reducible]
        instance TwoP.instInhabited :
        Inhabited TwoP
        source
        🔸 coverage
        noncomputable def TwoP.toBipointed (X : TwoP) :
        Bipointed

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

        Instances For
          source
          📐 coverage
          @[simp]
          theorem TwoP.coe_toBipointed (X : TwoP) :
          X.toBipointed.X = X.X
          source
          🔸 coverage
          @[implicit_reducible]
          noncomputable instance TwoP.largeCategory :
          CategoryTheory.LargeCategory TwoP
          source
          🔸 coverage
          @[implicit_reducible]
          noncomputable instance TwoP.concreteCategory :
          CategoryTheory.ConcreteCategory TwoP fun (X Y : TwoP) => X.toBipointed.HomSubtype Y.toBipointed
          source
          🔸 coverage
          @[implicit_reducible]
          noncomputable instance TwoP.hasForgetToBipointed :
          CategoryTheory.HasForget₂ TwoP Bipointed
          source
          theorem TwoP.hom_ext {X Y : TwoP} {f g : X ⟶ Y} (h : f.hom = g.hom) :
          f = g
          source
          📐 coverage
          theorem TwoP.hom_ext_iff {X Y : TwoP} {f g : X ⟶ Y} :
          f = g ↔ f.hom = g.hom
          source
          🔸 coverage
          noncomputable def TwoP.swap :
          CategoryTheory.Functor TwoP TwoP

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

          Instances For
            source
            📐 coverage
            @[simp]
            theorem TwoP.swap_map {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) :
            swap.map f = CategoryTheory.InducedCategory.homMk { toFun := ⇑(CategoryTheory.ConcreteCategory.hom f.hom), map_fst := ⋯, map_snd := ⋯ }
            source
            📐 coverage
            @[simp]
            theorem TwoP.swap_obj_toTwoPointing (X : TwoP) :
            (swap.obj X).toTwoPointing = X.toTwoPointing.swap
            source
            📐 coverage
            @[simp]
            theorem TwoP.swap_obj_X (X : TwoP) :
            (swap.obj X).X = X.X
            source
            🔸 coverage
            noncomputable def TwoP.swapEquiv :
            TwoP ≌ TwoP

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

            Instances For
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_counitIso_hom_app_hom_toFun (X : TwoP) (a : ((swap.comp swap).obj X).toBipointed.X) :
              (swapEquiv.counitIso.hom.app X).hom.toFun a = a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_counitIso_inv_app_hom_toFun (X : TwoP) (a : ((swap.comp swap).obj X).toBipointed.X) :
              (swapEquiv.counitIso.inv.app X).hom.toFun a = a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_inverse_map_hom_toFun {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) (a : X✝.toBipointed.X) :
              (swapEquiv.inverse.map f).hom.toFun a = (CategoryTheory.ConcreteCategory.hom f.hom) a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_unitIso_inv_app_hom_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :
              (swapEquiv.unitIso.inv.app X).hom.toFun a = a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_functor_obj_toTwoPointing_toProd (X : TwoP) :
              (swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd (X : TwoP) :
              (swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_inverse_obj_X (X : TwoP) :
              (swapEquiv.inverse.obj X).X = X.X
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_functor_map_hom_toFun {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) (a : X✝.toBipointed.X) :
              (swapEquiv.functor.map f).hom.toFun a = (CategoryTheory.ConcreteCategory.hom f.hom) a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_unitIso_hom_app_hom_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :
              (swapEquiv.unitIso.hom.app X).hom.toFun a = a
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_functor_obj_X (X : TwoP) :
              (swapEquiv.functor.obj X).X = X.X
              source
              📐 coverage
              @[simp]
              theorem TwoP.swapEquiv_symm :
              swapEquiv.symm = swapEquiv
              source
              📐 coverage
              @[simp]
              theorem TwoP_swap_comp_forget_to_Bipointed :
              TwoP.swap.comp (CategoryTheory.forget₂ TwoP Bipointed) = (CategoryTheory.forget₂ TwoP Bipointed).comp Bipointed.swap
              source
              🔸 coverage
              noncomputable def pointedToTwoPFst :
              CategoryTheory.Functor Pointed TwoP

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

              Instances For
                source
                📐 coverage
                @[simp]
                theorem pointedToTwoPFst_obj_X (X : Pointed) :
                (pointedToTwoPFst.obj X).X = Option X.X
                source
                📐 coverage
                @[simp]
                theorem pointedToTwoPFst_map_hom_toFun {X✝ Y✝ : Pointed} (f : X✝ ⟶ Y✝) (a✝ : Option X✝.X) :
                (pointedToTwoPFst.map f).hom.toFun a✝ = Option.map f.toFun a✝
                source
                📐 coverage
                @[simp]
                theorem pointedToTwoPFst_obj_toTwoPointing_toProd (X : Pointed) :
                (pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)
                source
                🔸 coverage
                noncomputable def pointedToTwoPSnd :
                CategoryTheory.Functor Pointed TwoP

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

                Instances For
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPSnd_obj_toTwoPointing_toProd (X : Pointed) :
                  (pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPSnd_map_hom_toFun {X✝ Y✝ : Pointed} (f : X✝ ⟶ Y✝) (a✝ : Option X✝.X) :
                  (pointedToTwoPSnd.map f).hom.toFun a✝ = Option.map f.toFun a✝
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPSnd_obj_X (X : Pointed) :
                  (pointedToTwoPSnd.obj X).X = Option X.X
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPFst_comp_swap :
                  pointedToTwoPFst.comp TwoP.swap = pointedToTwoPSnd
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPSnd_comp_swap :
                  pointedToTwoPSnd.comp TwoP.swap = pointedToTwoPFst
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPFst_comp_forget_to_bipointed :
                  pointedToTwoPFst.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedFst
                  source
                  📐 coverage
                  @[simp]
                  theorem pointedToTwoPSnd_comp_forget_to_bipointed :
                  pointedToTwoPSnd.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedSnd
                  source
                  🔸 coverage
                  noncomputable def pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction :
                  pointedToTwoPFst ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedFst

                  Adding a second point is left adjoint to forgetting the second point.

                  Instances For
                    source
                    🔸 coverage
                    noncomputable def pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction :
                    pointedToTwoPSnd ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedSnd

                    Adding a first point is left adjoint to forgetting the first point.

                    Instances For