mathlib3 documentation

category_theory.limits.bicones

Bicones #

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

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] :

decidable_eq (category_theory.bicone J)

inductive category_theory.bicone (J : Type u₁) :

Type u₁

left : Π {J : Type u₁}, category_theory.bicone J
right : Π {J : Type u₁}, category_theory.bicone J
diagram : Π {J : Type u₁}, J → category_theory.bicone J

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₁) :

inhabited (category_theory.bicone J)

Equations

category_theory.bicone.inhabited J = {default := category_theory.bicone.left J}

@[protected, instance]

noncomputable def category_theory.fin_bicone (J : Type u₁) [fintype J] :

fintype (category_theory.bicone J)

Equations

category_theory.fin_bicone J = {elems := [category_theory.bicone.left, category_theory.bicone.right].to_finset ∪ finset.image category_theory.bicone.diagram (fintype.elems J), complete := _}

inductive category_theory.bicone_hom (J : Type u₁) [category_theory.category J] :

category_theory.bicone J → category_theory.bicone J → Type (max u₁ v₁)

left_id : Π {J : Type u₁} [_inst_1 : category_theory.category J], category_theory.bicone_hom J category_theory.bicone.left category_theory.bicone.left
right_id : Π {J : Type u₁} [_inst_1 : category_theory.category J], category_theory.bicone_hom J category_theory.bicone.right category_theory.bicone.right
left : Π {J : Type u₁} [_inst_1 : category_theory.category J] (j : J), category_theory.bicone_hom J category_theory.bicone.left (category_theory.bicone.diagram j)
right : Π {J : Type u₁} [_inst_1 : category_theory.category J] (j : J), category_theory.bicone_hom J category_theory.bicone.right (category_theory.bicone.diagram j)
diagram : Π {J : Type u₁} [_inst_1 : category_theory.category J] {j k : J}, (j ⟶ k) → category_theory.bicone_hom J (category_theory.bicone.diagram j) (category_theory.bicone.diagram k)

The homs for a walking bicone J.

Instances for category_theory.bicone_hom

category_theory.bicone_hom.has_sizeof_inst
category_theory.bicone_hom.inhabited

@[protected, instance]

def category_theory.bicone_hom.inhabited (J : Type u₁) [category_theory.category J] :

inhabited (category_theory.bicone_hom J category_theory.bicone.left category_theory.bicone.left)

Equations

category_theory.bicone_hom.inhabited J = {default := category_theory.bicone_hom.left_id _inst_1}

@[protected, instance]

noncomputable def category_theory.bicone_hom.decidable_eq (J : Type u₁) [category_theory.category J] {j k : category_theory.bicone J} :

decidable_eq (category_theory.bicone_hom J j k)

Equations

category_theory.bicone_hom.decidable_eq J = λ (f g : category_theory.bicone_hom J j k), f.cases_on (λ (H_1 : j = category_theory.bicone.left), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.left k) (H_2 : k = category_theory.bicone.left), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.left category_theory.bicone.left) (H_3 : f == category_theory.bicone_hom.left_id), eq.rec (g.cases_on (λ (H_1 H_2 : category_theory.bicone.left = category_theory.bicone.left) (H_3 : g == category_theory.bicone_hom.left_id), eq.rec (_.mpr decidable.true) _) (λ (H_1 : category_theory.bicone.left = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.left = category_theory.bicone.left) (H_2 : category_theory.bicone.left = category_theory.bicone.diagram g_1), category_theory.bicone.no_confusion H_2) (λ (g_1 : J) (H_1 : category_theory.bicone.left = 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.left = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (H_1 : j = category_theory.bicone.right), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.right k) (H_2 : k = category_theory.bicone.right), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.right category_theory.bicone.right) (H_3 : f == category_theory.bicone_hom.right_id), eq.rec (g.cases_on (λ (H_1 : category_theory.bicone.right = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 H_2 : category_theory.bicone.right = category_theory.bicone.right) (H_3 : g == category_theory.bicone_hom.right_id), eq.rec (_.mpr decidable.true) _) (λ (g_1 : J) (H_1 : category_theory.bicone.right = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.right = category_theory.bicone.right) (H_2 : category_theory.bicone.right = category_theory.bicone.diagram g_1), category_theory.bicone.no_confusion H_2) (λ {g_j g_k : J} (g_f : g_j ⟶ g_k) (H_1 : category_theory.bicone.right = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (f_1 : J) (H_1 : j = category_theory.bicone.left), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.left k) (H_2 : k = category_theory.bicone.diagram f_1), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.left (category_theory.bicone.diagram f_1)) (H_3 : f == category_theory.bicone_hom.left f_1), eq.rec (g.cases_on (λ (H_1 : category_theory.bicone.left = category_theory.bicone.left) (H_2 : category_theory.bicone.diagram f_1 = category_theory.bicone.left), category_theory.bicone.no_confusion H_2) (λ (H_1 : category_theory.bicone.left = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.left = category_theory.bicone.left) (H_2 : category_theory.bicone.diagram f_1 = category_theory.bicone.diagram g_1), category_theory.bicone.no_confusion H_2 (λ (val_eq : f_1 = g_1), eq.rec (λ (H_3 : g == category_theory.bicone_hom.left f_1), eq.rec (_.mpr decidable.true) _) val_eq)) (λ (g_1 : J) (H_1 : category_theory.bicone.left = 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.left = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ (f_1 : J) (H_1 : j = category_theory.bicone.right), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.right k) (H_2 : k = category_theory.bicone.diagram f_1), eq.rec (λ (f g : category_theory.bicone_hom J category_theory.bicone.right (category_theory.bicone.diagram f_1)) (H_3 : f == category_theory.bicone_hom.right f_1), eq.rec (g.cases_on (λ (H_1 : category_theory.bicone.right = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 : category_theory.bicone.right = category_theory.bicone.right) (H_2 : category_theory.bicone.diagram f_1 = category_theory.bicone.right), category_theory.bicone.no_confusion H_2) (λ (g_1 : J) (H_1 : category_theory.bicone.right = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.right = category_theory.bicone.right) (H_2 : category_theory.bicone.diagram f_1 = category_theory.bicone.diagram g_1), category_theory.bicone.no_confusion H_2 (λ (val_eq : f_1 = g_1), eq.rec (λ (H_3 : g == category_theory.bicone_hom.right f_1), eq.rec (_.mpr decidable.true) _) val_eq)) (λ {g_j g_k : J} (g_f : g_j ⟶ g_k) (H_1 : category_theory.bicone.right = category_theory.bicone.diagram g_j), category_theory.bicone.no_confusion H_1) _ _ _) _) _ f g) _ f g) (λ {f_j f_k : J} (f_f : f_j ⟶ f_k) (H_1 : j = category_theory.bicone.diagram f_j), eq.rec (λ (f g : category_theory.bicone_hom J (category_theory.bicone.diagram f_j) k) (H_2 : k = category_theory.bicone.diagram f_k), eq.rec (λ (f g : category_theory.bicone_hom J (category_theory.bicone.diagram f_j) (category_theory.bicone.diagram f_k)) (H_3 : f == category_theory.bicone_hom.diagram f_f), eq.rec (g.cases_on (λ (H_1 : category_theory.bicone.diagram f_j = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (H_1 : category_theory.bicone.diagram f_j = category_theory.bicone.right), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_j = category_theory.bicone.left), category_theory.bicone.no_confusion H_1) (λ (g_1 : J) (H_1 : category_theory.bicone.diagram f_j = 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_j = category_theory.bicone.diagram g_j), 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.diagram f_k = category_theory.bicone.diagram g_k), category_theory.bicone.no_confusion H_2 (λ (val_eq : f_k = g_k), eq.rec (λ (g_f : f_j ⟶ f_k) (H_3 : g == category_theory.bicone_hom.diagram g_f), 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₁) [category_theory.category J] (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]

def category_theory.bicone_category_struct (J : Type u₁) [category_theory.category J] :

category_theory.category_struct (category_theory.bicone J)

Equations

category_theory.bicone_category_struct J = {to_quiver := {hom := category_theory.bicone_hom J _inst_1}, id := λ (j : category_theory.bicone J), j.cases_on category_theory.bicone_hom.left_id category_theory.bicone_hom.right_id (λ (k : J), category_theory.bicone_hom.diagram (𝟙 k)), comp := λ (X Y Z : category_theory.bicone J) (f : X ⟶ Y) (g : Y ⟶ Z), 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) _ _ _}

@[simp]

theorem category_theory.bicone_category_struct_to_quiver_hom (J : Type u₁) [category_theory.category J] (ᾰ ᾰ_1 : category_theory.bicone J) :

(ᾰ ⟶ ᾰ_1) = category_theory.bicone_hom J ᾰ ᾰ_1

@[simp]

theorem category_theory.bicone_category_struct_id (J : Type u₁) [category_theory.category J] (j : category_theory.bicone J) :

𝟙 j = j.cases_on category_theory.bicone_hom.left_id category_theory.bicone_hom.right_id (λ (k : J), category_theory.bicone_hom.diagram (𝟙 k))

@[protected, instance]

def category_theory.bicone_category (J : Type u₁) [category_theory.category J] :

category_theory.category (category_theory.bicone J)

Equations

category_theory.bicone_category J = {to_category_struct := category_theory.bicone_category_struct J _inst_1, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.bicone_mk_obj (J : Type v₁) [category_theory.small_category J] {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] {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] {C : Type u₁} [category_theory.category C] {F : J ⥤ C} (c₁ c₂ : category_theory.limits.cone F) :

category_theory.bicone J ⥤ C

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

Equations

category_theory.bicone_mk J c₁ c₂ = {obj := λ (X : category_theory.bicone J), X.cases_on c₁.X c₂.X (λ (j : J), F.obj j), map := λ (X Y : category_theory.bicone J) (f : X ⟶ Y), 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) _ _ _, map_id' := _, map_comp' := _}

@[protected, instance]

noncomputable def category_theory.fin_bicone_hom (J : Type v₁) [category_theory.small_category J] [category_theory.fin_category J] (j k : category_theory.bicone J) :

fintype (j ⟶ k)

Equations

category_theory.fin_bicone_hom J j k = j.cases_on (k.cases_on {elems := {category_theory.bicone_hom.left_id}, complete := _} {elems := ∅, complete := _} (λ (k : J), {elems := {category_theory.bicone_hom.left k}, complete := _})) (k.cases_on {elems := ∅, complete := _} {elems := {category_theory.bicone_hom.right_id}, complete := _} (λ (k : J), {elems := {category_theory.bicone_hom.right k}, complete := _})) (λ (j : J), k.cases_on {elems := ∅, complete := _} {elems := ∅, complete := _} (λ (k : J), {elems := finset.image category_theory.bicone_hom.diagram (fintype.elems (j ⟶ k)), complete := _}))

@[protected, instance]

def category_theory.bicone_small_category (J : Type v₁) [category_theory.small_category J] :

category_theory.small_category (category_theory.bicone J)

Equations

category_theory.bicone_small_category J = category_theory.bicone_category J

@[protected, instance]

noncomputable def category_theory.bicone_fin_category (J : Type v₁) [category_theory.small_category J] [category_theory.fin_category J] :

category_theory.fin_category (category_theory.bicone J)

Equations

category_theory.bicone_fin_category J = {fintype_obj := category_theory.fin_bicone J category_theory.fin_category.fintype_obj, fintype_hom := λ (j j' : category_theory.bicone J), category_theory.fin_bicone_hom J j j'}