# mathlibdocumentation

category_theory.limits.bicones

# Bicones #

Given a category J, a walking bicone J is a category whose objects are the objects of J and two extra vertices bicone.left and bicone.right. The morphisms are the morphisms of J and left ⟶ j, right ⟶ j for each j : J such that ⬝ ⟶ j and ⬝ ⟶ k commutes with each f : j ⟶ k.

Given a diagram F : J ⥤ C and two cone Fs, we can join them into a diagram bicone J ⥤ C via bicone_mk.

This is used in category_theory.flat_functors.preserves_finite_limits_of_flat.

@[protected, instance]
def category_theory.bicone.decidable_eq (J : Type u₁) [a : decidable_eq J] :
inductive category_theory.bicone (J : Type u₁) :
Type u₁
• left : Π {J : Type u₁},
• right : Π {J : Type u₁},
• diagram : Π {J : Type u₁},

Given a category J, construct a walking bicone J by adjoining two elements.

Instances for category_theory.bicone
@[protected, instance]
def category_theory.bicone.inhabited (J : Type u₁) :
Equations
@[protected, instance]
noncomputable def category_theory.fin_bicone (J : Type u₁) [fintype J] :
Equations
inductive category_theory.bicone_hom (J : Type u₁)  :
Type (max u₁ v₁)
• left_id : Π {J : Type u₁} [_inst_1 : ,
• right_id : Π {J : Type u₁} [_inst_1 : ,
• left : Π {J : Type u₁} [_inst_1 : (j : J),
• right : Π {J : Type u₁} [_inst_1 : (j : J),
• diagram : Π {J : Type u₁} [_inst_1 : {j k : J},

The homs for a walking bicone J.

Instances for category_theory.bicone_hom
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.bicone_hom.decidable_eq (J : Type u₁) {j k : category_theory.bicone J} :
Equations
• = λ (f g : , f.cases_on (λ (H_1 : , eq.rec (λ (f g : (H_2 : , eq.rec (λ (f g : (H_3 : , eq.rec (g.cases_on (λ (H_1 H_2 : (H_3 : , eq.rec _) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (H_1 : , eq.rec (λ (f g : (H_2 : , eq.rec (λ (f g : (H_3 : , eq.rec (g.cases_on (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 H_2 : (H_3 : , eq.rec _) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (f_1 : J) (H_1 : , eq.rec (λ (f g : (H_2 : , eq.rec (λ (f g : (H_3 : , eq.rec (g.cases_on (λ (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2 (λ (val_eq : f_1 = g_1), eq.rec (λ (H_3 : , eq.rec _) val_eq)) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (f_1 : J) (H_1 : , eq.rec (λ (f g : (H_2 : , eq.rec (λ (f g : (H_3 : , eq.rec (g.cases_on (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : (H_2 : , category_theory.bicone.no_confusion H_2 (λ (val_eq : f_1 = g_1), eq.rec (λ (H_3 : , eq.rec _) val_eq)) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : , eq.rec (λ (f g : (H_2 : , eq.rec (λ (f g : (H_3 : , eq.rec (g.cases_on (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_j = g_j), eq.rec (λ (g_f : f_j g_k) (H_2 : , category_theory.bicone.no_confusion H_2 (λ (val_eq : f_k = g_k), eq.rec (λ (g_f : f_j f_k) (H_3 : , eq.rec (_.mpr (classical.prop_decidable (f_f = g_f))) _) val_eq g_f)) val_eq g_f)) _ _ _) _) _ f g) _ f g) _ _ _
@[simp]
theorem category_theory.bicone_category_struct_comp (J : Type u₁) (X Y Z : category_theory.bicone J) (f : X Y) (g : Y Z) :
f g = category_theory.bicone_hom.cases_on f (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec g _) _ g f) _ f) (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec g _) _ g f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_k = g_j), eq.rec (λ (g_f : f_k g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec (category_theory.bicone_hom.diagram (f_f g_f)) _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) _ _ _
@[protected, instance]
Equations
• = {to_quiver := {hom := _inst_1}, id := λ (j : , (λ (k : J), , comp := λ (X Y Z : (f : X Y) (g : Y Z), category_theory.bicone_hom.cases_on f (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec g _) _ g f) _ f) (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec g _) _ g f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (g : (f : (H_3 : , eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : , category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : , category_theory.bicone.no_confusion H_1 (λ (val_eq : f_k = g_j), eq.rec (λ (g_f : f_k g_k) (H_2 : , eq.rec (λ (g : (H_3 : , eq.rec (category_theory.bicone_hom.diagram (f_f g_f)) _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) _ _ _}
@[simp]
theorem category_theory.bicone_category_struct_to_quiver_hom (J : Type u₁) (ᾰ ᾰ_1 : category_theory.bicone J) :
(ᾰ ᾰ_1) = ᾰ_1
@[simp]
theorem category_theory.bicone_category_struct_id (J : Type u₁) (j : category_theory.bicone J) :
𝟙 j = (λ (k : J),
@[protected, instance]
def category_theory.bicone_category (J : Type u₁)  :
Equations
@[simp]
theorem category_theory.bicone_mk_obj (J : Type v₁) {C : Type u₁} {F : J C} (c₁ c₂ : category_theory.limits.cone F) (X : category_theory.bicone J) :
c₂).obj X = X.cases_on c₁.X c₂.X (λ (j : J), F.obj j)
@[simp]
theorem category_theory.bicone_mk_map (J : Type v₁) {C : Type u₁} {F : J C} (c₁ c₂ : category_theory.limits.cone F) (X Y : category_theory.bicone J) (f : X Y) :
c₂).map f = category_theory.bicone_hom.cases_on f (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (𝟙 (category_theory.bicone.left.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (𝟙 (category_theory.bicone.right.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (c₁.π.app f_1) _) _ f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (c₂.π.app f_1) _) _ f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (F.map f_f) _) _ f) _ f) _ _ _
def category_theory.bicone_mk (J : Type v₁) {C : Type u₁} {F : J C} (c₁ c₂ : category_theory.limits.cone F) :

Given a diagram F : J ⥤ C and two cone Fs, we can join them into a diagram bicone J ⥤ C.

Equations
• c₂ = {obj := λ (X : , X.cases_on c₁.X c₂.X (λ (j : J), F.obj j), map := λ (X Y : (f : X Y), category_theory.bicone_hom.cases_on f (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (𝟙 (category_theory.bicone.left.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (𝟙 (category_theory.bicone.right.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (c₁.π.app f_1) _) _ f) _ f) (λ (f_1 : J) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (c₂.π.app f_1) _) _ f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : , eq.rec (λ (f : (H_2 : , eq.rec (λ (f : (H_3 : , eq.rec (F.map f_f) _) _ f) _ f) _ _ _, map_id' := _, map_comp' := _}
@[protected, instance]
noncomputable def category_theory.fin_bicone_hom (J : Type v₁) (j k : category_theory.bicone J) :
fintype (j k)
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.bicone_fin_category (J : Type v₁)  :
Equations