API for compositions of two arrows

Given morphisms f : i ⟶ j, g : j ⟶ k, and fg : i ⟶ k in a category C such that f ≫ g = fg, we define maps twoδ₂Toδ₁ : mk₁ f ⟶ mk₁ fg and twoδ₁Toδ₀ : mk₁ fg ⟶ mk₁ g in the category ComposableArrows C 1. The names are justified by the fact that ComposableArrow.mk₂ f g can be thought of as a 2-simplex in the simplicial set nerve C, and its faces (numbered from 0 to 2) are respectively mk₁ g, mk₁ fg and mk₁ f.

def CategoryTheory.ComposableArrows.twoδ₂Toδ₁ {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : mk₁ f ⟶ mk₁ fg

The morphism mk₁ f ⟶ mk₁ fg when f ≫ g = fg for some morphism g.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : (twoδ₂Toδ₁ f g fg h).app 0 = CategoryStruct.id ((mk₁ f).obj 0)

@[simp]

theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : (twoδ₂Toδ₁ f g fg h).app 1 = g

def CategoryTheory.ComposableArrows.twoδ₁Toδ₀ {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : mk₁ fg ⟶ mk₁ g

The morphism mk₁ fg ⟶ mk₁ g when f ≫ g = fg for some morphism f.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : (twoδ₁Toδ₀ f g fg h).app 0 = f

@[simp]

theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one {C : Type u} [Category.{v, u} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) : (twoδ₁Toδ₀ f g fg h).app 1 = CategoryStruct.id ((mk₁ fg).obj 1)