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
    Equations
    • CategoryTheory.instDecidableEqBicone = CategoryTheory.decEqBicone✝
    Equations
    Equations
    • One or more equations did not get rendered due to their size.

    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)
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      @[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 : CategoryTheory.Bicone J) (x : CategoryTheory.BiconeHom J a a_1) => X = aY = a_1HEq f x(X Z)) f (fun (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.leftHEq f CategoryTheory.BiconeHom.left_id(X Z)) (fun (f : CategoryTheory.Bicone.left Y) (h : Y = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (Y Z)(f : CategoryTheory.Bicone.left Y) → HEq f CategoryTheory.BiconeHom.left_id(CategoryTheory.Bicone.left Z)) (fun (g : CategoryTheory.Bicone.left Z) (f : CategoryTheory.Bicone.left CategoryTheory.Bicone.left) (h : HEq f CategoryTheory.BiconeHom.left_id) => g) g f) f) (fun (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.rightHEq f CategoryTheory.BiconeHom.right_id(X Z)) (fun (f : CategoryTheory.Bicone.right Y) (h : Y = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (Y Z)(f : CategoryTheory.Bicone.right Y) → HEq f CategoryTheory.BiconeHom.right_id(CategoryTheory.Bicone.right Z)) (fun (g : CategoryTheory.Bicone.right Z) (f : CategoryTheory.Bicone.right CategoryTheory.Bicone.right) (h : HEq f CategoryTheory.BiconeHom.right_id) => g) g f) f) (fun (j : J) (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram jHEq f (CategoryTheory.BiconeHom.left j)(X Z)) (fun (f : CategoryTheory.Bicone.left Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (Y Z)(f : CategoryTheory.Bicone.left Y) → HEq f (CategoryTheory.BiconeHom.left j)(CategoryTheory.Bicone.left Z)) (fun (g : CategoryTheory.Bicone.diagram j Z) (f : CategoryTheory.Bicone.left CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.left j)) => CategoryTheory.BiconeHom.casesOn (motive := fun (a a_1 : CategoryTheory.Bicone J) (t : CategoryTheory.BiconeHom J a a_1) => CategoryTheory.Bicone.diagram j = aZ = a_1HEq g t(CategoryTheory.Bicone.left Z)) g (fun (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k : J} (f : j_1 k) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.diagram j_1) => CategoryTheory.Bicone.noConfusion h fun (val_eq : j = j_1) => Eq.ndrec (motive := fun {j_2 : J} => (f : j_2 k) → Z = CategoryTheory.Bicone.diagram kHEq g (CategoryTheory.BiconeHom.diagram f)(CategoryTheory.Bicone.left Z)) (fun (f : j k) (h : Z = CategoryTheory.Bicone.diagram k) => Eq.ndrec (motive := fun {Z : CategoryTheory.Bicone J} => (g : CategoryTheory.Bicone.diagram j Z) → HEq g (CategoryTheory.BiconeHom.diagram f)(CategoryTheory.Bicone.left Z)) (fun (g : CategoryTheory.Bicone.diagram j CategoryTheory.Bicone.diagram k) (h : HEq g (CategoryTheory.BiconeHom.diagram f)) => CategoryTheory.BiconeHom.left k) g) val_eq f) ) g f) f) (fun (j : J) (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram jHEq f (CategoryTheory.BiconeHom.right j)(X Z)) (fun (f : CategoryTheory.Bicone.right Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (Y Z)(f : CategoryTheory.Bicone.right Y) → HEq f (CategoryTheory.BiconeHom.right j)(CategoryTheory.Bicone.right Z)) (fun (g : CategoryTheory.Bicone.diagram j Z) (f : CategoryTheory.Bicone.right CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.right j)) => CategoryTheory.BiconeHom.casesOn (motive := fun (a a_1 : CategoryTheory.Bicone J) (t : CategoryTheory.BiconeHom J a a_1) => CategoryTheory.Bicone.diagram j = aZ = a_1HEq g t(CategoryTheory.Bicone.right Z)) g (fun (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k : J} (f : j_1 k) (h : CategoryTheory.Bicone.diagram j = CategoryTheory.Bicone.diagram j_1) => CategoryTheory.Bicone.noConfusion h fun (val_eq : j = j_1) => Eq.ndrec (motive := fun {j_2 : J} => (f : j_2 k) → Z = CategoryTheory.Bicone.diagram kHEq g (CategoryTheory.BiconeHom.diagram f)(CategoryTheory.Bicone.right Z)) (fun (f : j k) (h : Z = CategoryTheory.Bicone.diagram k) => Eq.ndrec (motive := fun {Z : CategoryTheory.Bicone J} => (g : CategoryTheory.Bicone.diagram j Z) → HEq g (CategoryTheory.BiconeHom.diagram f)(CategoryTheory.Bicone.right Z)) (fun (g : CategoryTheory.Bicone.diagram j CategoryTheory.Bicone.diagram k) (h : HEq g (CategoryTheory.BiconeHom.diagram f)) => CategoryTheory.BiconeHom.right k) g) val_eq f) ) g f) f) (fun {j k : J} (f_1 : j k) (h : X = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram kHEq f (CategoryTheory.BiconeHom.diagram f_1)(X Z)) (fun (f : CategoryTheory.Bicone.diagram j Y) (h : Y = CategoryTheory.Bicone.diagram k) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (Y Z)(f : CategoryTheory.Bicone.diagram j Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1)(CategoryTheory.Bicone.diagram j Z)) (fun (g : CategoryTheory.Bicone.diagram k Z) (f : CategoryTheory.Bicone.diagram j CategoryTheory.Bicone.diagram k) (h : HEq f (CategoryTheory.BiconeHom.diagram f_1)) => CategoryTheory.BiconeHom.casesOn (motive := fun (a a_1 : CategoryTheory.Bicone J) (x : CategoryTheory.BiconeHom J a a_1) => CategoryTheory.Bicone.diagram k = aZ = a_1HEq g x(CategoryTheory.Bicone.diagram j Z)) g (fun (h : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (h : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.left) => CategoryTheory.Bicone.noConfusion h) (fun (j_1 : J) (h : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.right) => CategoryTheory.Bicone.noConfusion h) (fun {j_1 k_1 : J} (g_1 : j_1 k_1) (h : CategoryTheory.Bicone.diagram k = CategoryTheory.Bicone.diagram j_1) => CategoryTheory.Bicone.noConfusion h fun (val_eq : k = j_1) => Eq.ndrec (motive := fun {j_2 : J} => (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 : k k_1) (h : Z = CategoryTheory.Bicone.diagram k_1) => Eq.ndrec (motive := fun {Z : CategoryTheory.Bicone J} => (g : CategoryTheory.Bicone.diagram k Z) → HEq g (CategoryTheory.BiconeHom.diagram g_2)(CategoryTheory.Bicone.diagram j Z)) (fun (g : CategoryTheory.Bicone.diagram k CategoryTheory.Bicone.diagram k_1) (h : HEq g (CategoryTheory.BiconeHom.diagram g_2)) => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.comp f_1 g_2)) g) val_eq g_1) ) g f) f)
      Equations
      • One or more equations did not get rendered due to their size.
      @[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 (motive := fun (a a_1 : CategoryTheory.Bicone J) (x : CategoryTheory.BiconeHom J a a_1) => X = aY = a_1HEq f x((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) f (fun (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.leftHEq f CategoryTheory.BiconeHom.left_id((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.left Y) (h : Y = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.left Y) → HEq f CategoryTheory.BiconeHom.left_id((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.left (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.left CategoryTheory.Bicone.left) (h : HEq f CategoryTheory.BiconeHom.left_id) => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.left)) f) f) (fun (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.rightHEq f CategoryTheory.BiconeHom.right_id((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.right Y) (h : Y = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.right Y) → HEq f CategoryTheory.BiconeHom.right_id((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.right (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.right CategoryTheory.Bicone.right) (h : HEq f CategoryTheory.BiconeHom.right_id) => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.right)) f) f) (fun (j : J) (h : X = CategoryTheory.Bicone.left) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram jHEq f (CategoryTheory.BiconeHom.left j)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.left Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.left Y) → HEq f (CategoryTheory.BiconeHom.left j)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.left (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.left CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.left j)) => c₁.app j) f) f) (fun (j : J) (h : X = CategoryTheory.Bicone.right) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram jHEq f (CategoryTheory.BiconeHom.right j)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.right Y) (h : Y = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.right Y) → HEq f (CategoryTheory.BiconeHom.right j)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) CategoryTheory.Bicone.right (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.right CategoryTheory.Bicone.diagram j) (h : HEq f (CategoryTheory.BiconeHom.right j)) => c₂.app j) f) f) (fun {j k : J} (f_1 : j k) (h : X = CategoryTheory.Bicone.diagram j) => Eq.ndrec (motive := fun {X : CategoryTheory.Bicone J} => (f : X Y) → Y = CategoryTheory.Bicone.diagram kHEq f (CategoryTheory.BiconeHom.diagram f_1)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) X (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.diagram j Y) (h : Y = CategoryTheory.Bicone.diagram k) => Eq.ndrec (motive := fun {Y : CategoryTheory.Bicone J} => (f : CategoryTheory.Bicone.diagram j Y) → HEq f (CategoryTheory.BiconeHom.diagram f_1)((fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) (CategoryTheory.Bicone.diagram j) (fun (X : CategoryTheory.Bicone J) => CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun (j : J) => F.obj j) Y)) (fun (f : CategoryTheory.Bicone.diagram j CategoryTheory.Bicone.diagram k) (h : HEq f (CategoryTheory.BiconeHom.diagram f_1)) => F.map f_1) f) f)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.