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)

source

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.

Instances For

source

instance TwoP.instCoeSortType :

CoeSort TwoP (Type u_3)

Equations

source

@[reducible, inline]

abbrev TwoP.of {X : Type u_3} (toTwoPointing : TwoPointing X) :

TwoP

Turns a two-pointing into a two-pointed type.

Equations

Instances For

source

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

(of toTwoPointing).X = X

source

def TwoPointing.TwoP {X : Type u_3} (toTwoPointing : TwoPointing X) :

_root_.TwoP

Alias of TwoP.of.

Turns a two-pointing into a two-pointed type.

Equations

Instances For

source

instance TwoP.instInhabited :

Inhabited TwoP

Equations

source

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

Instances For

source

@[simp]

theorem TwoP.coe_toBipointed (X : TwoP) :

X.toBipointed.X = X.X

source

noncomputable instance TwoP.largeCategory :

CategoryTheory.LargeCategory TwoP

Equations

source

noncomputable instance TwoP.concreteCategory :

CategoryTheory.ConcreteCategory TwoP fun (X Y : TwoP) => X.toBipointed.HomSubtype Y.toBipointed

Equations

source

noncomputable instance TwoP.hasForgetToBipointed :

CategoryTheory.HasForget₂ TwoP Bipointed

Equations

source

noncomputable def TwoP.swap :

CategoryTheory.Functor TwoP TwoP

Swaps the pointed elements of a two-pointed type. TwoPointing.swap as a functor.

Equations

Instances For

source

@[simp]

theorem TwoP.swap_map_toFun {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) (a✝ : X✝.toBipointed.X) :

(swap.map f).toFun a✝ = f.toFun a✝

source

@[simp]

theorem TwoP.swap_obj_X (X : TwoP) :

(swap.obj X).X = X.X

source

@[simp]

theorem TwoP.swap_obj_toTwoPointing (X : TwoP) :

(swap.obj X).toTwoPointing = X.toTwoPointing.swap

source

noncomputable def TwoP.swapEquiv :

TwoP ≌ TwoP

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

Equations

Instances For

source

@[simp]

theorem TwoP.swapEquiv_functor_map_toFun {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) (a✝ : X✝.toBipointed.X) :

(swapEquiv.functor.map f).toFun a✝ = f.toFun a✝

source

@[simp]

theorem TwoP.swapEquiv_unitIso_hom_app_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :

(swapEquiv.unitIso.hom.app X).toFun a = a

source

@[simp]

theorem TwoP.swapEquiv_inverse_map_toFun {X✝ Y✝ : TwoP} (f : X✝ ⟶ Y✝) (a✝ : X✝.toBipointed.X) :

(swapEquiv.inverse.map f).toFun a✝ = f.toFun a✝

source

@[simp]

theorem TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd (X : TwoP) :

(swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)

source

@[simp]

theorem TwoP.swapEquiv_counitIso_inv_app_toFun (X : TwoP) (a : ((swap.comp swap).obj X).toBipointed.X) :

(swapEquiv.counitIso.inv.app X).toFun a = a

source

@[simp]

theorem TwoP.swapEquiv_unitIso_inv_app_toFun (X : TwoP) (a : ((CategoryTheory.Functor.id TwoP).obj X).toBipointed.X) :

(swapEquiv.unitIso.inv.app X).toFun a = a

source

@[simp]

theorem TwoP.swapEquiv_functor_obj_X (X : TwoP) :

(swapEquiv.functor.obj X).X = X.X

source

@[simp]

theorem TwoP.swapEquiv_inverse_obj_X (X : TwoP) :

(swapEquiv.inverse.obj X).X = X.X

source

@[simp]

theorem TwoP.swapEquiv_counitIso_hom_app_toFun (X : TwoP) (a : ((swap.comp swap).obj X).toBipointed.X) :

(swapEquiv.counitIso.hom.app X).toFun a = a

source

@[simp]

theorem TwoP.swapEquiv_functor_obj_toTwoPointing_toProd (X : TwoP) :

(swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)

source

@[simp]

theorem TwoP.swapEquiv_symm :

swapEquiv.symm = swapEquiv

source

@[simp]

theorem TwoP_swap_comp_forget_to_Bipointed :

TwoP.swap.comp (CategoryTheory.forget₂ TwoP Bipointed) = (CategoryTheory.forget₂ TwoP Bipointed).comp Bipointed.swap

source

noncomputable def pointedToTwoPFst :

CategoryTheory.Functor Pointed TwoP

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

Equations

Instances For

source

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

source

@[simp]

theorem pointedToTwoPFst_obj_X (X : Pointed) :

(pointedToTwoPFst.obj X).X = Option X.X

source

@[simp]

theorem pointedToTwoPFst_obj_toTwoPointing_toProd (X : Pointed) :

(pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none )

source

noncomputable def pointedToTwoPSnd :

CategoryTheory.Functor Pointed TwoP

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

Equations

Instances For

source

@[simp]

theorem pointedToTwoPSnd_obj_X (X : Pointed) :

(pointedToTwoPSnd.obj X).X = Option X.X

source

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

source

@[simp]

theorem pointedToTwoPSnd_obj_toTwoPointing_toProd (X : Pointed) :

(pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none , some X.point)

source

@[simp]

theorem pointedToTwoPFst_comp_swap :

pointedToTwoPFst.comp TwoP.swap = pointedToTwoPSnd

source

@[simp]

theorem pointedToTwoPSnd_comp_swap :

pointedToTwoPSnd.comp TwoP.swap = pointedToTwoPFst

source

@[simp]

theorem pointedToTwoPFst_comp_forget_to_bipointed :

pointedToTwoPFst.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedFst

source

@[simp]

theorem pointedToTwoPSnd_comp_forget_to_bipointed :

pointedToTwoPSnd.comp (CategoryTheory.forget₂ TwoP Bipointed) = pointedToBipointedSnd

source

noncomputable def pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction :

pointedToTwoPFst ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedFst

Adding a second point is left adjoint to forgetting the second point.

Equations

Instances For

source

noncomputable def pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction :

pointedToTwoPSnd ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedSnd

Adding a first point is left adjoint to forgetting the first point.

Equations

Instances For

Documentation

Mathlib.CategoryTheory.Category.TwoP

The category of two-pointed types #

References #