The category of bipointed types

This defines Bipointed, the category of bipointed types.

TODO

Monoidal structure

structure Bipointed : Type (u + 1)

The category of bipointed types.

• X : Type u

  The underlying type of a bipointed type.

• toProd : self.X × self.X

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

instance Bipointed.instCoeSortType : CoeSort Bipointed (Type u_1)

Equations

• Bipointed.instCoeSortType = { coe := Bipointed.X }

@[reducible, inline]

abbrev Bipointed.of {X : Type u_1} (to_prod : X × X) : Bipointed

Turns a bipointing into a bipointed type.

Equations

• Bipointed.of to_prod = { X := X, toProd := to_prod }

theorem Bipointed.coe_of {X : Type u_1} (to_prod : X × X) : (of to_prod).X = X

def Prod.Bipointed {X : Type u_1} (to_prod : X × X) : _root_.Bipointed

Alias of Bipointed.of.

---

Turns a bipointing into a bipointed type.

Equations

• @Prod.Bipointed = @Bipointed.of

instance Bipointed.instInhabited : Inhabited Bipointed

Equations

• Bipointed.instInhabited = { default := Bipointed.of ((), ()) }

structure Bipointed.Hom (X Y : Bipointed) : Type u

Morphisms in Bipointed.

• toFun : X.X → Y.X

  The underlying function of a morphism of bipointed types.

• map_fst : self.toFun X.toProd.1 = Y.toProd.1
• map_snd : self.toFun X.toProd.2 = Y.toProd.2

theorem Bipointed.Hom.ext {X Y : Bipointed} {x y : X.Hom Y} (toFun : x.toFun = y.toFun) : x = y

theorem Bipointed.Hom.ext_iff {X Y : Bipointed} {x y : X.Hom Y} : x = y ↔ x.toFun = y.toFun

def Bipointed.Hom.id (X : Bipointed) : X.Hom X

The identity morphism of X : Bipointed.

Equations

• Bipointed.Hom.id X = { toFun := id, map_fst := ⋯, map_snd := ⋯ }

@[simp]

theorem Bipointed.Hom.id_toFun (X : Bipointed) (a : X.X) : (id X).toFun a = _root_.id a

instance Bipointed.Hom.instInhabited (X : Bipointed) : Inhabited (X.Hom X)

Equations

• Bipointed.Hom.instInhabited X = { default := Bipointed.Hom.id X }

def Bipointed.Hom.comp {X Y Z : Bipointed} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms of Bipointed.

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, map_fst := ⋯, map_snd := ⋯ }

@[simp]

theorem Bipointed.Hom.comp_toFun {X Y Z : Bipointed} (f : X.Hom Y) (g : Y.Hom Z) (a✝ : X.X) : (f.comp g).toFun a✝ = (g.toFun ∘ f.toFun) a✝

instance Bipointed.largeCategory : CategoryTheory.LargeCategory Bipointed

Equations

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

@[reducible, inline]

abbrev Bipointed.HomSubtype (X : Bipointed) (Y : Bipointed) : Type (max 0 u_1 u_2)

The subtype of functions corresponding to the morphisms in Bipointed.

Equations

• X.HomSubtype Y = { f : X.X → Y.X // f X.toProd.1 = Y.toProd.1 ∧ f X.toProd.2 = Y.toProd.2 }

instance Bipointed.instFunLikeHomSubtypeX (X : Bipointed) (Y : Bipointed) : FunLike (X.HomSubtype Y) X.X Y.X

Equations

• X.instFunLikeHomSubtypeX Y = { coe := fun (f : X.HomSubtype Y) => ↑f, coe_injective' := ⋯ }

instance Bipointed.hasForget : CategoryTheory.ConcreteCategory Bipointed HomSubtype

Equations

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

def Bipointed.swap : CategoryTheory.Functor Bipointed Bipointed

Swaps the pointed elements of a bipointed type. Prod.swap as a functor.

Equations

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

@[simp]

theorem Bipointed.swap_obj_X (X : Bipointed) : (swap.obj X).X = X.X

@[simp]

theorem Bipointed.swap_obj_toProd (X : Bipointed) : (swap.obj X).toProd = X.toProd.swap

@[simp]

theorem Bipointed.swap_map_toFun {X✝ Y✝ : Bipointed} (f : X✝ ⟶ Y✝) (a✝ : X✝.X) : (swap.map f).toFun a✝ = f.toFun a✝

def Bipointed.swapEquiv : Bipointed ≌ Bipointed

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

Equations

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

@[simp]

theorem Bipointed.swapEquiv_inverse_map_toFun {X✝ Y✝ : Bipointed} (f : X✝ ⟶ Y✝) (a✝ : X✝.X) : (swapEquiv.inverse.map f).toFun a✝ = f.toFun a✝

@[simp]

theorem Bipointed.swapEquiv_unitIso_inv_app_toFun (X : Bipointed) (a : ((CategoryTheory.Functor.id Bipointed).obj X).X) : (swapEquiv.unitIso.inv.app X).toFun a = a

@[simp]

theorem Bipointed.swapEquiv_counitIso_hom_app_toFun (X : Bipointed) (a : ((swap.comp swap).obj X).X) : (swapEquiv.counitIso.hom.app X).toFun a = a

@[simp]

theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) : (swapEquiv.inverse.obj X).toProd = X.toProd.swap

@[simp]

theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) : (swapEquiv.functor.obj X).toProd = X.toProd.swap

@[simp]

theorem Bipointed.swapEquiv_unitIso_hom_app_toFun (X : Bipointed) (a : ((CategoryTheory.Functor.id Bipointed).obj X).X) : (swapEquiv.unitIso.hom.app X).toFun a = a

@[simp]

theorem Bipointed.swapEquiv_functor_map_toFun {X✝ Y✝ : Bipointed} (f : X✝ ⟶ Y✝) (a✝ : X✝.X) : (swapEquiv.functor.map f).toFun a✝ = f.toFun a✝

@[simp]

theorem Bipointed.swapEquiv_inverse_obj_X (X : Bipointed) : (swapEquiv.inverse.obj X).X = X.X

@[simp]

theorem Bipointed.swapEquiv_counitIso_inv_app_toFun (X : Bipointed) (a : ((swap.comp swap).obj X).X) : (swapEquiv.counitIso.inv.app X).toFun a = a

@[simp]

theorem Bipointed.swapEquiv_functor_obj_X (X : Bipointed) : (swapEquiv.functor.obj X).X = X.X

@[simp]

theorem Bipointed.swapEquiv_symm : swapEquiv.symm = swapEquiv

def bipointedToPointedFst : CategoryTheory.Functor Bipointed Pointed

The forgetful functor from Bipointed to Pointed which forgets about the second point.

Equations

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

def bipointedToPointedSnd : CategoryTheory.Functor Bipointed Pointed

The forgetful functor from Bipointed to Pointed which forgets about the first point.

Equations

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

@[simp]

theorem bipointedToPointedFst_comp_forget : bipointedToPointedFst.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed

@[simp]

theorem bipointedToPointedSnd_comp_forget : bipointedToPointedSnd.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed

@[simp]

theorem swap_comp_bipointedToPointedFst : Bipointed.swap.comp bipointedToPointedFst = bipointedToPointedSnd

@[simp]

theorem swap_comp_bipointedToPointedSnd : Bipointed.swap.comp bipointedToPointedSnd = bipointedToPointedFst

def pointedToBipointed : CategoryTheory.Functor Pointed Bipointed

The functor from Pointed to Bipointed which bipoints the point.

Equations

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

def pointedToBipointedFst : CategoryTheory.Functor Pointed Bipointed

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

Equations

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

def pointedToBipointedSnd : CategoryTheory.Functor Pointed Bipointed

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

Equations

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

@[simp]

theorem pointedToBipointedFst_comp_swap : pointedToBipointedFst.comp Bipointed.swap = pointedToBipointedSnd

@[simp]

theorem pointedToBipointedSnd_comp_swap : pointedToBipointedSnd.comp Bipointed.swap = pointedToBipointedFst

def pointedToBipointedCompBipointedToPointedFst : pointedToBipointed.comp bipointedToPointedFst ≅ CategoryTheory.Functor.id Pointed

BipointedToPointed_fst is inverse to PointedToBipointed.

Equations

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

@[simp]

theorem pointedToBipointedCompBipointedToPointedFst_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) : (pointedToBipointedCompBipointedToPointedFst.inv.app X).toFun a = a

@[simp]

theorem pointedToBipointedCompBipointedToPointedFst_hom_app_toFun (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedFst).obj X).X) : (pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a

def pointedToBipointedCompBipointedToPointedSnd : pointedToBipointed.comp bipointedToPointedSnd ≅ CategoryTheory.Functor.id Pointed

BipointedToPointed_snd is inverse to PointedToBipointed.

Equations

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

@[simp]

theorem pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedSnd).obj X).X) : (pointedToBipointedCompBipointedToPointedSnd.hom.app X).toFun a = a

@[simp]

theorem pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) : (pointedToBipointedCompBipointedToPointedSnd.inv.app X).toFun a = a

def pointedToBipointedFstBipointedToPointedFstAdjunction : pointedToBipointedFst ⊣ bipointedToPointedFst

The free/forgetful adjunction between PointedToBipointed_fst and BipointedToPointed_fst.

Equations

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

def pointedToBipointedSndBipointedToPointedSndAdjunction : pointedToBipointedSnd ⊣ bipointedToPointedSnd

The free/forgetful adjunction between PointedToBipointed_snd and BipointedToPointed_snd.

Equations

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