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 F
s, we can join them into a diagram Bicone J ⥤ C
via
biconeMk
.
This is used in CategoryTheory.Functor.Flat
.
- 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.
Instances For
instance
CategoryTheory.instDecidableEqBicone :
{J : Type u_1} → [inst : DecidableEq J] → DecidableEq (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
.
Instances For
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)
@[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)
:
Given a diagram F : J ⥤ C
and two Cone F
s, we can join them into a diagram Bicone J ⥤ C
.
Instances For
instance
CategoryTheory.finBiconeHom
(J : Type v₁)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
(j : CategoryTheory.Bicone J)
(k : CategoryTheory.Bicone J)
:
instance
CategoryTheory.biconeFinCategory
(J : Type v₁)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
: