The category of two-pointed types #
This defines TwoP
, the category of two-pointed types.
References #
- [nLab, coalgebra of the real interval] (https://ncatlab.org/nlab/show/coalgebra+of+the+real+interval)
Turns a two-pointing into a two-pointed type.
Instances For
@[simp]
Alias of TwoP.of
.
Turns a two-pointing into a two-pointed type.
Instances For
Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.
Instances For
@[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]
@[simp]
theorem
TwoP.swapEquiv_counitIso_hom_app_toFun
(X : TwoP)
(a : (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).X)
:
Bipointed.Hom.toFun (TwoP.swapEquiv.counitIso.hom.app X) a = a
@[simp]
@[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_counitIso_inv_app_toFun
(X : TwoP)
(a : (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).X)
:
Bipointed.Hom.toFun (TwoP.swapEquiv.counitIso.inv.app X) a = 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
@[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
@[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)
Adding a second point is left adjoint to forgetting the second point.
Instances For
Adding a first point is left adjoint to forgetting the first point.