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

TwoP.instCoeSortType = { coe := TwoP.X }

source

@[reducible, inline]

abbrev 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 }

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

@TwoPointing.TwoP = @TwoP.of

Instances For

source

instance TwoP.instInhabited :

Inhabited TwoP

Equations

TwoP.instInhabited = { default := TwoP.of TwoPointing.bool }

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

X.toBipointed = X.toTwoPointing.Bipointed

Instances For

source

@[simp]

theorem TwoP.coe_toBipointed (X : TwoP) :

X.toBipointed.X = X.X

source

noncomputable instance TwoP.largeCategory :

CategoryTheory.LargeCategory TwoP

Equations

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

source

noncomputable instance TwoP.concreteCategory :

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

Equations

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

source

noncomputable instance TwoP.hasForgetToBipointed :

CategoryTheory.HasForget₂ TwoP Bipointed

Equations

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

source

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.

Instances For

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

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

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.

Instances For

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_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_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_inverse_obj_X (X : TwoP) :

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

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_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_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_X (X : TwoP) :

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

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

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

Instances For

source

@[simp]

theorem pointedToTwoPFst_obj_toTwoPointing_toProd (X : Pointed) :

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

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

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.

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

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

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

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

Instances For

Documentation

Mathlib.CategoryTheory.Category.TwoP

The category of two-pointed types #

References #