Arrows of composable strings, and isomorphism classes of their vertices

For positions i ≤ j of a string F : ComposableArrows C n of composable arrows, its arrow from the i-th to the j-th object, viewed as a total arrow of C, is F.totalArrow i j hij. The string is determined by these arrows (CategoryTheory.ComposableArrows.ext_of_totalArrow); reindexing the string along a functor of the indexing posets reindexes its arrows (CategoryTheory.ComposableArrows.totalArrow_whiskerLeft), prepending an arrow with CategoryTheory.ComposableArrows.precomp shifts them (CategoryTheory.ComposableArrows.totalArrow_precomp_succ_succ), and applying a functor to the string maps its arrows along the functor (CategoryTheory.ComposableArrows.totalArrow_mapComposableArrows_obj) and commutes with prepending (CategoryTheory.Functor.mapComposableArrows_obj_precomp). A string of at least one arrow is already determined by its first arrow and the remaining string (CategoryTheory.ComposableArrows.ext_succ_of_totalArrow).

All vertices of a composable string in a groupoid have the same isomorphism class.

Main declarations

• CategoryTheory.ComposableArrows.totalArrow: the arrow of a string between two positions.
• CategoryTheory.ComposableArrows.ext_of_totalArrow: a string is determined by its arrows.
• CategoryTheory.ComposableArrows.ext_succ_of_totalArrow: a string is determined by its first arrow and its remaining arrows.
• CategoryTheory.ComposableArrows.quotient_mk_obj: the vertices of a string in a groupoid are isomorphic.

def CategoryTheory.ComposableArrows.totalArrow {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) (i j : Fin (n + 1)) (hij : i ≤ j) : Quiver.Total C

The arrow of a string of composable arrows from its i-th to its j-th object, as a total arrow of C. For i = j this is the identity arrow of the i-th object.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_left {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) (i j : Fin (n + 1)) (hij : i ≤ j) : (F.totalArrow i j hij).left = F.obj i

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_right {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) (i j : Fin (n + 1)) (hij : i ≤ j) : (F.totalArrow i j hij).right = F.obj j

theorem CategoryTheory.ComposableArrows.totalArrow_def {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) (i j : Fin (n + 1)) (hij : i ≤ j) : F.totalArrow i j hij = { left := F.obj i, right := F.obj j, hom := F.map (homOfLE hij) }

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_self {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) (i : Fin (n + 1)) : F.totalArrow i i ⋯ = { left := F.obj i, right := F.obj i, hom := CategoryStruct.id (F.obj i) }

The arrow of a string of composable arrows from a position to itself is an identity arrow.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_precomp_zero_one {C : Type u} [Category.{v, u} C] {n : ℕ} (a : Quiver.Total C) (F : ComposableArrows C n) (h : a.right = F.left) : (F.precomp (CategoryStruct.comp a.hom (eqToHom h))).totalArrow 0 1 ⋯ = a

The first arrow of a string obtained by prepending an arrow is that arrow, including when its target is identified with the first vertex by an equality.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_precomp_zero_succ_succ {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : ℕ) (hj : j + 2 < n + 1 + 1) : (F.precomp f).totalArrow 0 ⟨j + 2, hj⟩ ⋯ = { left := X, right := F.obj' (j + 1) ⋯, hom := CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯) }

An arrow from the new first vertex to a later vertex is the prepended arrow followed by an arrow of the original string.

theorem CategoryTheory.ComposableArrows.totalArrow_precomp_zero_succ {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : Fin (n + 1)) : (F.precomp f).totalArrow 0 j.succ ⋯ = { left := X, right := F.obj j, hom := CategoryStruct.comp f (F.map (homOfLE ⋯)) }

An arrow from the new first vertex of a prepended string to a shifted vertex is the prepended arrow followed by an arrow of the original string. Unlike CategoryTheory.ComposableArrows.totalArrow_precomp_zero_succ_succ, this holds uniformly in the target position, including the first arrow.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_precomp_succ_succ {C : Type u} [Category.{v, u} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i j : Fin (n + 1)) (hij : i ≤ j) : (F.precomp f).totalArrow i.succ j.succ ⋯ = F.totalArrow i j hij

Arrows between shifted vertices of a prepended string are the arrows of the original string.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_whiskerLeft {C : Type u} [Category.{v, u} C] {n m : ℕ} (F : ComposableArrows C m) (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) (i j : Fin (n + 1)) (hij : i ≤ j) : (F.whiskerLeft Φ).totalArrow i j hij = F.totalArrow (Φ.obj i) (Φ.obj j) ⋯

Reindexing a string of composable arrows along a functor Φ of the indexing posets reindexes its arrows.

@[simp]

theorem CategoryTheory.ComposableArrows.totalArrow_mapComposableArrows_obj {C : Type u} [Category.{v, u} C] {n : ℕ} {D : Type u_1} [Category.{u_2, u_1} D] (Φ : Functor C D) (F : ComposableArrows C n) (i j : Fin (n + 1)) (hij : i ≤ j) : ((Φ.mapComposableArrows n).obj F).totalArrow i j hij = Φ.toPrefunctor.mapTotal (F.totalArrow i j hij)

An arrow of the image of a string under a functor is the image of the arrow of the string.

theorem CategoryTheory.ComposableArrows.ext_of_totalArrow {C : Type u} [Category.{v, u} C] {n : ℕ} {F G : ComposableArrows C n} (h : ∀ (i j : Fin (n + 1)) (hij : i ≤ j), F.totalArrow i j hij = G.totalArrow i j hij) : F = G

A string of composable arrows is determined by its arrows.

theorem CategoryTheory.ComposableArrows.ext_succ_of_totalArrow {C : Type u} [Category.{v, u} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (h : F.δ₀ = G.δ₀) (w : F.totalArrow 0 1 ⋯ = G.totalArrow 0 1 ⋯) : F = G

A string of at least one composable arrow is determined by its first arrow and the string F.δ₀ of the remaining arrows.

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_obj_precomp {C : Type u} [Category.{v, u} C] {n : ℕ} {D : Type u_1} [Category.{u_2, u_1} D] (Φ : Functor C D) (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : (Φ.mapComposableArrows (n + 1)).obj (F.precomp f) = ((Φ.mapComposableArrows n).obj F).precomp (Φ.map f)

Applying a functor to a string with a prepended arrow prepends the image of that arrow to the image of the string.

@[simp]

theorem CategoryTheory.ComposableArrows.quotient_mk_obj {C : Type u_1} [Category.{u_2, u_1} C] [IsGroupoid C] {n : ℕ} (F : ComposableArrows C n) (i : Fin (n + 1)) : ⟦F.obj i⟧ = ⟦F.obj 0⟧

All vertices of a composable string in a groupoid represent the same isomorphism class.

theorem CategoryTheory.ComposableArrows.mk₁_eq_mk₁_iff {C : Type u_1} [Category.{u_2, u_1} C] {X₀ X₁ Y₀ Y₁ : C} {f : X₀ ⟶ X₁} {f' : Y₀ ⟶ Y₁} : mk₁ f = mk₁ f' ↔ Arrow.mk f = Arrow.mk f'

The composable arrows mk₁ f and mk₁ f' are equal exactly when f and f' are equal as arrows.