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.

• left {J : Type u₁} : Bicone J
• right {J : Type u₁} : Bicone J
• diagram {J : Type u₁} (val : J) : Bicone J

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

Equations

• CategoryTheory.instDecidableEqBicone = CategoryTheory.instDecidableEqBicone.decEq

def CategoryTheory.instDecidableEqBicone.decEq {J✝ : Type u_1} [DecidableEq J✝] (x✝ x✝¹ : Bicone J✝) : Decidable (x✝ = x✝¹)

Equations

• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.left CategoryTheory.Bicone.left = isTrue ⋯
• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.left CategoryTheory.Bicone.right = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.left (CategoryTheory.Bicone.diagram val) = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.right CategoryTheory.Bicone.left = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.right CategoryTheory.Bicone.right = isTrue ⋯
• CategoryTheory.instDecidableEqBicone.decEq CategoryTheory.Bicone.right (CategoryTheory.Bicone.diagram val) = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq (CategoryTheory.Bicone.diagram val) CategoryTheory.Bicone.left = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq (CategoryTheory.Bicone.diagram val) CategoryTheory.Bicone.right = isFalse ⋯
• CategoryTheory.instDecidableEqBicone.decEq (CategoryTheory.Bicone.diagram a) (CategoryTheory.Bicone.diagram b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

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

Equations

• CategoryTheory.instInhabitedBicone J = { default := CategoryTheory.Bicone.left }

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

Equations

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

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

The homs for a walking Bicone J.

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

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

Equations

• CategoryTheory.instInhabitedBiconeHomLeft J = { default := CategoryTheory.BiconeHom.left_id }

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.biconeCategory J = { toCategoryStruct := CategoryTheory.biconeCategoryStruct J, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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

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.

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

• CategoryTheory.biconeSmallCategory J = CategoryTheory.biconeCategory J

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

Equations

• CategoryTheory.biconeFinCategory J = { fintypeObj := inferInstance, fintypeHom := inferInstance }