mathlib3 documentation

category_theory.category.Bipointed

The category of bipointed types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines Bipointed, the category of bipointed types.

TODO #

Monoidal structure

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

Turns a bipointing into a bipointed type.

Equations
@[simp]
theorem Bipointed.coe_of {X : Type u_1} (to_prod : X × X) :
(Bipointed.of to_prod) = X
def prod.Bipointed {X : Type u_1} (to_prod : X × X) :

Alias of Bipointed.of.

theorem Bipointed.hom.ext {X Y : Bipointed} (x y : X.hom Y) (h : x.to_fun = y.to_fun) :
x = y
theorem Bipointed.hom.ext_iff {X Y : Bipointed} (x y : X.hom Y) :
x = y x.to_fun = y.to_fun
@[ext]
structure Bipointed.hom (X Y : Bipointed) :

Morphisms in Bipointed.

Instances for Bipointed.hom
def Bipointed.hom.id (X : Bipointed) :
X.hom X

The identity morphism of X : Bipointed.

Equations
@[simp]
theorem Bipointed.hom.id_to_fun (X : Bipointed) (a : X) :
@[protected, instance]
Equations
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
@[simp]
theorem Bipointed.hom.comp_to_fun {X Y Z : Bipointed} (f : X.hom Y) (g : Y.hom Z) (ᾰ : X) :
(f.comp g).to_fun = (g.to_fun f.to_fun)
@[protected, instance]
Equations
@[protected, instance]
Equations

Swaps the pointed elements of a bipointed type. prod.swap as a functor.

Equations
@[simp]
theorem Bipointed.swap_map_to_fun (X Y : Bipointed) (f : X Y) (ᾰ : X) :

The equivalence between Bipointed and itself induced by prod.swap both ways.

Equations
@[simp]
@[simp]

The forgetful functor from Bipointed to Pointed which forgets about the second point.

Equations

The forgetful functor from Bipointed to Pointed which forgets about the first point.

Equations

The functor from Pointed to Bipointed which bipoints the point.

Equations

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

Equations

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

Equations