# Documentation

Mathlib.CategoryTheory.ComposableArrows

# Composable arrows #

If C is a category, the type of n-simplices in the nerve of C identifies to the type of functors Fin (n + 1) ⥤ C, which can be thought as families of n composable arrows in C. In this file, we introduce and study this category ComposableArrows C n of n composable arrows in C.

If F : ComposableArrows C n, we define F.left as the leftmost object, F.right as the rightmost object, and F.hom : F.left ⟶ F.right is the canonical map.

The most significant definition in this file is the constructor F.precomp f : ComposableArrows C (n + 1) for F : ComposableArrows C n and f : X ⟶ F.left: "it shifts F towards the right and inserts f on the left". This precomp has good definitional properties.

In the namespace CategoryTheory.ComposableArrows, we provide constructors like mk₁ f, mk₂ f g, mk₃ f g h for ComposableArrows C n for small n.

TODO (@joelriou):

• redefine Arrow C as ComposableArrow C 1?
• construct some elements in ComposableArrows m (Fin (n + 1)) for small n the precomposition with which shall induce funtors ComposableArrows C n ⥤ ComposableArrows C m which correspond to simplicial operations (specifically faces) with good definitional properties (this might be necessary for up to n = 7 in order to formalize spectral sequences following Verdier)
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows (C : Type u_1) [] (n : ) :
Type (max u_2 u_1)

ComposableArrows C n is the type of functors Fin (n + 1) ⥤ C.

Equations
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.obj' {C : Type u_1} [] {n : } (F : ) (i : ) (hi : autoParam (i n) _auto✝) :
C

The ith object (with i : ℕ such that i ≤ n) of F : ComposableArrows C n.

Equations
• = F.obj { val := i, isLt := (_ : i < n + 1) }
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.map' {C : Type u_1} [] {n : } (F : ) (i : ) (j : ) (hij : autoParam (i j) _auto✝) (hjn : autoParam (j n) _auto✝) :
F.obj { val := i, isLt := (_ : i < n + 1) } F.obj { val := j, isLt := (_ : j < n + 1) }

The map F.obj' i ⟶ F.obj' j when F : ComposableArrows C n, and i and j are natural numbers such that i ≤ j ≤ n.

Equations
Instances For
theorem CategoryTheory.ComposableArrows.map'_self {C : Type u_1} [] {n : } (F : ) (i : ) (hi : autoParam (i n) _auto✝) :
= CategoryTheory.CategoryStruct.id (F.obj { val := i, isLt := (_ : i < n + 1) })
theorem CategoryTheory.ComposableArrows.map'_comp {C : Type u_1} [] {n : } (F : ) (i : ) (j : ) (k : ) (hij : autoParam (i j) _auto✝) (hjk : autoParam (j k) _auto✝) (hk : autoParam (k n) _auto✝) :
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.left {C : Type u_1} [] {n : } (F : ) :
C

The leftmost object of F : ComposableArrows C n.

Equations
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.right {C : Type u_1} [] {n : } (F : ) :
C

The rightmost object of F : ComposableArrows C n.

Equations
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.hom {C : Type u_1} [] {n : } (F : ) :

The canonical map F.left ⟶ F.right for F : ComposableArrows C n.

Equations
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.app' {C : Type u_1} [] {n : } {F : } {G : } (φ : F G) (i : ) (hi : autoParam (i n) _auto✝) :

The map F.obj' i ⟶ G.obj' i induced on ith objects by a morphism F ⟶ G in ComposableArrows C n when i is a natural number such that i ≤ n.

Equations
• = φ.app { val := i, isLt := (_ : i < n + 1) }
Instances For
theorem CategoryTheory.ComposableArrows.naturality'_assoc {C : Type u_1} [] {n : } {F : } {G : } (φ : F G) (i : ) (j : ) (hij : autoParam (i j) _auto✝) (hj : autoParam (j n) _auto✝) {Z : C} (h : ) :
theorem CategoryTheory.ComposableArrows.naturality' {C : Type u_1} [] {n : } {F : } {G : } (φ : F G) (i : ) (j : ) (hij : autoParam (i j) _auto✝) (hj : autoParam (j n) _auto✝) :
@[simp]
theorem CategoryTheory.ComposableArrows.mk₀_obj {C : Type u_1} [] (X : C) :
∀ (x : Fin 1), .obj x = X
@[simp]
theorem CategoryTheory.ComposableArrows.mk₀_map {C : Type u_1} [] (X : C) :
∀ {X_1 Y : Fin 1} (x : X_1 Y),
def CategoryTheory.ComposableArrows.mk₀ {C : Type u_1} [] (X : C) :

Constructor for ComposableArrows C 0.

Equations
Instances For
def CategoryTheory.ComposableArrows.Mk₁.obj {C : Type u_1} (X₀ : C) (X₁ : C) :
Fin 2C

The map which sends 0 : Fin 2 to X₀ and 1 to X₁.

Equations
• = match x with | { val := 0, isLt := isLt } => X₀ | { val := 1, isLt := isLt } => X₁
Instances For
def CategoryTheory.ComposableArrows.Mk₁.map {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) (i : Fin 2) (j : Fin 2) :
i j()

The obvious map obj X₀ X₁ i ⟶ obj X₀ X₁ j whenever i j : Fin 2 satisfy i ≤ j.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.Mk₁.map_id {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) (i : Fin 2) :
theorem CategoryTheory.ComposableArrows.Mk₁.map_comp {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) {i : Fin 2} {j : Fin 2} {k : Fin 2} (hij : i j) (hjk : j k) :
@[simp]
theorem CategoryTheory.ComposableArrows.mk₁_obj {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) :
∀ (a : Fin 2),
@[simp]
theorem CategoryTheory.ComposableArrows.mk₁_map {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) :
∀ {X Y : Fin (1 + 1)} (g : X Y), .map g = CategoryTheory.ComposableArrows.Mk₁.map f X Y (_ : X Y)
def CategoryTheory.ComposableArrows.mk₁ {C : Type u_1} [] {X₀ : C} {X₁ : C} (f : X₀ X₁) :

Constructor for ComposableArrows C 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMk_app {C : Type u_1} [] {n : } {F : } {G : } (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }) ()) (i : Fin (n + 1)) :
.app i = app i
def CategoryTheory.ComposableArrows.homMk {C : Type u_1} [] {n : } {F : } {G : } (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }) ()) :
F G

Constructor for morphisms F ⟶ G in ComposableArrows C n which takes as inputs a family of morphisms F.obj i ⟶ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

Equations
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk_inv {C : Type u_1} [] {n : } {F : } {G : } (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom ()) :
.inv = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).inv) (_ : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () ((fun (i : Fin (n + 1)) => (app i).inv) { val := i + 1, isLt := (_ : i + 1 < n + 1) }) = CategoryTheory.CategoryStruct.comp ((fun (i : Fin (n + 1)) => (app i).inv) { val := i, isLt := (_ : i < n + 1) }) ())
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk_hom {C : Type u_1} [] {n : } {F : } {G : } (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom ()) :
.hom = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).hom) w
def CategoryTheory.ComposableArrows.isoMk {C : Type u_1} [] {n : } {F : } {G : } (app : (i : Fin (n + 1)) → F.obj i G.obj i) (w : ∀ (i : ) (hi : i < n), CategoryTheory.CategoryStruct.comp () (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom ()) :
F G

Constructor for isomorphisms F ≅ G in ComposableArrows C n which takes as inputs a family of isomorphisms F.obj i ≅ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.ext {C : Type u_1} [] {n : } {F : } {G : } (h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i) (w : ∀ (i : ) (hi : i < n), = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.obj { val := i, isLt := (_ : i < n + 1) } = G.obj { val := i, isLt := (_ : i < n + 1) })) (CategoryTheory.CategoryStruct.comp () (CategoryTheory.eqToHom (_ : G.obj { val := i + 1, isLt := (_ : i + 1 < n + 1) } = F.obj { val := i + 1, isLt := (_ : i + 1 < n + 1) })))) :
F = G
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₀_app {C : Type u_1} [] {F : } {G : } (i : Fin (0 + 1)) :
= match i with | { val := 0, isLt := isLt } => f
def CategoryTheory.ComposableArrows.homMk₀ {C : Type u_1} [] {F : } {G : } :
F G

Constructor for morphisms in ComposableArrows C 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.hom_ext₀ {C : Type u_1} [] {F : } {G : } {φ : F G} {φ' : F G} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₀_inv_app {C : Type u_1} [] {F : } {G : } (i : Fin (0 + 1)) :
.app i = match i with | { val := 0, isLt := isLt } => e.inv
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₀_hom_app {C : Type u_1} [] {F : } {G : } (i : Fin (0 + 1)) :
.app i = match i with | { val := 0, isLt := isLt } => e.hom
def CategoryTheory.ComposableArrows.isoMk₀ {C : Type u_1} [] {F : } {G : } :
F G

Constructor for isomorphisms in ComposableArrows C 0.

Equations
Instances For
theorem CategoryTheory.ComposableArrows.ext₀ {C : Type u_1} [] {F : } {G : } (h : = G.obj 0) :
F = G
theorem CategoryTheory.ComposableArrows.mk₀_surjective {C : Type u_1} [] (F : ) :
∃ (X : C),
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₁_app {C : Type u_1} [] {F : } {G : } (right : ) (w : ) (i : Fin (1 + 1)) :
().app i = match i with | { val := 0, isLt := isLt } => left | { val := 1, isLt := isLt } => right
def CategoryTheory.ComposableArrows.homMk₁ {C : Type u_1} [] {F : } {G : } (right : ) (w : ) :
F G

Constructor for morphisms in ComposableArrows C 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.hom_ext₁ {C : Type u_1} [] {F : } {G : } {φ : F G} {φ' : F G} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₁_hom_app {C : Type u_1} [] {F : } {G : } (right : ) (w : autoParam ( = ) _auto✝) (i : Fin (1 + 1)) :
().hom.app i = match i with | { val := 0, isLt := isLt } => left.hom | { val := 1, isLt := isLt } => right.hom
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₁_inv_app {C : Type u_1} [] {F : } {G : } (right : ) (w : autoParam ( = ) _auto✝) (i : Fin (1 + 1)) :
().inv.app i = match i with | { val := 0, isLt := isLt } => left.inv | { val := 1, isLt := isLt } => right.inv
def CategoryTheory.ComposableArrows.isoMk₁ {C : Type u_1} [] {F : } {G : } (right : ) (w : autoParam ( = ) _auto✝) :
F G

Constructor for isomorphisms in ComposableArrows C 1.

Equations
Instances For
theorem CategoryTheory.ComposableArrows.ext₁ {C : Type u_1} [] {F : } {G : } :
F = G
theorem CategoryTheory.ComposableArrows.mk₁_surjective {C : Type u_1} [] (X : ) :
∃ (X₀ : C) (X₁ : C) (f : X₀ X₁),
def CategoryTheory.ComposableArrows.Precomp.obj {C : Type u_1} [] {n : } (F : ) (X : C) :
Fin (n + 1 + 1)C

The map Fin (n + 1 + 1) → C which "shifts" F.obj' to the right and inserts X in the zeroth position.

Equations
• = match x with | { val := 0, isLt := isLt } => X | { val := , isLt := hi } =>
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.obj_zero {C : Type u_1} [] {n : } (F : ) (X : C) :
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.obj_one {C : Type u_1} [] {n : } (F : ) (X : C) :
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.obj_succ {C : Type u_1} [] {n : } (F : ) (X : C) (i : ) (hi : i + 1 < n + 1 + 1) :
CategoryTheory.ComposableArrows.Precomp.obj F X { val := i + 1, isLt := hi } =
def CategoryTheory.ComposableArrows.Precomp.map {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) (i : Fin (n + 1 + 1)) (j : Fin (n + 1 + 1)) :

Auxiliary definition for the action on maps of the functor F.precomp f. It sends 0 ≤ 1 to f and i + 1 ≤ j + 1 to F.map' i j.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_zero_zero {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_one_one {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
CategoryTheory.ComposableArrows.Precomp.map F f 1 1 (_ : 1 1) = F.map (CategoryTheory.CategoryStruct.id { val := 0, isLt := (_ : 0 < n + 1) })
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one' {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
CategoryTheory.ComposableArrows.Precomp.map F f 0 { val := 0 + 1, isLt := (_ : 0 + 1 < n + 1 + 1) } (_ : 0 { val := 0 + 1, isLt := (_ : 0 + 1 < n + 1 + 1) }) = f
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) (j : ) (hj : j + 2 < n + 1 + 1) :
CategoryTheory.ComposableArrows.Precomp.map F f 0 { val := j + 2, isLt := hj } (_ : 0 { val := j + 2, isLt := hj }) =
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_succ_succ {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) (i : ) (j : ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 j + 1) :
CategoryTheory.ComposableArrows.Precomp.map F f { val := i + 1, isLt := hi } { val := j + 1, isLt := hj } hij =
@[simp]
theorem CategoryTheory.ComposableArrows.Precomp.map_one_succ {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) (j : ) (hj : j + 1 < n + 1 + 1) :
CategoryTheory.ComposableArrows.Precomp.map F f 1 { val := j + 1, isLt := hj } (_ : 1 { val := j + 1, isLt := hj }) =
theorem CategoryTheory.ComposableArrows.Precomp.map_id {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) (i : Fin (n + 1 + 1)) :
theorem CategoryTheory.ComposableArrows.Precomp.map_comp {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) {i : Fin (n + 1 + 1)} {j : Fin (n + 1 + 1)} {k : Fin (n + 1 + 1)} (hij : i j) (hjk : j k) :
@[simp]
theorem CategoryTheory.ComposableArrows.precomp_map {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
∀ {X_1 Y : Fin (n + 1 + 1)} (g : X_1 Y), .map g = CategoryTheory.ComposableArrows.Precomp.map F f X_1 Y (_ : X_1 Y)
@[simp]
theorem CategoryTheory.ComposableArrows.precomp_obj {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
∀ (a : Fin (n + 1 + 1)),
def CategoryTheory.ComposableArrows.precomp {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :

"Precomposition" of F : ComposableArrows C n by a morphism f : X ⟶ F.left.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.ComposableArrows.mk₂ {C : Type u_1} [] {X₀ : C} {X₁ : C} {X₂ : C} (f : X₀ X₁) (g : X₁ X₂) :

Constructor for ComposableArrows C 2.

Equations
Instances For
def CategoryTheory.ComposableArrows.mk₃ {C : Type u_1} [] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) :

Constructor for ComposableArrows C 3.

Equations
Instances For
def CategoryTheory.ComposableArrows.mk₄ {C : Type u_1} [] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) (i : X₃ X₄) :

Constructor for ComposableArrows C 4.

Equations
Instances For
def CategoryTheory.ComposableArrows.mk₅ {C : Type u_1} [] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} {X₅ : C} (f : X₀ X₁) (g : X₁ X₂) (h : X₂ X₃) (i : X₃ X₄) (j : X₄ X₅) :

Constructor for ComposableArrows C 5.

Equations
Instances For

These examples are meant to test the good definitional properties of precomp, and that dsimp can see through.

@[simp]
theorem CategoryTheory.ComposableArrows.whiskerLeft_obj {C : Type u_1} [] {n : } {m : } (F : ) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (X : Fin (n + 1)) :
.obj X = F.obj (Φ.obj X)
@[simp]
theorem CategoryTheory.ComposableArrows.whiskerLeft_map {C : Type u_1} [] {n : } {m : } (F : ) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :
∀ {X Y : Fin (n + 1)} (f : X Y), .map f = F.map (Φ.map f)
def CategoryTheory.ComposableArrows.whiskerLeft {C : Type u_1} [] {n : } {m : } (F : ) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :

The map ComposableArrows C m → ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

Equations
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app {C : Type u_1} [] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :
∀ {X Y : } (f : X Y) (X_1 : Fin (n + 1)), .app X_1 = f.app (Φ.obj X_1)
@[simp]
theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj {C : Type u_1} [] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : ) (X : Fin (n + 1)) :
.obj X = F.obj (Φ.obj X)
@[simp]
theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map {C : Type u_1} [] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : ) :
∀ {X Y : Fin (n + 1)} (f : X Y), .map f = F.map (Φ.map f)
def CategoryTheory.ComposableArrows.whiskerLeftFunctor {C : Type u_1} [] {n : } {m : } (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) :

The functor ComposableArrows C m ⥤ ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Fin.succFunctor_obj (n : ) (i : Fin n) :
().obj i =
@[simp]
theorem Fin.succFunctor_map (n : ) {i : Fin n} {j : Fin n} (hij : i j) :
().map hij = CategoryTheory.homOfLE (_ : )

The functor Fin n ⥤ Fin (n + 1) which sends i to i.succ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_map {C : Type u_1} [] {n : } (F : ) :
∀ {X Y : Fin (n + 1)} (f : X Y), (CategoryTheory.ComposableArrows.δ₀Functor.obj F).map f = F.map (CategoryTheory.homOfLE (_ : ))
@[simp]
theorem CategoryTheory.ComposableArrows.δ₀Functor_map_app {C : Type u_1} [] {n : } :
∀ {X Y : } (f : X Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.map f).app X_1 = f.app (Fin.succ X_1)
@[simp]
theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_obj {C : Type u_1} [] {n : } (F : ) (X : Fin (n + 1)) :
(CategoryTheory.ComposableArrows.δ₀Functor.obj F).obj X = F.obj ()

The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n which forgets the first arrow.

Equations
• CategoryTheory.ComposableArrows.δ₀Functor =
Instances For
@[inline, reducible]
abbrev CategoryTheory.ComposableArrows.δ₀ {C : Type u_1} [] {n : } (F : ) :

The ComposableArrows C n obtained by forgetting the first arrow.

Equations
• = CategoryTheory.ComposableArrows.δ₀Functor.obj F
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.precomp_δ₀ {C : Type u_1} [] {n : } (F : ) {X : C} (f : ) :
def CategoryTheory.ComposableArrows.homMkSucc {C : Type u_1} [] {n : } {F : } {G : } :
F G

Inductive construction of morphisms in ComposableArrows C (n + 1): in order to construct a morphism F ⟶ G, it suffices to provide α : F.obj' 0 ⟶ G.obj' 0 and β : F.δ₀ ⟶ G.δ₀ such that F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMkSucc_app_zero {C : Type u_1} [] {n : } {F : } {G : } :
.app 0 = α
@[simp]
theorem CategoryTheory.ComposableArrows.homMkSucc_app_succ {C : Type u_1} [] {n : } {F : } {G : } (i : ) (hi : i + 1 < n + 1 + 1) :
.app { val := i + 1, isLt := hi } =
theorem CategoryTheory.ComposableArrows.hom_ext_succ {C : Type u_1} [] {n : } {F : } {G : } {f : F G} {g : F G} (h₁ : CategoryTheory.ComposableArrows.δ₀Functor.map f = CategoryTheory.ComposableArrows.δ₀Functor.map g) :
f = g
@[simp]
theorem CategoryTheory.ComposableArrows.isoMkSucc_inv {C : Type u_1} [] {n : } {F : } {G : } (w : ) :
@[simp]
theorem CategoryTheory.ComposableArrows.isoMkSucc_hom {C : Type u_1} [] {n : } {F : } {G : } (w : ) :
def CategoryTheory.ComposableArrows.isoMkSucc {C : Type u_1} [] {n : } {F : } {G : } (w : ) :
F G

Inductive construction of isomorphisms in ComposableArrows C (n + 1): in order to construct an isomorphism F ≅ G, it suffices to provide α : F.obj' 0 ≅ G.obj' 0 and β : F.δ₀ ≅ G.δ₀ such that F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.precomp_surjective {C : Type u_1} [] {n : } (F : ) :
∃ (F₀ : ) (X₀ : C) (f₀ : ),
def CategoryTheory.ComposableArrows.homMk₂ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) :
f g

Constructor for morphisms in ComposableArrows C 2.

Equations
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₂_app_zero {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) :
(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₂_app_one {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) :
(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₂_app_two {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) :
(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app { val := 2, isLt := (_ : 2 < 2 + 1) } = app₂
theorem CategoryTheory.ComposableArrows.hom_ext₂ {C : Type u_1} [] {f : } {g : } {φ : f g} {φ' : f g} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₂_inv {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) :
(CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv (_ : = ) (_ : = )
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₂_hom {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) :
(CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).hom = CategoryTheory.ComposableArrows.homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁
def CategoryTheory.ComposableArrows.isoMk₂ {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) :
f g

Constructor for isomorphisms in ComposableArrows C 2.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.ext₂ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) :
f = g
theorem CategoryTheory.ComposableArrows.mk₂_surjective {C : Type u_1} [] (X : ) :
∃ (X₀ : C) (X₁ : C) (X₂ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂),
def CategoryTheory.ComposableArrows.homMk₃ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
f g

Constructor for morphisms in ComposableArrows C 3.

Equations
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₃_app_zero {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₃_app_one {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₃_app_two {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app { val := 2, isLt := (_ : 2 < 3 + 1) } = app₂
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₃_app_three {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app { val := 3, isLt := (_ : 3 < 3 + 1) } = app₃
theorem CategoryTheory.ComposableArrows.hom_ext₃ {C : Type u_1} [] {f : } {g : } {φ : f g} {φ' : f g} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₃_inv {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) :
(CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv = CategoryTheory.ComposableArrows.homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv (_ : = ) (_ : = ) (_ : = )
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₃_hom {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) :
(CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).hom = CategoryTheory.ComposableArrows.homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂
def CategoryTheory.ComposableArrows.isoMk₃ {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) :
f g

Constructor for isomorphisms in ComposableArrows C 3.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.ext₃ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) :
f = g
theorem CategoryTheory.ComposableArrows.mk₃_surjective {C : Type u_1} [] (X : ) :
∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃), X =
def CategoryTheory.ComposableArrows.homMk₄ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
f g

Constructor for morphisms in ComposableArrows C 4.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₄_app_zero {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 0 = app₀
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₄_app_one {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 1 = app₁
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₄_app_two {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app { val := 2, isLt := (_ : 2 < 4 + 1) } = app₂
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₄_app_three {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app { val := 3, isLt := (_ : 3 < 4 + 1) } = app₃
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₄_app_four {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app { val := 4, isLt := (_ : 4 < 4 + 1) } = app₄
theorem CategoryTheory.ComposableArrows.hom_ext₄ {C : Type u_1} [] {f : } {g : } {φ : f g} {φ' : f g} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₄_inv {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) :
(CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).inv = CategoryTheory.ComposableArrows.homMk₄ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv (_ : = ) (_ : = ) (_ : = ) (_ : = )
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₄_hom {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) :
(CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).hom = CategoryTheory.ComposableArrows.homMk₄ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom w₀ w₁ w₂ w₃
def CategoryTheory.ComposableArrows.isoMk₄ {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) :
f g

Constructor for isomorphisms in ComposableArrows C 4.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.ext₄ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) :
f = g
theorem CategoryTheory.ComposableArrows.mk₄_surjective {C : Type u_1} [] (X : ) :
∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃) (f₃ : X₃ X₄), X =
def CategoryTheory.ComposableArrows.homMk₅ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
f g

Constructor for morphisms in ComposableArrows C 5.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_zero {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 0 = app₀
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_one {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 1 = app₁
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_two {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app { val := 2, isLt := (_ : 2 < 5 + 1) } = app₂
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_three {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app { val := 3, isLt := (_ : 3 < 5 + 1) } = app₃
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_four {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app { val := 4, isLt := (_ : 4 < 5 + 1) } = app₄
@[simp]
theorem CategoryTheory.ComposableArrows.homMk₅_app_five {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app { val := 5, isLt := (_ : 5 < 5 + 1) } = app₅
theorem CategoryTheory.ComposableArrows.hom_ext₅ {C : Type u_1} [] {f : } {g : } {φ : f g} {φ' : f g} :
φ = φ'
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₅_inv {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) (w₄ : = ) :
(CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).inv = CategoryTheory.ComposableArrows.homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv (_ : = ) (_ : = ) (_ : = ) (_ : = ) (_ : = )
@[simp]
theorem CategoryTheory.ComposableArrows.isoMk₅_hom {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) (w₄ : = ) :
(CategoryTheory.ComposableArrows.isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).hom = CategoryTheory.ComposableArrows.homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄
def CategoryTheory.ComposableArrows.isoMk₅ {C : Type u_1} [] {f : } {g : } (w₀ : = ) (w₁ : = ) (w₂ : = ) (w₃ : = ) (w₄ : = ) :
f g

Constructor for isomorphisms in ComposableArrows C 5.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ComposableArrows.ext₅ {C : Type u_1} [] {f : } {g : } (w₀ : ) (w₁ : ) (w₂ : ) (w₃ : ) (w₄ : ) :
f = g
theorem CategoryTheory.ComposableArrows.mk₅_surjective {C : Type u_1} [] (X : ) :
∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (X₅ : C) (f₀ : X₀ X₁) (f₁ : X₁ X₂) (f₂ : X₂ X₃) (f₃ : X₃ X₄) (f₄ : X₄ X₅), X = CategoryTheory.ComposableArrows.mk₅ f₀ f₁ f₂ f₃ f₄
@[simp]
theorem CategoryTheory.Functor.mapComposableArrows_obj_map {C : Type u_1} [] {D : Type u_2} [] (G : ) (n : ) (F : CategoryTheory.Functor (Fin (n + 1)) C) :
∀ {X Y : Fin (n + 1)} (f : X Y), (.obj F).map f = G.map (F.map f)
@[simp]
theorem CategoryTheory.Functor.mapComposableArrows_map_app {C : Type u_1} [] {D : Type u_2} [] (G : ) (n : ) :
∀ {X Y : CategoryTheory.Functor (Fin (n + 1)) C} (α : X Y) (X_1 : Fin (n + 1)), (.map α).app X_1 = G.map (α.app X_1)
@[simp]
theorem CategoryTheory.Functor.mapComposableArrows_obj_obj {C : Type u_1} [] {D : Type u_2} [] (G : ) (n : ) (F : CategoryTheory.Functor (Fin (n + 1)) C) (X : Fin (n + 1)) :
(.obj F).obj X = G.obj (F.obj X)
def CategoryTheory.Functor.mapComposableArrows {C : Type u_1} [] {D : Type u_2} [] (G : ) (n : ) :

The functor ComposableArrows C n ⥤ ComposableArrows D n obtained by postcomposition with a functor C ⥤ D.

Equations
Instances For