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.instCoeSortBipointedType : CoeSort Bipointed (Type u_3)

Equations

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

def Bipointed.of {X : Type u_3} (to_prod : X × X) : Bipointed

Turns a bipointing into a bipointed type.

Equations

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

@[simp]

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

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

Alias of Bipointed.of.

---

Turns a bipointing into a bipointed type.

Equations

• @Prod.Bipointed = @Bipointed.of

instance Bipointed.instInhabitedBipointed : Inhabited Bipointed

Equations

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

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) : x = y ↔ x.toFun = y.toFun

structure Bipointed.Hom (X : Bipointed) (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

@[simp]

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

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

The identity morphism of X : Bipointed.

Equations

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

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

Equations

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

@[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.comp f g).toFun 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.

Equations

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

instance Bipointed.largeCategory : CategoryTheory.LargeCategory Bipointed

Equations

• Bipointed.largeCategory = CategoryTheory.Category.mk @Bipointed.largeCategory.proof_1 @Bipointed.largeCategory.proof_2 @Bipointed.largeCategory.proof_3

instance Bipointed.concreteCategory : CategoryTheory.ConcreteCategory Bipointed

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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.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.swapEquiv.unitIso.inv.app X).toFun a = (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })) (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) { toFun := id, map_fst := ⋯, map_snd := ⋯ })).toFun ((CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun a)

@[simp]

theorem Bipointed.swapEquiv_functor_map_toFun : ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swapEquiv.functor.map f).toFun a = f.toFun 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.swapEquiv.unitIso.hom.app X).toFun a = (CategoryTheory.CategoryStruct.id (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun ((CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := ⋯, map_snd := ⋯ } (CategoryTheory.CategoryStruct.comp (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })))).toFun a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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_symm : Bipointed.swapEquiv.symm = Bipointed.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 : CategoryTheory.Functor.comp bipointedToPointedFst (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed

@[simp]

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

@[simp]

theorem swap_comp_bipointedToPointedFst : CategoryTheory.Functor.comp Bipointed.swap bipointedToPointedFst = bipointedToPointedSnd

@[simp]

theorem swap_comp_bipointedToPointedSnd : CategoryTheory.Functor.comp Bipointed.swap 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 : CategoryTheory.Functor.comp pointedToBipointedFst Bipointed.swap = pointedToBipointedSnd

@[simp]

theorem pointedToBipointedSnd_comp_swap : CategoryTheory.Functor.comp pointedToBipointedSnd Bipointed.swap = pointedToBipointedFst

@[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 : ((CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedFst).obj X).X) : (pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a

def pointedToBipointedCompBipointedToPointedFst : CategoryTheory.Functor.comp pointedToBipointed 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 pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.comp pointedToBipointed 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 pointedToBipointedCompBipointedToPointedSnd : CategoryTheory.Functor.comp pointedToBipointed bipointedToPointedSnd ≅ CategoryTheory.Functor.id Pointed

BipointedToPointed_snd is inverse to PointedToBipointed.

Equations

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

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.