category_theory.category.Bipointed

source

structure Bipointed :

Type (u+1)

X : Type ?
to_prod : self.X × self.X

The category of bipointed types.

source

@[protected, instance]

def Bipointed.has_coe_to_sort :

has_coe_to_sort Bipointed (Type u_1)

Equations

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

source

def 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, to_prod := to_prod}

source

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

Bipointed

Alias of of.

source

@[protected, instance]

def Bipointed.inhabited :

inhabited Bipointed

Equations

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

source

theorem Bipointed.hom.ext {X Y : Bipointed} (x y : X.hom Y) (h : x.to_fun = y.to_fun) :

x = y

source

theorem Bipointed.hom.ext_iff {X Y : Bipointed} (x y : X.hom Y) :

x = y ↔ x.to_fun = y.to_fun

source

@[ext]

structure Bipointed.hom (X Y : Bipointed) :

Type u

to_fun : ↥X → ↥Y
map_fst : self.to_fun X.to_prod.fst = Y.to_prod.fst
map_snd : self.to_fun X.to_prod.snd = Y.to_prod.snd

Morphisms in Bipointed.

source

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

X.hom X

The identity morphism of X : Bipointed.

Equations

Bipointed.hom.id X = {to_fun := id ↥X, map_fst := _, map_snd := _}

source

@[simp]

theorem Bipointed.hom.id_to_fun (X : Bipointed) (a : ↥X) :

(Bipointed.hom.id X).to_fun a = id a

source

@[protected, instance]

def Bipointed.hom.inhabited (X : Bipointed) :

inhabited (X.hom X)

Equations

Bipointed.hom.inhabited 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 = {to_fun := g.to_fun ∘ f.to_fun, map_fst := _, map_snd := _}

source

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

source

@[protected, instance]

def Bipointed.large_category :

category_theory.large_category Bipointed

Equations

Bipointed.large_category = {to_category_struct := {to_quiver := {hom := Bipointed.hom}, id := Bipointed.hom.id, comp := Bipointed.hom.comp}, id_comp' := Bipointed.large_category._proof_1, comp_id' := Bipointed.large_category._proof_2, assoc' := Bipointed.large_category._proof_3}

source

@[protected, instance]

def Bipointed.concrete_category :

category_theory.concrete_category Bipointed

Equations

Bipointed.concrete_category = category_theory.concrete_category.mk {obj := Bipointed.X, map := Bipointed.hom.to_fun, map_id' := Bipointed.concrete_category._proof_1, map_comp' := Bipointed.concrete_category._proof_2}

source

@[simp]

theorem Bipointed.swap_obj_X (X : Bipointed) :

↥(Bipointed.swap.obj X) = ↥X

source

@[simp]

theorem Bipointed.swap_obj_to_prod (X : Bipointed) :

(Bipointed.swap.obj X).to_prod = X.to_prod.swap

source

def Bipointed.swap :

Bipointed ⥤ Bipointed

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

Equations

Bipointed.swap = {obj := λ (X : Bipointed), {X := ↥X, to_prod := X.to_prod.swap}, map := λ (X Y : Bipointed) (f : X ⟶ Y), {to_fun := f.to_fun, map_fst := _, map_snd := _}, map_id' := Bipointed.swap._proof_1, map_comp' := Bipointed.swap._proof_2}

source

@[simp]

theorem Bipointed.swap_map_to_fun (X Y : Bipointed) (f : X ⟶ Y) (ᾰ : ↥X) :

(Bipointed.swap.map f).to_fun ᾰ = f.to_fun ᾰ

source

@[simp]

theorem Bipointed.swap_equiv_functor_obj_X (X : Bipointed) :

↥(Bipointed.swap_equiv.functor.obj X) = ↥X

source

@[simp]

theorem Bipointed.swap_equiv_unit_iso_inv_app_to_fun (X : Bipointed) (ᾰ : ↥((Bipointed.swap ⋙ Bipointed.swap).obj X)) :

(Bipointed.swap_equiv.unit_iso.inv.app X).to_fun ᾰ = (Bipointed.swap.map (Bipointed.swap.map {to_fun := id ↥X, map_fst := _, map_snd := _}) ≫ Bipointed.swap.map {to_fun := id ↥X, map_fst := _, map_snd := _} ≫ {to_fun := id ↥X, map_fst := _, map_snd := _}).to_fun ((𝟙 (Bipointed.swap.obj (Bipointed.swap.obj X))).to_fun ᾰ)

source

@[simp]

theorem Bipointed.swap_equiv_inverse_obj_to_prod (X : Bipointed) :

(Bipointed.swap_equiv.inverse.obj X).to_prod = X.to_prod.swap

source

@[simp]

theorem Bipointed.swap_equiv_unit_iso_hom_app_to_fun (X : Bipointed) (ᾰ : ↥((𝟭 Bipointed).obj X)) :

(Bipointed.swap_equiv.unit_iso.hom.app X).to_fun ᾰ = (𝟙 (Bipointed.swap.obj (Bipointed.swap.obj X))).to_fun (({to_fun := id ↥X, map_fst := _, map_snd := _} ≫ Bipointed.swap.map {to_fun := id ↥(Bipointed.swap.obj X), map_fst := _, map_snd := _} ≫ Bipointed.swap.map (Bipointed.swap.map {to_fun := id ↥X, map_fst := _, map_snd := _})).to_fun ᾰ)

source

def Bipointed.swap_equiv :

Bipointed ≌ Bipointed

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

Equations

Bipointed.swap_equiv = category_theory.equivalence.mk Bipointed.swap Bipointed.swap (category_theory.nat_iso.of_components (λ (X : Bipointed), {hom := {to_fun := id ↥((𝟭 Bipointed).obj X), map_fst := _, map_snd := _}, inv := {to_fun := id ↥((Bipointed.swap ⋙ Bipointed.swap).obj X), map_fst := _, map_snd := _}, hom_inv_id' := _, inv_hom_id' := _}) Bipointed.swap_equiv._proof_7) (category_theory.nat_iso.of_components (λ (X : Bipointed), {hom := {to_fun := id ↥((Bipointed.swap ⋙ Bipointed.swap).obj X), map_fst := _, map_snd := _}, inv := {to_fun := id ↥((𝟭 Bipointed).obj X), map_fst := _, map_snd := _}, hom_inv_id' := _, inv_hom_id' := _}) Bipointed.swap_equiv._proof_14)

source

@[simp]

theorem Bipointed.swap_equiv_counit_iso_hom_app_to_fun (X : Bipointed) (a : ↥((Bipointed.swap ⋙ Bipointed.swap).obj X)) :

(Bipointed.swap_equiv.counit_iso.hom.app X).to_fun a = a

source

@[simp]

theorem Bipointed.swap_equiv_inverse_obj_X (X : Bipointed) :

↥(Bipointed.swap_equiv.inverse.obj X) = ↥X

source

@[simp]

theorem Bipointed.swap_equiv_functor_obj_to_prod (X : Bipointed) :

(Bipointed.swap_equiv.functor.obj X).to_prod = X.to_prod.swap

source

@[simp]

theorem Bipointed.swap_equiv_counit_iso_inv_app_to_fun (X : Bipointed) (a : ↥((𝟭 Bipointed).obj X)) :

(Bipointed.swap_equiv.counit_iso.inv.app X).to_fun a = a

source

@[simp]

theorem Bipointed.swap_equiv_functor_map_to_fun (X Y : Bipointed) (f : X ⟶ Y) (ᾰ : ↥X) :

(Bipointed.swap_equiv.functor.map f).to_fun ᾰ = f.to_fun ᾰ

source

@[simp]

theorem Bipointed.swap_equiv_inverse_map_to_fun (X Y : Bipointed) (f : X ⟶ Y) (ᾰ : ↥X) :

(Bipointed.swap_equiv.inverse.map f).to_fun ᾰ = f.to_fun ᾰ

source

@[simp]

theorem Bipointed.swap_equiv_symm :

Bipointed.swap_equiv.symm = Bipointed.swap_equiv

source

def Bipointed_to_Pointed_fst :

Bipointed ⥤ Pointed

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

Equations

Bipointed_to_Pointed_fst = {obj := λ (X : Bipointed), {X := ↥X, point := X.to_prod.fst}, map := λ (X Y : Bipointed) (f : X ⟶ Y), {to_fun := f.to_fun, map_point := _}, map_id' := Bipointed_to_Pointed_fst._proof_1, map_comp' := Bipointed_to_Pointed_fst._proof_2}

source

def Bipointed_to_Pointed_snd :

Bipointed ⥤ Pointed

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

Equations

Bipointed_to_Pointed_snd = {obj := λ (X : Bipointed), {X := ↥X, point := X.to_prod.snd}, map := λ (X Y : Bipointed) (f : X ⟶ Y), {to_fun := f.to_fun, map_point := _}, map_id' := Bipointed_to_Pointed_snd._proof_1, map_comp' := Bipointed_to_Pointed_snd._proof_2}

source

@[simp]

theorem Bipointed_to_Pointed_fst_comp_forget :

Bipointed_to_Pointed_fst ⋙ category_theory.forget Pointed = category_theory.forget Bipointed

source

@[simp]

theorem Bipointed_to_Pointed_snd_comp_forget :

Bipointed_to_Pointed_snd ⋙ category_theory.forget Pointed = category_theory.forget Bipointed

source

@[simp]

theorem swap_comp_Bipointed_to_Pointed_fst :

Bipointed.swap ⋙ Bipointed_to_Pointed_fst = Bipointed_to_Pointed_snd

source

@[simp]

theorem swap_comp_Bipointed_to_Pointed_snd :

Bipointed.swap ⋙ Bipointed_to_Pointed_snd = Bipointed_to_Pointed_fst

source

def Pointed_to_Bipointed :

Pointed ⥤ Bipointed

The functor from Pointed to Bipointed which bipoints the point.

Equations

Pointed_to_Bipointed = {obj := λ (X : Pointed), {X := ↥X, to_prod := (X.point, X.point)}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Bipointed._proof_1, map_comp' := Pointed_to_Bipointed._proof_2}

source

def Pointed_to_Bipointed_fst :

Pointed ⥤ Bipointed

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

Equations

Pointed_to_Bipointed_fst = {obj := λ (X : Pointed), {X := option ↥X, to_prod := (↑(X.point), none ↥X)}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Bipointed_fst._proof_3, map_comp' := Pointed_to_Bipointed_fst._proof_4}

source

def Pointed_to_Bipointed_snd :

Pointed ⥤ Bipointed

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

Equations

Pointed_to_Bipointed_snd = {obj := λ (X : Pointed), {X := option ↥X, to_prod := (none ↥X, ↑(X.point))}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Bipointed_snd._proof_3, map_comp' := Pointed_to_Bipointed_snd._proof_4}

source

@[simp]

theorem Pointed_to_Bipointed_fst_comp_swap :

Pointed_to_Bipointed_fst ⋙ Bipointed.swap = Pointed_to_Bipointed_snd

source

@[simp]

theorem Pointed_to_Bipointed_snd_comp_swap :

Pointed_to_Bipointed_snd ⋙ Bipointed.swap = Pointed_to_Bipointed_fst

source

def Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst :

Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_fst ≅ 𝟭 Pointed

Bipointed_to_Pointed_fst is inverse to Pointed_to_Bipointed.

Equations

Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst = category_theory.nat_iso.of_components (λ (X : Pointed), {hom := {to_fun := id ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_fst).obj X), map_point := _}, inv := {to_fun := id ↥((𝟭 Pointed).obj X), map_point := _}, hom_inv_id' := _, inv_hom_id' := _}) Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst._proof_5

source

@[simp]

theorem Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst_hom_app_to_fun (X : Pointed) (a : ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_fst).obj X)) :

(Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst.hom.app X).to_fun a = a

source

@[simp]

theorem Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst_inv_app_to_fun (X : Pointed) (a : ↥((𝟭 Pointed).obj X)) :

(Pointed_to_Bipointed_comp_Bipointed_to_Pointed_fst.inv.app X).to_fun a = a

source

def Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd :

Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_snd ≅ 𝟭 Pointed

Bipointed_to_Pointed_snd is inverse to Pointed_to_Bipointed.

Equations

Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd = category_theory.nat_iso.of_components (λ (X : Pointed), {hom := {to_fun := id ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_snd).obj X), map_point := _}, inv := {to_fun := id ↥((𝟭 Pointed).obj X), map_point := _}, hom_inv_id' := _, inv_hom_id' := _}) Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd._proof_5

source

@[simp]

theorem Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd_inv_app_to_fun (X : Pointed) (a : ↥((𝟭 Pointed).obj X)) :

(Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd.inv.app X).to_fun a = a

source

@[simp]

theorem Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd_hom_app_to_fun (X : Pointed) (a : ↥((Pointed_to_Bipointed ⋙ Bipointed_to_Pointed_snd).obj X)) :

(Pointed_to_Bipointed_comp_Bipointed_to_Pointed_snd.hom.app X).to_fun a = a

source

def Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction :

Pointed_to_Bipointed_fst ⊣ Bipointed_to_Pointed_fst

The free/forgetful adjunction between Pointed_to_Bipointed_fst and Bipointed_to_Pointed_fst.

Equations

Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Pointed) (Y : Bipointed), {to_fun := λ (f : Pointed_to_Bipointed_fst.obj X ⟶ Y), {to_fun := f.to_fun ∘ some, map_point := _}, inv_fun := λ (f : X ⟶ Bipointed_to_Pointed_fst.obj Y), {to_fun := λ (o : ↥(Pointed_to_Bipointed_fst.obj X)), option.elim o Y.to_prod.snd f.to_fun, map_fst := _, map_snd := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction._proof_6, hom_equiv_naturality_right' := Pointed_to_Bipointed_fst_Bipointed_to_Pointed_fst_adjunction._proof_7}

source

def Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction :

Pointed_to_Bipointed_snd ⊣ Bipointed_to_Pointed_snd

The free/forgetful adjunction between Pointed_to_Bipointed_snd and Bipointed_to_Pointed_snd.

Equations

Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Pointed) (Y : Bipointed), {to_fun := λ (f : Pointed_to_Bipointed_snd.obj X ⟶ Y), {to_fun := f.to_fun ∘ some, map_point := _}, inv_fun := λ (f : X ⟶ Bipointed_to_Pointed_snd.obj Y), {to_fun := λ (o : ↥(Pointed_to_Bipointed_snd.obj X)), option.elim o Y.to_prod.fst f.to_fun, map_fst := _, map_snd := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction._proof_6, hom_equiv_naturality_right' := Pointed_to_Bipointed_snd_Bipointed_to_Pointed_snd_adjunction._proof_7}

mathlib documentation

The category of bipointed types #

TODO #