The category of bipointed types #

This defines Bipointed, the category of bipointed types.

TODO #

Monoidal structure

source

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.

Instances For

source

instance Bipointed.instCoeSortType :

CoeSort Bipointed (Type u_1)

Equations

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

source

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

Instances For

source

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

(of to_prod).X = X

source

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

Instances For

source

instance Bipointed.instInhabited :

Inhabited Bipointed

Equations

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

source

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

Instances For

source

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

x = y

source

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 := ⋯ }

Instances For

source

@[simp]

theorem Bipointed.Hom.id_toFun (X : Bipointed) (a : X.X) :

(id X).toFun a = _root_.id a

source

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

Inhabited (X.Hom X)

Equations

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

source

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 := ⋯ }

Instances For

source

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

source

instance Bipointed.largeCategory :

CategoryTheory.LargeCategory Bipointed

Equations

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

source

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

Instances For

source

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' := ⋯ }

source

instance Bipointed.hasForget :

CategoryTheory.ConcreteCategory Bipointed HomSubtype

Equations

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

source

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.

Instances For

source

@[simp]

theorem Bipointed.swap_obj_X (X : Bipointed) :

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

source

@[simp]

theorem Bipointed.swap_obj_toProd (X : Bipointed) :

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

source

@[simp]

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

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

source

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.

Instances For

source

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

source

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

source

@[simp]

theorem Bipointed.swapEquiv_inverse_obj_toProd (X : Bipointed) :

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

source

@[simp]

theorem Bipointed.swapEquiv_functor_obj_toProd (X : Bipointed) :

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

source

@[simp]

theorem Bipointed.swapEquiv_inverse_obj_X (X : Bipointed) :

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem Bipointed.swapEquiv_functor_obj_X (X : Bipointed) :

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

source

@[simp]

theorem Bipointed.swapEquiv_symm :

swapEquiv.symm = swapEquiv

source

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.

Instances For

source

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.

Instances For

source

@[simp]

theorem bipointedToPointedFst_comp_forget :

bipointedToPointedFst.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed

source

@[simp]

theorem bipointedToPointedSnd_comp_forget :

bipointedToPointedSnd.comp (CategoryTheory.forget Pointed) = CategoryTheory.forget Bipointed

source

@[simp]

theorem swap_comp_bipointedToPointedFst :

Bipointed.swap.comp bipointedToPointedFst = bipointedToPointedSnd

source

@[simp]

theorem swap_comp_bipointedToPointedSnd :

Bipointed.swap.comp bipointedToPointedSnd = bipointedToPointedFst

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

@[simp]

theorem pointedToBipointedFst_comp_swap :

pointedToBipointedFst.comp Bipointed.swap = pointedToBipointedSnd

source

@[simp]

theorem pointedToBipointedSnd_comp_swap :

pointedToBipointedSnd.comp Bipointed.swap = pointedToBipointedFst

source

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.

Instances For

source

@[simp]

theorem pointedToBipointedCompBipointedToPointedFst_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) :

(pointedToBipointedCompBipointedToPointedFst.inv.app X).toFun a = a

source

@[simp]

theorem pointedToBipointedCompBipointedToPointedFst_hom_app_toFun (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedFst).obj X).X) :

(pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a

source

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.

Instances For

source

@[simp]

theorem pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun (X : Pointed) (a : ((pointedToBipointed.comp bipointedToPointedSnd).obj X).X) :

(pointedToBipointedCompBipointedToPointedSnd.hom.app X).toFun a = a

source

@[simp]

theorem pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) :

(pointedToBipointedCompBipointedToPointedSnd.inv.app X).toFun a = a

source

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.

Instances For

source

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.

Instances For

Documentation

Mathlib.CategoryTheory.Category.Bipointed

The category of bipointed types #

TODO #