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 biconeMk.

This is used in CategoryTheory.Functor.Flat.

inductive CategoryTheory.Bicone (J : Type u₁) : Type u₁

• left: {J : Type u₁} → CategoryTheory.Bicone J
• right: {J : Type u₁} → CategoryTheory.Bicone J
• diagram: {J : Type u₁} → J → CategoryTheory.Bicone J

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

instance CategoryTheory.instDecidableEqBicone : {J : Type u_1} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Bicone J)

instance CategoryTheory.instInhabitedBicone (J : Type u₁) : Inhabited (CategoryTheory.Bicone J)

instance CategoryTheory.finBicone (J : Type u₁) [Fintype J] : Fintype (CategoryTheory.Bicone J)

inductive CategoryTheory.BiconeHom (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.Bicone J → CategoryTheory.Bicone J → Type (max u₁ v₁)

• left_id: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left
• right_id: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right CategoryTheory.Bicone.right
• left: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.left (CategoryTheory.Bicone.diagram j)
• right: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → (j : J) → CategoryTheory.BiconeHom J CategoryTheory.Bicone.right (CategoryTheory.Bicone.diagram j)
• diagram: {J : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} J] → {j k : J} → (j ⟶ k) → CategoryTheory.BiconeHom J (CategoryTheory.Bicone.diagram j) (CategoryTheory.Bicone.diagram k)

The homs for a walking Bicone J.

instance CategoryTheory.instInhabitedBiconeHomLeft (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : Inhabited (CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left)

instance CategoryTheory.BiconeHom.decidableEq (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {j : CategoryTheory.Bicone J} {k : CategoryTheory.Bicone J} : DecidableEq (CategoryTheory.BiconeHom J j k)

@[simp]

theorem CategoryTheory.biconeCategoryStruct_comp (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : ∀ {X Y Z : CategoryTheory.Bicone J} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x => X = a → Y = a_1 → HEq f x → (X ⟶ Z)) f (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.left → HEq f CategoryTheory.BiconeHom.left_id → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f CategoryTheory.BiconeHom.left_id → (CategoryTheory.Bicone.left ⟶ Z)) (fun g f h => (_ : CategoryTheory.BiconeHom.left_id = f) ▸ g) (_ : CategoryTheory.Bicone.left = Y) g f) (_ : CategoryTheory.Bicone.left = X) f) (fun h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.right → HEq f CategoryTheory.BiconeHom.right_id → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f CategoryTheory.BiconeHom.right_id → (CategoryTheory.Bicone.right ⟶ Z)) (fun g f h => (_ : CategoryTheory.BiconeHom.right_id = f) ▸ g) (_ : CategoryTheory.Bicone.right = Y) g f) (_ : CategoryTheory.Bicone.right = X) f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.left j) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f (CategoryTheory.BiconeHom.left j) → (CategoryTheory.Bicone.left ⟶ Z)) (fun g f h => (_ : CategoryTheory.BiconeHom.left j = f) ▸ CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 t => CategoryTheory.Bicone.diagram j = a → Z = a_1 → HEq g t → (CategoryTheory.Bicone.left ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k} f h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (f : j_2 ⟶ k) → Z = CategoryTheory.Bicone.diagram k → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.left ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram j ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.left ⟶ Z)) (fun g h => (_ : CategoryTheory.BiconeHom.diagram f = g) ▸ CategoryTheory.BiconeHom.left k) (_ : CategoryTheory.Bicone.diagram k = Z) g) val_eq f) (_ : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.diagram j) (_ : Z = Z) (_ : HEq g g)) (_ : CategoryTheory.Bicone.diagram j = Y) g f) (_ : CategoryTheory.Bicone.left = X) f) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.right j) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f (CategoryTheory.BiconeHom.right j) → (CategoryTheory.Bicone.right ⟶ Z)) (fun g f h => (_ : CategoryTheory.BiconeHom.right j = f) ▸ CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 t => CategoryTheory.Bicone.diagram j = a → Z = a_1 → HEq g t → (CategoryTheory.Bicone.right ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k} f h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (f : j_2 ⟶ k) → Z = CategoryTheory.Bicone.diagram k → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.right ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram j ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram f) → (CategoryTheory.Bicone.right ⟶ Z)) (fun g h => (_ : CategoryTheory.BiconeHom.diagram f = g) ▸ CategoryTheory.BiconeHom.right k) (_ : CategoryTheory.Bicone.diagram k = Z) g) val_eq f) (_ : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.diagram j) (_ : Z = Z) (_ : HEq g g)) (_ : CategoryTheory.Bicone.diagram j = Y) g f) (_ : CategoryTheory.Bicone.right = X) f) (fun {j k} f_1 h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram k → HEq f (CategoryTheory.BiconeHom.diagram f_1) → (X ⟶ Z)) (fun f h => Eq.ndrec (motive := fun {Y} => (Y ⟶ Z) → (f : CategoryTheory.Bicone.diagram j ⟶ Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1) → (CategoryTheory.Bicone.diagram j ⟶ Z)) (fun g f h => (_ : CategoryTheory.BiconeHom.diagram f_1 = f) ▸ CategoryTheory.BiconeHom.casesOn (motive := fun a a_1 x => CategoryTheory.Bicone.diagram k = a → Z = a_1 → HEq g x → (CategoryTheory.Bicone.diagram j ⟶ Z)) g (fun h => CategoryTheory.Bicone.noConfusion h) (fun h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun j_1 h => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k_1} g_1 h => CategoryTheory.Bicone.noConfusion h fun val_eq => Eq.ndrec (motive := fun {j_2} => (g_2 : j_2 ⟶ k_1) → Z = CategoryTheory.Bicone.diagram k_1 → HEq g (CategoryTheory.BiconeHom.diagram g_2) → (CategoryTheory.Bicone.diagram j ⟶ Z)) (fun g_2 h => Eq.ndrec (motive := fun {Z} => (g : CategoryTheory.Bicone.diagram k ⟶ Z) → HEq g (CategoryTheory.BiconeHom.diagram g_2) → (CategoryTheory.Bicone.diagram j ⟶ Z)) (fun g h => (_ : CategoryTheory.BiconeHom.diagram g_2 = g) ▸ CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.comp f_1 g_2)) (_ : CategoryTheory.Bicone.diagram k_1 = Z) g) val_eq g_1) (_ : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.diagram k) (_ : Z = Z) (_ : HEq g g)) (_ : CategoryTheory.Bicone.diagram k = Y) g f) (_ : CategoryTheory.Bicone.diagram j = X) f) (_ : X = X) (_ : Y = Y) (_ : HEq f f)

@[simp]

theorem CategoryTheory.biconeCategoryStruct_Hom (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : ∀ (a a_1 : CategoryTheory.Bicone J), (a ⟶ a_1) = CategoryTheory.BiconeHom J a a_1

@[simp]

theorem CategoryTheory.biconeCategoryStruct_id (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.Bicone J) : CategoryTheory.CategoryStruct.id j = CategoryTheory.Bicone.casesOn j CategoryTheory.BiconeHom.left_id CategoryTheory.BiconeHom.right_id fun k => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.id k)

instance CategoryTheory.biconeCategoryStruct (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.CategoryStruct.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)

instance CategoryTheory.biconeCategory (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] : CategoryTheory.Category.{max u₁ v₁, u₁} (CategoryTheory.Bicone J)

@[simp]

theorem CategoryTheory.biconeMk_map (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) : ∀ {X Y : CategoryTheory.Bicone J} (f : X ⟶ Y), (CategoryTheory.biconeMk J c₁ c₂).map f = CategoryTheory.BiconeHom.casesOn J inst✝ (fun a a_1 x => X = a → Y = a_1 → HEq f x → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) X Y f (fun h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.left (fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.left → HEq f CategoryTheory.BiconeHom.left_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.left (fun {Y} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f CategoryTheory.BiconeHom.left_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => (_ : CategoryTheory.BiconeHom.left_id = f) ▸ CategoryTheory.CategoryStruct.id ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left)) Y (_ : CategoryTheory.Bicone.left = Y) f) X (_ : CategoryTheory.Bicone.left = X) f) (fun h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.right (fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.right → HEq f CategoryTheory.BiconeHom.right_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.right (fun {Y} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f CategoryTheory.BiconeHom.right_id → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => (_ : CategoryTheory.BiconeHom.right_id = f) ▸ CategoryTheory.CategoryStruct.id ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right)) Y (_ : CategoryTheory.Bicone.right = Y) f) X (_ : CategoryTheory.Bicone.right = X) f) (fun j h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.left (fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.left j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (CategoryTheory.Bicone J) (CategoryTheory.Bicone.diagram j) (fun {Y} => (f : CategoryTheory.Bicone.left ⟶ Y) → HEq f (CategoryTheory.BiconeHom.left j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.left ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => (_ : CategoryTheory.BiconeHom.left j = f) ▸ c₁.π.app j) Y (_ : CategoryTheory.Bicone.diagram j = Y) f) X (_ : CategoryTheory.Bicone.left = X) f) (fun j h => Eq.ndrec (CategoryTheory.Bicone J) CategoryTheory.Bicone.right (fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram j → HEq f (CategoryTheory.BiconeHom.right j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (CategoryTheory.Bicone J) (CategoryTheory.Bicone.diagram j) (fun {Y} => (f : CategoryTheory.Bicone.right ⟶ Y) → HEq f (CategoryTheory.BiconeHom.right j) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) CategoryTheory.Bicone.right ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => (_ : CategoryTheory.BiconeHom.right j = f) ▸ c₂.π.app j) Y (_ : CategoryTheory.Bicone.diagram j = Y) f) X (_ : CategoryTheory.Bicone.right = X) f) (fun {j k} f_1 h => Eq.ndrec (CategoryTheory.Bicone J) (CategoryTheory.Bicone.diagram j) (fun {X} => (f : X ⟶ Y) → Y = CategoryTheory.Bicone.diagram k → HEq f (CategoryTheory.BiconeHom.diagram f_1) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) X ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => Eq.ndrec (CategoryTheory.Bicone J) (CategoryTheory.Bicone.diagram k) (fun {Y} => (f : CategoryTheory.Bicone.diagram j ⟶ Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1) → ((fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) (CategoryTheory.Bicone.diagram j) ⟶ (fun X => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j) Y)) (fun f h => (_ : CategoryTheory.BiconeHom.diagram f_1 = f) ▸ F.map f_1) Y (_ : CategoryTheory.Bicone.diagram k = Y) f) X (_ : CategoryTheory.Bicone.diagram j = X) f) (_ : X = X) (_ : Y = Y) (_ : HEq f f)

@[simp]

theorem CategoryTheory.biconeMk_obj (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) (X : CategoryTheory.Bicone J) : (CategoryTheory.biconeMk J c₁ c₂).obj X = CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j

def CategoryTheory.biconeMk (J : Type v₁) [CategoryTheory.SmallCategory J] {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor J C} (c₁ : CategoryTheory.Limits.Cone F) (c₂ : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor (CategoryTheory.Bicone J) C

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

instance CategoryTheory.finBiconeHom (J : Type v₁) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (j : CategoryTheory.Bicone J) (k : CategoryTheory.Bicone J) : Fintype (j ⟶ k)

instance CategoryTheory.biconeSmallCategory (J : Type v₁) [CategoryTheory.SmallCategory J] : CategoryTheory.SmallCategory (CategoryTheory.Bicone J)

instance CategoryTheory.biconeFinCategory (J : Type v₁) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.FinCategory (CategoryTheory.Bicone J)