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
.
Given a category J
, construct a walking Bicone J
by adjoining two elements.
- left: {J : Type u₁} → CategoryTheory.Bicone J
- right: {J : Type u₁} → CategoryTheory.Bicone J
- diagram: {J : Type u₁} → J → CategoryTheory.Bicone J
Instances For
instance
CategoryTheory.instDecidableEqBicone :
{J : Type u_1} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Bicone J)
Equations
- CategoryTheory.instDecidableEqBicone = CategoryTheory.decEqBicone✝
Equations
- CategoryTheory.instInhabitedBicone J = { default := CategoryTheory.Bicone.left }
Equations
- One or more equations did not get rendered due to their size.
inductive
CategoryTheory.BiconeHom
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
:
CategoryTheory.Bicone J → CategoryTheory.Bicone J → Type (max u₁ v₁)
The homs for a walking Bicone J
.
- 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)
Instances For
instance
CategoryTheory.instInhabitedBiconeHomLeft
(J : Type u₁)
[CategoryTheory.Category.{v₁, u₁} J]
:
Inhabited (CategoryTheory.BiconeHom J CategoryTheory.Bicone.left CategoryTheory.Bicone.left)
Equations
- CategoryTheory.instInhabitedBiconeHomLeft J = { default := CategoryTheory.BiconeHom.left_id }
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)
Equations
- One or more equations did not get rendered due to their size.
@[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 : J) =>
CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.id k)
@[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_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 = a → Y = a_1 → HEq 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.left → HEq 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.right → HEq 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 j → HEq 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 = a → Z = a_1 → HEq 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 k →
HEq 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 j → HEq 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 = a → Z = a_1 → HEq 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 k →
HEq 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 k → HEq 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 = a → Z = a_1 → HEq 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_1 →
HEq 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.
Equations
@[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 = a →
Y = a_1 →
HEq 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.left →
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)
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.right →
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)
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 j →
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)
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 j →
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)
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 k →
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)
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)
⋯ ⋯ ⋯
@[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 : 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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.finBiconeHom
(J : Type v₁)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
(j : CategoryTheory.Bicone J)
(k : CategoryTheory.Bicone J)
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.biconeFinCategory
(J : Type v₁)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Equations
- CategoryTheory.biconeFinCategory J = { fintypeObj := inferInstance, fintypeHom := inferInstance }