Functors to ComposableArrows C 1

@[implicit_reducible]

def CategoryTheory.ComposableArrows.functorArrows (C : Type u) [Category.{v, u} C] (i j n : ℕ) (hij : i ≤ j := by lia) (hj : j ≤ n := by lia) : Functor (ComposableArrows C n) (ComposableArrows C 1)

The functor ComposableArrows C n ⥤ ComposableArrows C 1 which sends S to mk₁ (S.map' i j) when i, j and n are such that i ≤ j and j ≤ n.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.functorArrows_obj (C : Type u) [Category.{v, u} C] (i j n : ℕ) (hij : i ≤ j := by lia) (hj : j ≤ n := by lia) (S : ComposableArrows C n) : (functorArrows C i j n hij hj).obj S = mk₁ (S.map' i j hij hj)

@[simp]

theorem CategoryTheory.ComposableArrows.functorArrows_map (C : Type u) [Category.{v, u} C] (i j n : ℕ) (hij : i ≤ j := by lia) (hj : j ≤ n := by lia) {S S' : ComposableArrows C n} (φ : S ⟶ S') : (functorArrows C i j n hij hj).map φ = homMk₁ (φ.app ⟨i, ⋯⟩) (φ.app ⟨j, ⋯⟩) ⋯

def CategoryTheory.ComposableArrows.mapFunctorArrows (C : Type u) [Category.{v, u} C] (i j i' j' n : ℕ) (x✝ : i ≤ j := by lia) (x✝¹ : i' ≤ j' := by lia) : autoParam (i ≤ i') mapFunctorArrows._auto_5 → (x✝² : autoParam (j ≤ j') mapFunctorArrows._auto_7) → (x✝³ : autoParam (j' ≤ n) mapFunctorArrows._auto_9) → functorArrows C i j n ⋯ ⋯ ⟶ functorArrows C i' j' n ⋯ ⋯

The natural transformation functorArrows C i j n ⟶ functorArrows C i' j' n when i ≤ i' and j ≤ j'.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.mapFunctorArrows_app (C : Type u) [Category.{v, u} C] (i j i' j' n : ℕ) (x✝ : i ≤ j := by lia) (x✝¹ : i' ≤ j' := by lia) (x✝² : i ≤ i' := by lia) (x✝³ : j ≤ j' := by lia) (x✝⁴ : j' ≤ n := by lia) (S : ComposableArrows C n) : (mapFunctorArrows C i j i' j' n x✝ x✝¹ x✝² x✝³ x✝⁴).app S = homMk₁ (S.map' i i' x✝² ⋯) (S.map' j j' x✝³ x✝⁴) ⋯