API for compositions of three arrows #
Given morphisms f₁ : i ⟶ j, f₂ : j ⟶ k, f₃ : k ⟶ l, and their
compositions f₁₂ : i ⟶ k and f₂₃ : j ⟶ l, we define
maps ComposableArrows.threeδ₃Toδ₂ : mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃,
threeδ₂Toδ₁ : mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃, and threeδ₁Toδ₀ : mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃.
The names are justified by the fact that ComposableArrow.mk₃ f₁ f₂ f₃
can be thought of as a 3-simplex in the simplicial set nerve C,
and its faces (numbered from 0 to 3) are respectively
mk₂ f₂ f₃, mk₂ f₁₂ f₃, mk₂ f₁ f₂₃, mk₂ f₁ f₂.
def
CategoryTheory.ComposableArrows.threeδ₃Toδ₂
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₂₃ : j ⟶ l)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃ := by cat_disch)
:
The morphism mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃ when f₂ ≫ f₃ = f₂₃.
Instances For
def
CategoryTheory.ComposableArrows.threeδ₂Toδ₁
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(f₂₃ : j ⟶ l)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂ := by cat_disch)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃ := by cat_disch)
:
The morphism mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃ when f₁ ≫ f₂ = f₁₂ and f₂ ≫ f₃ = f₂₃.
Instances For
def
CategoryTheory.ComposableArrows.threeδ₁Toδ₀
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂ := by cat_disch)
:
The morphism mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃ when f₁ ≫ f₂ = f₁₂.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_zero
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₂₃ : j ⟶ l)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_one
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₂₃ : j ⟶ l)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_two
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₂₃ : j ⟶ l)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_zero
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(f₂₃ : j ⟶ l)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_one
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(f₂₃ : j ⟶ l)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_two
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(f₂₃ : j ⟶ l)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
(h₂₃ : CategoryStruct.comp f₂ f₃ = f₂₃)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_zero
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_one
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_two
{C : Type u}
[Category.{v, u} C]
{i j k l : C}
(f₁ : i ⟶ j)
(f₂ : j ⟶ k)
(f₃ : k ⟶ l)
(f₁₂ : i ⟶ k)
(h₁₂ : CategoryStruct.comp f₁ f₂ = f₁₂)
: