category_theory.category.Twop

source

structure Twop :

Type (u+1)

X : Type ?
to_two_pointing : two_pointing self.X

The category of two-pointed types.

Instances for Twop

source

@[protected, instance]

def Twop.has_coe_to_sort :

has_coe_to_sort Twop (Type u_1)

Equations

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

source

def Twop.of {X : Type u_1} (to_two_pointing : two_pointing X) :

Twop

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

Equations

Twop.of to_two_pointing = {X := X, to_two_pointing := to_two_pointing}

source

@[simp]

theorem Twop.coe_of {X : Type u_1} (to_two_pointing : two_pointing X) :

↥(Twop.of to_two_pointing) = X

source

def two_pointing.Twop {X : Type u_1} (to_two_pointing : two_pointing X) :

Twop

Alias of Twop.of.

source

@[protected, instance]

def Twop.inhabited :

inhabited Twop

Equations

Twop.inhabited = {default := Twop.of two_pointing.bool}

source

def Twop.to_Bipointed (X : Twop) :

Bipointed

Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are distinct.

Equations

X.to_Bipointed = X.to_two_pointing.to_prod.Bipointed

source

@[simp]

theorem Twop.coe_to_Bipointed (X : Twop) :

↥(X.to_Bipointed) = ↥X

source

@[protected, instance]

def Twop.large_category :

category_theory.large_category Twop

Equations

Twop.large_category = category_theory.induced_category.category Twop.to_Bipointed

source

@[protected, instance]

def Twop.concrete_category :

category_theory.concrete_category Twop

Equations

Twop.concrete_category = category_theory.induced_category.concrete_category Twop.to_Bipointed

source

@[protected, instance]

def Twop.has_forget_to_Bipointed :

category_theory.has_forget₂ Twop Bipointed

Equations

Twop.has_forget_to_Bipointed = category_theory.induced_category.has_forget₂ Twop.to_Bipointed

source

def Twop.swap :

Twop ⥤ Twop

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

Equations

Twop.swap = {obj := λ (X : Twop), {X := ↥X, to_two_pointing := X.to_two_pointing.swap}, map := λ (X Y : Twop) (f : X ⟶ Y), {to_fun := f.to_fun, map_fst := _, map_snd := _}, map_id' := Twop.swap._proof_3, map_comp' := Twop.swap._proof_4}

source

@[simp]

theorem Twop.swap_obj_to_two_pointing (X : Twop) :

(Twop.swap.obj X).to_two_pointing = X.to_two_pointing.swap

source

@[simp]

theorem Twop.swap_obj_X (X : Twop) :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

def Twop.swap_equiv :

Twop ≌ Twop

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

Equations

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

source

@[simp]

theorem Twop.swap_equiv_functor_obj_to_two_pointing_to_prod (X : Twop) :

(Twop.swap_equiv.functor.obj X).to_two_pointing.to_prod = (X.to_two_pointing.to_prod.snd, X.to_two_pointing.to_prod.fst)

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem Twop.swap_equiv_counit_iso_inv_app_to_fun (X : Twop) (a : ↥(((𝟭 Twop).obj X).to_Bipointed)) :

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

source

@[simp]

theorem Twop.swap_equiv_inverse_obj_X (X : Twop) :

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

source

@[simp]

theorem Twop.swap_equiv_unit_iso_hom_app_to_fun (X : Twop) (ᾰ : ↥(((𝟭 Twop).obj X).to_Bipointed)) :

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

source

@[simp]

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

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

source

@[simp]

theorem Twop.swap_equiv_functor_obj_X (X : Twop) :

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

source

@[simp]

theorem Twop.swap_equiv_inverse_obj_to_two_pointing_to_prod (X : Twop) :

(Twop.swap_equiv.inverse.obj X).to_two_pointing.to_prod = (X.to_two_pointing.to_prod.snd, X.to_two_pointing.to_prod.fst)

source

@[simp]

theorem Twop.swap_equiv_symm :

Twop.swap_equiv.symm = Twop.swap_equiv

source

@[simp]

theorem Twop_swap_comp_forget_to_Bipointed :

Twop.swap ⋙ category_theory.forget₂ Twop Bipointed = category_theory.forget₂ Twop Bipointed ⋙ Bipointed.swap

source

def Pointed_to_Twop_fst :

Pointed ⥤ Twop

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

Equations

Pointed_to_Twop_fst = {obj := λ (X : Pointed), {X := option ↥X, to_two_pointing := {to_prod := (↑(X.point), option.none ↥X), fst_ne_snd := _}}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Twop_fst._proof_6, map_comp' := Pointed_to_Twop_fst._proof_7}

source

@[simp]

theorem Pointed_to_Twop_fst_obj_to_two_pointing_to_prod (X : Pointed) :

(Pointed_to_Twop_fst.obj X).to_two_pointing.to_prod = (↑(X.point), option.none ↥X)

source

@[simp]

theorem Pointed_to_Twop_fst_obj_X (X : Pointed) :

↥(Pointed_to_Twop_fst.obj X) = option ↥X

source

@[simp]

theorem Pointed_to_Twop_fst_map_to_fun (X Y : Pointed) (f : X ⟶ Y) (o : option ↥X) :

(Pointed_to_Twop_fst.map f).to_fun o = option.map f.to_fun o

source

@[simp]

theorem Pointed_to_Twop_snd_map_to_fun (X Y : Pointed) (f : X ⟶ Y) (o : option ↥X) :

(Pointed_to_Twop_snd.map f).to_fun o = option.map f.to_fun o

source

@[simp]

theorem Pointed_to_Twop_snd_obj_to_two_pointing_to_prod (X : Pointed) :

(Pointed_to_Twop_snd.obj X).to_two_pointing.to_prod = (option.none ↥X, ↑(X.point))

source

@[simp]

theorem Pointed_to_Twop_snd_obj_X (X : Pointed) :

↥(Pointed_to_Twop_snd.obj X) = option ↥X

source

def Pointed_to_Twop_snd :

Pointed ⥤ Twop

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

Equations

Pointed_to_Twop_snd = {obj := λ (X : Pointed), {X := option ↥X, to_two_pointing := {to_prod := (option.none ↥X, ↑(X.point)), fst_ne_snd := _}}, map := λ (X Y : Pointed) (f : X ⟶ Y), {to_fun := option.map f.to_fun, map_fst := _, map_snd := _}, map_id' := Pointed_to_Twop_snd._proof_6, map_comp' := Pointed_to_Twop_snd._proof_7}

source

@[simp]

theorem Pointed_to_Twop_fst_comp_swap :

Pointed_to_Twop_fst ⋙ Twop.swap = Pointed_to_Twop_snd

source

@[simp]

theorem Pointed_to_Twop_snd_comp_swap :

Pointed_to_Twop_snd ⋙ Twop.swap = Pointed_to_Twop_fst

source

@[simp]

theorem Pointed_to_Twop_fst_comp_forget_to_Bipointed :

Pointed_to_Twop_fst ⋙ category_theory.forget₂ Twop Bipointed = Pointed_to_Bipointed_fst

source

@[simp]

theorem Pointed_to_Twop_snd_comp_forget_to_Bipointed :

Pointed_to_Twop_snd ⋙ category_theory.forget₂ Twop Bipointed = Pointed_to_Bipointed_snd

source

def Pointed_to_Twop_fst_forget_comp_Bipointed_to_Pointed_fst_adjunction :

Pointed_to_Twop_fst ⊣ category_theory.forget₂ Twop Bipointed ⋙ Bipointed_to_Pointed_fst

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

Equations

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

source

def Pointed_to_Twop_snd_forget_comp_Bipointed_to_Pointed_snd_adjunction :

Pointed_to_Twop_snd ⊣ category_theory.forget₂ Twop Bipointed ⋙ Bipointed_to_Pointed_snd

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

Equations

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

mathlib3 documentation

The category of two-pointed types #

References #