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₂₃.
Equations
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₂₃.
Equations
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₁₂.
Equations
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₁₂)
:
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.threeδ₃Toδ₂'
{ι : Type u_1}
[Preorder ι]
(i₀ i₁ i₂ i₃ : ι)
(hi₀₁ : i₀ ≤ i₁)
(hi₁₂ : i₁ ≤ i₂)
(hi₂₃ : i₂ ≤ i₃)
:
Variant of threeδ₃Toδ₂ for preorders.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.threeδ₁Toδ₀'
{ι : Type u_1}
[Preorder ι]
(i₀ i₁ i₂ i₃ : ι)
(hi₀₁ : i₀ ≤ i₁)
(hi₁₂ : i₁ ≤ i₂)
(hi₂₃ : i₂ ≤ i₃)
:
Variant of threeδ₁Toδ₀ for preorders.