Documentation

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

This is used in CategoryTheory.Functor.Flat.

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

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

Instances For

    The homs for a walking Bicone J.

    Instances For
      instance CategoryTheory.instInhabitedBiconeHomLeft (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] :
      Inhabited (CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left)
      @[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 = aY = a_1HEq f x → (X Z)) f (fun h => Eq.ndrec (motive := fun {X} => (f : X Y) → Y = CategoryTheory.Bicone.leftHEq 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.rightHEq 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 jHEq 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 = aZ = a_1HEq 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 kHEq 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 jHEq 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 = aZ = a_1HEq 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 kHEq 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 kHEq 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 = aZ = a_1HEq 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_1HEq 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.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 = aY = a_1HEq 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.leftHEq 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.rightHEq 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 jHEq 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 jHEq 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 kHEq 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)

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

      Instances For