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)

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.

instance TwoP.instCoeSortTwoPType : CoeSort TwoP (Type u_3)

Equations

• TwoP.instCoeSortTwoPType = { coe := TwoP.X }

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 }

@[simp]

theorem TwoP.coe_of {X : Type u_3} (toTwoPointing : TwoPointing X) : (TwoP.of toTwoPointing).X = X

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

• @TwoPointing.TwoP = @TwoP.of

instance TwoP.instInhabitedTwoP : Inhabited TwoP

Equations

• TwoP.instInhabitedTwoP = { default := TwoP.of TwoPointing.bool }

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

• TwoP.toBipointed X = Prod.Bipointed X.toTwoPointing.toProd

@[simp]

theorem TwoP.coe_toBipointed (X : TwoP) : (TwoP.toBipointed X).X = X.X

noncomputable instance TwoP.largeCategory : CategoryTheory.LargeCategory TwoP

Equations

• TwoP.largeCategory = CategoryTheory.InducedCategory.category TwoP.toBipointed

noncomputable instance TwoP.concreteCategory : CategoryTheory.ConcreteCategory TwoP

Equations

• TwoP.concreteCategory = CategoryTheory.InducedCategory.concreteCategory TwoP.toBipointed

noncomputable instance TwoP.hasForgetToBipointed : CategoryTheory.HasForget₂ TwoP Bipointed

Equations

• TwoP.hasForgetToBipointed = CategoryTheory.InducedCategory.hasForget₂ TwoP.toBipointed

@[simp]

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

@[simp]

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

@[simp]

theorem TwoP.swap_obj_toTwoPointing (X : TwoP) : (TwoP.swap.obj X).toTwoPointing = TwoPointing.swap X.toTwoPointing

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.

@[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)

@[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)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TwoP.swapEquiv_unitIso_inv_app_toFun (X : TwoP) : ∀ (a : (TwoP.toBipointed ((CategoryTheory.Functor.comp TwoP.swap TwoP.swap).obj X)).X), (TwoP.swapEquiv.unitIso.inv.app X).toFun a = (CategoryTheory.CategoryStruct.comp (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })) (CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) { toFun := id, map_fst := ⋯, map_snd := ⋯ })).toFun ((CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))).toFun a)

@[simp]

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

@[simp]

theorem TwoP.swapEquiv_unitIso_hom_app_toFun (X : TwoP) : ∀ (a : (TwoP.toBipointed ((CategoryTheory.Functor.id TwoP).obj X)).X), (TwoP.swapEquiv.unitIso.hom.app X).toFun a = (CategoryTheory.CategoryStruct.id (TwoP.swap.obj (TwoP.swap.obj X))).toFun ((CategoryTheory.CategoryStruct.comp { toFun := id, map_fst := ⋯, map_snd := ⋯ } (CategoryTheory.CategoryStruct.comp (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })))).toFun a)

@[simp]

theorem TwoP.swapEquiv_functor_map_toFun : ∀ {X Y : TwoP} (f : X ⟶ Y) (a : (TwoP.toBipointed X).X), (TwoP.swapEquiv.functor.map f).toFun a = f.toFun a

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.

@[simp]

theorem TwoP.swapEquiv_symm : TwoP.swapEquiv.symm = TwoP.swapEquiv

@[simp]

theorem TwoP_swap_comp_forget_to_Bipointed : CategoryTheory.Functor.comp TwoP.swap (CategoryTheory.forget₂ TwoP Bipointed) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ TwoP Bipointed) Bipointed.swap

@[simp]

theorem pointedToTwoPFst_obj_X (X : Pointed) : (pointedToTwoPFst.obj X).X = Option X.X

@[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), (pointedToTwoPFst.map f).toFun a = Option.map f.toFun a

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.

@[simp]

theorem pointedToTwoPSnd_obj_X (X : Pointed) : (pointedToTwoPSnd.obj X).X = Option X.X

@[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

@[simp]

theorem pointedToTwoPSnd_obj_toTwoPointing_toProd (X : Pointed) : (pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)

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.

@[simp]

theorem pointedToTwoPFst_comp_swap : CategoryTheory.Functor.comp pointedToTwoPFst TwoP.swap = pointedToTwoPSnd

@[simp]

theorem pointedToTwoPSnd_comp_swap : CategoryTheory.Functor.comp pointedToTwoPSnd TwoP.swap = pointedToTwoPFst

@[simp]

theorem pointedToTwoPFst_comp_forget_to_bipointed : CategoryTheory.Functor.comp pointedToTwoPFst (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedFst

@[simp]

theorem pointedToTwoPSnd_comp_forget_to_bipointed : CategoryTheory.Functor.comp pointedToTwoPSnd (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedSnd

noncomputable def pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction : pointedToTwoPFst ⊣ CategoryTheory.Functor.comp (CategoryTheory.forget₂ TwoP Bipointed) 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.

noncomputable def pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction : pointedToTwoPSnd ⊣ CategoryTheory.Functor.comp (CategoryTheory.forget₂ TwoP Bipointed) 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.