mathlib documentation

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]
inductive category_theory.bicone (J : Type u₁) :
Type u₁

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

inductive category_theory.bicone_hom (J : Type u₁) [category_theory.category J] [Π (j k : J), decidable_eq (j k)] :
category_theory.bicone Jcategory_theory.bicone JType (max u₁ v₁)

The homs for a walking bicone J.

@[protected, instance]
Equations
@[simp]
theorem category_theory.bicone_category_struct_comp (J : Type u₁) [category_theory.category J] [Π (j k : J), decidable_eq (j k)] (X Y Z : category_theory.bicone J) (f : X Y) (g : Y Z) :
f g = category_theory.bicone_hom.cases_on f (λ (H_1 : X = category_theory.bicone.left), eq.rec (λ (f : category_theory.bicone.left Y) (H_2 : Y = category_theory.bicone.left), eq.rec (λ (g : category_theory.bicone.left Z) (f : category_theory.bicone.left category_theory.bicone.left) (H_3 : f == category_theory.bicone_hom.left_id), eq.rec g _) _ g f) _ f) (λ (H_1 : X = category_theory.bicone.right), eq.rec (λ (f : category_theory.bicone.right Y) (H_2 : Y = category_theory.bicone.right), eq.rec (λ (g : category_theory.bicone.right Z) (f : category_theory.bicone.right category_theory.bicone.right) (H_3 : f == category_theory.bicone_hom.right_id), eq.rec g _) _ g f) _ f) (λ (f_1 : J) (H_1 : X = category_theory.bicone.left), eq.rec (λ (f : category_theory.bicone.left Y) (H_2 : Y = category_theory.bicone.diagram f_1), eq.rec (λ (g : category_theory.bicone.diagram f_1 Z) (f : category_theory.bicone.left category_theory.bicone.diagram f_1) (H_3 : f == category_theory.bicone_hom.left f_1), eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : Z = category_theory.bicone.diagram g_k), eq.rec (λ (g : category_theory.bicone.diagram f_1 category_theory.bicone.diagram g_k) (H_3 : g == category_theory.bicone_hom.diagram g_f), eq.rec (category_theory.bicone_hom.left g_k) _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ (f_1 : J) (H_1 : X = category_theory.bicone.right), eq.rec (λ (f : category_theory.bicone.right Y) (H_2 : Y = category_theory.bicone.diagram f_1), eq.rec (λ (g : category_theory.bicone.diagram f_1 Z) (f : category_theory.bicone.right category_theory.bicone.diagram f_1) (H_3 : f == category_theory.bicone_hom.right f_1), eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : category_theory.bicone.diagram f_1 = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1 (λ (val_eq : f_1 = g_j), eq.rec (λ (g_f : f_1 g_k) (H_2 : Z = category_theory.bicone.diagram g_k), eq.rec (λ (g : category_theory.bicone.diagram f_1 category_theory.bicone.diagram g_k) (H_3 : g == category_theory.bicone_hom.diagram g_f), eq.rec (category_theory.bicone_hom.right g_k) _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : X = category_theory.bicone.diagram f_j), eq.rec (λ (f : category_theory.bicone.diagram f_j Y) (H_2 : Y = category_theory.bicone.diagram f_k), eq.rec (λ (g : category_theory.bicone.diagram f_k Z) (f : category_theory.bicone.diagram f_j category_theory.bicone.diagram f_k) (H_3 : f == category_theory.bicone_hom.diagram f_f), eq.rec (category_theory.bicone_hom.cases_on g (λ (H_1 : category_theory.bicone.diagram f_k = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 : category_theory.bicone.diagram f_k = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_k = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_k = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ {g_j g_k : J} (g_f : g_j g_k) (H_1 : category_theory.bicone.diagram f_k = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1 (λ (val_eq : f_k = g_j), eq.rec (λ (g_f : f_k g_k) (H_2 : Z = category_theory.bicone.diagram g_k), eq.rec (λ (g : category_theory.bicone.diagram f_k category_theory.bicone.diagram g_k) (H_3 : g == category_theory.bicone_hom.diagram g_f), eq.rec (category_theory.bicone_hom.diagram (f_f g_f)) _) _ g) val_eq g_f)) _ _ _) _) _ g f) _ f) _ _ _
@[protected, instance]
Equations
@[simp]
theorem category_theory.bicone_category_struct_to_quiver_hom (J : Type u₁) [category_theory.category J] [Π (j k : J), decidable_eq (j k)] (ᾰ ᾰ_1 : category_theory.bicone J) :
(ᾰ ᾰ_1) = category_theory.bicone_hom J ᾰ_1
@[protected, instance]
Equations
@[simp]
theorem category_theory.bicone_mk_obj (J : Type v₁) [category_theory.small_category J] [Π (j k : J), decidable_eq (j k)] {C : Type u₁} [category_theory.category C] {F : J C} (c₁ c₂ : category_theory.limits.cone F) (X : category_theory.bicone J) :
(category_theory.bicone_mk J c₁ 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₁) [category_theory.small_category J] [Π (j k : J), decidable_eq (j k)] {C : Type u₁} [category_theory.category C] {F : J C} (c₁ c₂ : category_theory.limits.cone F) (X Y : category_theory.bicone J) (f : X Y) :
(category_theory.bicone_mk J c₁ c₂).map f = category_theory.bicone_hom.cases_on f (λ (H_1 : X = category_theory.bicone.left), eq.rec (λ (f : category_theory.bicone.left Y) (H_2 : Y = category_theory.bicone.left), eq.rec (λ (f : category_theory.bicone.left category_theory.bicone.left) (H_3 : f == category_theory.bicone_hom.left_id), eq.rec (𝟙 (category_theory.bicone.left.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (H_1 : X = category_theory.bicone.right), eq.rec (λ (f : category_theory.bicone.right Y) (H_2 : Y = category_theory.bicone.right), eq.rec (λ (f : category_theory.bicone.right category_theory.bicone.right) (H_3 : f == category_theory.bicone_hom.right_id), eq.rec (𝟙 (category_theory.bicone.right.cases_on c₁.X c₂.X (λ (j : J), F.obj j))) _) _ f) _ f) (λ (f_1 : J) (H_1 : X = category_theory.bicone.left), eq.rec (λ (f : category_theory.bicone.left Y) (H_2 : Y = category_theory.bicone.diagram f_1), eq.rec (λ (f : category_theory.bicone.left category_theory.bicone.diagram f_1) (H_3 : f == category_theory.bicone_hom.left f_1), eq.rec (c₁.π.app f_1) _) _ f) _ f) (λ (f_1 : J) (H_1 : X = category_theory.bicone.right), eq.rec (λ (f : category_theory.bicone.right Y) (H_2 : Y = category_theory.bicone.diagram f_1), eq.rec (λ (f : category_theory.bicone.right category_theory.bicone.diagram f_1) (H_3 : f == category_theory.bicone_hom.right f_1), eq.rec (c₂.π.app f_1) _) _ f) _ f) (λ {f_j f_k : J} (f_f : f_j f_k) (H_1 : X = category_theory.bicone.diagram f_j), eq.rec (λ (f : category_theory.bicone.diagram f_j Y) (H_2 : Y = category_theory.bicone.diagram f_k), eq.rec (λ (f : category_theory.bicone.diagram f_j category_theory.bicone.diagram f_k) (H_3 : f == category_theory.bicone_hom.diagram f_f), eq.rec (F.map f_f) _) _ f) _ f) _ _ _
def category_theory.bicone_mk (J : Type v₁) [category_theory.small_category J] [Π (j k : J), decidable_eq (j k)] {C : Type u₁} [category_theory.category C] {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
@[protected, instance]
Equations