Documentation

Mathlib.CategoryTheory.Category.TwoP

The category of two-pointed types #

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

References #

source
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
instance TwoP.instCoeSortType :
CoeSort TwoP (Type u_3)
Equations
source
def TwoP.of {X : Type u_3} (toTwoPointing : TwoPointing X) :
TwoP

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

Equations
  • TwoP.of toTwoPointing = { X := X, toTwoPointing := toTwoPointing }
source
@[simp]
theorem TwoP.coe_of {X : Type u_3} (toTwoPointing : TwoPointing X) :
(TwoP.of toTwoPointing).X = X
source
def TwoPointing.TwoP {X : Type u_3} (toTwoPointing : TwoPointing X) :
TwoP

Alias of TwoP.of.

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

Equations
source
instance TwoP.instInhabited :
Inhabited TwoP
Equations
source
noncomputable def TwoP.toBipointed (X : TwoP) :
Bipointed

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

Equations
  • X.toBipointed = X.toTwoPointing.Bipointed
source
@[simp]
theorem TwoP.coe_toBipointed (X : TwoP) :
X.toBipointed.X = X.X
source
noncomputable instance TwoP.largeCategory :
CategoryTheory.LargeCategory TwoP
Equations
source
noncomputable instance TwoP.concreteCategory :
CategoryTheory.ConcreteCategory TwoP
Equations
source
noncomputable instance TwoP.hasForgetToBipointed :
CategoryTheory.HasForget₂ TwoP Bipointed
Equations
source
@[simp]
theorem TwoP.swap_obj_toTwoPointing (X : TwoP) :
(TwoP.swap.obj X).toTwoPointing = X.toTwoPointing.swap
source
@[simp]
theorem TwoP.swap_obj_X (X : TwoP) :
(TwoP.swap.obj X).X = X.X
source
@[simp]
theorem TwoP.swap_map_toFun :
∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swap.map f).toFun a = f.toFun a
source
noncomputable def TwoP.swap :
CategoryTheory.Functor TwoP TwoP

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem TwoP.swapEquiv_inverse_obj_X (X : TwoP) :
(TwoP.swapEquiv.inverse.obj X).X = X.X
source
@[simp]
theorem TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd (X : TwoP) :
(TwoP.swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
source
@[simp]
theorem TwoP.swapEquiv_unitIso_hom_app_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :
(TwoP.swapEquiv.unitIso.hom.app X).toFun a = a
source
@[simp]
theorem TwoP.swapEquiv_counitIso_inv_app_toFun (X : TwoP) (a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X) :
(TwoP.swapEquiv.counitIso.inv.app X).toFun a = a
source
@[simp]
theorem TwoP.swapEquiv_functor_map_toFun :
∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.functor.map f).toFun a = f.toFun a
source
@[simp]
theorem TwoP.swapEquiv_inverse_map_toFun :
∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.inverse.map f).toFun a = f.toFun a
source
@[simp]
theorem TwoP.swapEquiv_functor_obj_toTwoPointing_toProd (X : TwoP) :
(TwoP.swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
source
@[simp]
theorem TwoP.swapEquiv_functor_obj_X (X : TwoP) :
(TwoP.swapEquiv.functor.obj X).X = X.X
source
@[simp]
theorem TwoP.swapEquiv_unitIso_inv_app_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :
(TwoP.swapEquiv.unitIso.inv.app X).toFun a = a
source
@[simp]
theorem TwoP.swapEquiv_counitIso_hom_app_toFun (X : TwoP) (a : ((TwoP.swap.comp TwoP.swap).obj X).toBipointed.X) :
(TwoP.swapEquiv.counitIso.hom.app X).toFun a = a
source
noncomputable def TwoP.swapEquiv :
TwoP ≌ TwoP

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem TwoP.swapEquiv_symm :
TwoP.swapEquiv.symm = TwoP.swapEquiv
source
@[simp]
theorem TwoP_swap_comp_forget_to_Bipointed :
TwoP.swap.comp (CategoryTheory.forget₂ TwoP Bipointed) = (CategoryTheory.forget₂ TwoP Bipointed).comp Bipointed.swap
source
@[simp]
theorem pointedToTwoPFst_obj_toTwoPointing_toProd (X : Pointed) :
(pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)
source
@[simp]
theorem pointedToTwoPFst_obj_X (X : Pointed) :
(pointedToTwoPFst.obj X).X = Option X.X
source
@[simp]
theorem pointedToTwoPFst_map_toFun :
∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPFst.map f).toFun a = Option.map f.toFun a
source
noncomputable def pointedToTwoPFst :
CategoryTheory.Functor Pointed TwoP

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem pointedToTwoPSnd_obj_toTwoPointing_toProd (X : Pointed) :
(pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)
source
@[simp]
theorem pointedToTwoPSnd_obj_X (X : Pointed) :
(pointedToTwoPSnd.obj X).X = Option X.X
source
@[simp]
theorem pointedToTwoPSnd_map_toFun :
∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPSnd.map f).toFun a = Option.map f.toFun a
source
noncomputable def pointedToTwoPSnd :
CategoryTheory.Functor Pointed TwoP

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem pointedToTwoPFst_comp_swap :
pointedToTwoPFst.comp TwoP.swap = pointedToTwoPSnd
source
@[simp]
theorem pointedToTwoPSnd_comp_swap :
pointedToTwoPSnd.comp TwoP.swap = pointedToTwoPFst
source
@[simp]
theorem pointedToTwoPFst_comp_forget_to_bipointed :
pointedToTwoPFst.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedFst
source
@[simp]
theorem pointedToTwoPSnd_comp_forget_to_bipointed :
pointedToTwoPSnd.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedSnd
source
noncomputable def pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction :
pointedToTwoPFst ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedFst

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

Equations
  • One or more equations did not get rendered due to their size.
source
noncomputable def pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction :
pointedToTwoPSnd ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedSnd

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

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