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) : mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃

The morphism mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃ when f₂ ≫ f₃ = f₂₃.

Equations

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

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) : mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃

The morphism mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃ when f₁ ≫ f₂ = f₁₂ and f₂ ≫ f₃ = f₂₃.

Equations

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

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) : mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃

The morphism mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃ when f₁ ≫ f₂ = f₁₂.

Equations

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

@[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₂₃) : (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0 = CategoryStruct.id ((mk₂ f₁ f₂).obj 0)

@[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₂₃) : (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1 = CategoryStruct.id ((mk₂ f₁ f₂).obj 1)

@[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₂₃) : (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 2 = 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₂₃) : (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 0 = CategoryStruct.id ((mk₂ f₁ f₂₃).obj 0)

@[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₂₃) : (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = 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₂₃) : (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2 = CategoryStruct.id ((mk₂ f₁ f₂₃).obj 2)

@[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₁₂) : (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 0 = 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₁₂) : (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1 = CategoryStruct.id ((mk₂ f₁₂ f₃).obj 1)

@[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₁₂) : (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2 = CategoryStruct.id ((mk₂ f₁₂ f₃).obj 2)

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.threeδ₃Toδ₂' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) : mk₂ (homOfLE hi₀₁) (homOfLE hi₁₂) ⟶ mk₂ (homOfLE hi₀₁) (homOfLE ⋯)

Variant of threeδ₃Toδ₂ for preorders.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.threeδ₂Toδ₁' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) : mk₂ (homOfLE hi₀₁) (homOfLE ⋯) ⟶ mk₂ (homOfLE ⋯) (homOfLE hi₂₃)

Variant of threeδ₂Toδ₁ for preorders.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.threeδ₁Toδ₀' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ i₃ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) : mk₂ (homOfLE ⋯) (homOfLE hi₂₃) ⟶ mk₂ (homOfLE hi₁₂) (homOfLE hi₂₃)

Variant of threeδ₁Toδ₀ for preorders.

Equations

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