The category of bipointed types #
This defines Bipointed
, the category of bipointed types.
TODO #
Monoidal structure
Turns a bipointing into a bipointed type.
Instances For
@[simp]
Alias of Bipointed.of
.
Turns a bipointing into a bipointed type.
Instances For
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
theorem
Bipointed.Hom.ext_iff
{X : Bipointed}
{Y : Bipointed}
(x : Bipointed.Hom X Y)
(y : Bipointed.Hom X Y)
:
- toFun : X.X → Y.X
- map_fst : Bipointed.Hom.toFun s X.toProd.fst = Y.toProd.fst
- map_snd : Bipointed.Hom.toFun s X.toProd.snd = Y.toProd.snd
Morphisms in Bipointed
.
Instances For
@[simp]
theorem
Bipointed.Hom.id_toFun
(X : Bipointed)
(a : X.X)
:
Bipointed.Hom.toFun (Bipointed.Hom.id X) a = id a
@[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
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
@[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
@[simp]
theorem
Bipointed.swap_obj_toProd
(X : Bipointed)
:
(Bipointed.swap.obj X).toProd = Prod.swap X.toProd
Swaps the pointed elements of a bipointed type. Prod.swap
as a functor.
Instances For
@[simp]
theorem
Bipointed.swapEquiv_functor_obj_toProd
(X : Bipointed)
:
(Bipointed.swapEquiv.functor.obj X).toProd = Prod.swap X.toProd
@[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)
@[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
@[simp]
theorem
Bipointed.swapEquiv_inverse_obj_toProd
(X : Bipointed)
:
(Bipointed.swapEquiv.inverse.obj X).toProd = Prod.swap X.toProd
@[simp]
theorem
Bipointed.swapEquiv_functor_obj_X
(X : Bipointed)
:
(Bipointed.swapEquiv.functor.obj X).X = X.X
@[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)
@[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
@[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
@[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
@[simp]
theorem
Bipointed.swapEquiv_inverse_obj_X
(X : Bipointed)
:
(Bipointed.swapEquiv.inverse.obj X).X = X.X
@[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
@[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
BipointedToPointed_fst
is inverse to PointedToBipointed
.
Instances For
@[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
@[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
BipointedToPointed_snd
is inverse to PointedToBipointed
.
Instances For
The free/forgetful adjunction between PointedToBipointed_fst
and BipointedToPointed_fst
.
Instances For
The free/forgetful adjunction between PointedToBipointed_snd
and BipointedToPointed_snd
.