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 functors 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) [CategoryTheory.Category.{u_2, u_1} C] (n : ℕ) : Type (max u_2 u_1)

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

Equations

• CategoryTheory.ComposableArrows C n = CategoryTheory.Functor (Fin (n + 1)) C

def CategoryTheory.ComposableArrows.tacticValid : Lean.ParserDescr

A wrapper for omega which prefaces it with some quick and useful attempts

Equations

• CategoryTheory.ComposableArrows.tacticValid = Lean.ParserDescr.node `CategoryTheory.ComposableArrows.tacticValid 1024 (Lean.ParserDescr.nonReservedSymbol "valid" false)

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.obj' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ) (hi : autoParam (i ≤ n) _auto✝) : C

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

Equations

• CategoryTheory.ComposableArrows.obj' F i = F.toPrefunctor.obj { val := i, isLt := (_ : i < n + 1) }

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.map' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ) (j : ℕ) (hij : autoParam (i ≤ j) _auto✝) (hjn : autoParam (j ≤ n) _auto✝) : F.toPrefunctor.obj { val := i, isLt := (_ : i < n + 1) } ⟶ F.toPrefunctor.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

• CategoryTheory.ComposableArrows.map' F i j = F.toPrefunctor.map (CategoryTheory.homOfLE (_ : { val := i, isLt := (_ : i < n + 1) } ≤ { val := j, isLt := (_ : j < n + 1) }))

theorem CategoryTheory.ComposableArrows.map'_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ) (hi : autoParam (i ≤ n) _auto✝) : CategoryTheory.ComposableArrows.map' F i i = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj { val := i, isLt := (_ : i < n + 1) })

theorem CategoryTheory.ComposableArrows.map'_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i ≤ j) _auto✝) (hjk : autoParam (j ≤ k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) : CategoryTheory.ComposableArrows.map' F i k = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i j) (CategoryTheory.ComposableArrows.map' F j k)

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) : C

The leftmost object of F : ComposableArrows C n.

Equations

• CategoryTheory.ComposableArrows.left F = CategoryTheory.ComposableArrows.obj' F 0

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) : C

The rightmost object of F : ComposableArrows C n.

Equations

• CategoryTheory.ComposableArrows.right F = CategoryTheory.ComposableArrows.obj' F n

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) : CategoryTheory.ComposableArrows.left F ⟶ CategoryTheory.ComposableArrows.right F

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

Equations

• CategoryTheory.ComposableArrows.hom F = CategoryTheory.ComposableArrows.map' F 0 n

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.app' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (φ : F ⟶ G) (i : ℕ) (hi : autoParam (i ≤ n) _auto✝) : CategoryTheory.ComposableArrows.obj' F i ⟶ CategoryTheory.ComposableArrows.obj' G i

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

• CategoryTheory.ComposableArrows.app' φ i = φ.app { val := i, isLt := (_ : i < n + 1) }

theorem CategoryTheory.ComposableArrows.naturality'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (φ : F ⟶ G) (i : ℕ) (j : ℕ) (hij : autoParam (i ≤ j) _auto✝) (hj : autoParam (j ≤ n) _auto✝) {Z : C} (h : CategoryTheory.ComposableArrows.obj' G j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G i j) h)

theorem CategoryTheory.ComposableArrows.naturality' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (φ : F ⟶ G) (i : ℕ) (j : ℕ) (hij : autoParam (i ≤ j) _auto✝) (hj : autoParam (j ≤ n) _auto✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i j) (CategoryTheory.ComposableArrows.app' φ j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i) (CategoryTheory.ComposableArrows.map' G i j)

@[simp]

theorem CategoryTheory.ComposableArrows.mk₀_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : ∀ (x : Fin 1), (CategoryTheory.ComposableArrows.mk₀ X).toPrefunctor.obj x = X

@[simp]

theorem CategoryTheory.ComposableArrows.mk₀_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : ∀ {X_1 Y : Fin 1} (x : X_1 ⟶ Y), (CategoryTheory.ComposableArrows.mk₀ X).toPrefunctor.map x = CategoryTheory.CategoryStruct.id X

def CategoryTheory.ComposableArrows.mk₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) : CategoryTheory.ComposableArrows C 0

Constructor for ComposableArrows C 0.

Equations

• CategoryTheory.ComposableArrows.mk₀ X = (CategoryTheory.Functor.const (Fin 1)).toPrefunctor.obj X

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

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

Equations

• CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ x = match x with | { val := 0, isLt := isLt } => X₀ | { val := 1, isLt := isLt } => X₁

def CategoryTheory.ComposableArrows.Mk₁.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) (i : Fin 2) (j : Fin 2) : i ≤ j → (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i ⟶ CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ 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.

theorem CategoryTheory.ComposableArrows.Mk₁.map_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) (i : Fin 2) : CategoryTheory.ComposableArrows.Mk₁.map f i i (_ : i ≤ i) = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i)

theorem CategoryTheory.ComposableArrows.Mk₁.map_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) {i : Fin 2} {j : Fin 2} {k : Fin 2} (hij : i ≤ j) (hjk : j ≤ k) : CategoryTheory.ComposableArrows.Mk₁.map f i k (_ : i ≤ k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Mk₁.map f i j hij) (CategoryTheory.ComposableArrows.Mk₁.map f j k hjk)

@[simp]

theorem CategoryTheory.ComposableArrows.mk₁_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) : ∀ {X Y : Fin (1 + 1)} (g : X ⟶ Y), (CategoryTheory.ComposableArrows.mk₁ f).toPrefunctor.map g = CategoryTheory.ComposableArrows.Mk₁.map f X Y (_ : X ≤ Y)

@[simp]

theorem CategoryTheory.ComposableArrows.mk₁_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) : ∀ (a : Fin 2), (CategoryTheory.ComposableArrows.mk₁ f).toPrefunctor.obj a = CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ a

def CategoryTheory.ComposableArrows.mk₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} (f : X₀ ⟶ X₁) : CategoryTheory.ComposableArrows C 1

Constructor for ComposableArrows C 1.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.homMk_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.toPrefunctor.obj i ⟶ G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }) (CategoryTheory.ComposableArrows.map' G i (i + 1))) (i : Fin (n + 1)) : (CategoryTheory.ComposableArrows.homMk app w).app i = app i

def CategoryTheory.ComposableArrows.homMk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.toPrefunctor.obj i ⟶ G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }) (CategoryTheory.ComposableArrows.map' G i (i + 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

• CategoryTheory.ComposableArrows.homMk app w = CategoryTheory.NatTrans.mk app

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.toPrefunctor.obj i ≅ G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1))) : (CategoryTheory.ComposableArrows.isoMk app w).inv = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).inv) (_ : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G i (i + 1)) ((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) }) (CategoryTheory.ComposableArrows.map' F i (i + 1)))

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.toPrefunctor.obj i ≅ G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1))) : (CategoryTheory.ComposableArrows.isoMk app w).hom = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).hom) w

def CategoryTheory.ComposableArrows.isoMk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (app : (i : Fin (n + 1)) → F.toPrefunctor.obj i ≅ G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (app { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := (_ : i < n + 1) }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1))) : 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.

theorem CategoryTheory.ComposableArrows.ext {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C n} {G : CategoryTheory.ComposableArrows C n} (h : ∀ (i : Fin (n + 1)), F.toPrefunctor.obj i = G.toPrefunctor.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.ComposableArrows.map' F i (i + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.toPrefunctor.obj { val := i, isLt := (_ : i < n + 1) } = G.toPrefunctor.obj { val := i, isLt := (_ : i < n + 1) })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G i (i + 1)) (CategoryTheory.eqToHom (_ : G.toPrefunctor.obj { val := i + 1, isLt := (_ : i + 1 < n + 1) } = F.toPrefunctor.obj { val := i + 1, isLt := (_ : i + 1 < n + 1) })))) : F = G

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₀_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (f : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.homMk₀ f).app i = match i with | { val := 0, isLt := isLt } => f

def CategoryTheory.ComposableArrows.homMk₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (f : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) : F ⟶ G

Constructor for morphisms in ComposableArrows C 0.

Equations

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

theorem CategoryTheory.ComposableArrows.hom_ext₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} {φ : F ⟶ G} {φ' : F ⟶ G} (h : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) : φ = φ'

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₀_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (e : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i = match i with | { val := 0, isLt := isLt } => e.hom

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₀_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (e : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (i : Fin (0 + 1)) : (CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i = match i with | { val := 0, isLt := isLt } => e.inv

def CategoryTheory.ComposableArrows.isoMk₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (e : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) : F ≅ G

Constructor for isomorphisms in ComposableArrows C 0.

Equations

• CategoryTheory.ComposableArrows.isoMk₀ e = CategoryTheory.Iso.mk (CategoryTheory.ComposableArrows.homMk₀ e.hom) (CategoryTheory.ComposableArrows.homMk₀ e.inv)

theorem CategoryTheory.ComposableArrows.ext₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 0} {G : CategoryTheory.ComposableArrows C 0} (h : CategoryTheory.ComposableArrows.obj' F 0 = G.toPrefunctor.obj 0) : F = G

theorem CategoryTheory.ComposableArrows.mk₀_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.ComposableArrows C 0) : ∃ (X : C), F = CategoryTheory.ComposableArrows.mk₀ X

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₁_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (right : CategoryTheory.ComposableArrows.obj' F 1 ⟶ CategoryTheory.ComposableArrows.obj' G 1) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) right = CategoryTheory.CategoryStruct.comp left (CategoryTheory.ComposableArrows.map' G 0 1)) _auto✝) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.homMk₁ left right).app i = match i with | { val := 0, isLt := isLt } => left | { val := 1, isLt := isLt } => right

def CategoryTheory.ComposableArrows.homMk₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (right : CategoryTheory.ComposableArrows.obj' F 1 ⟶ CategoryTheory.ComposableArrows.obj' G 1) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) right = CategoryTheory.CategoryStruct.comp left (CategoryTheory.ComposableArrows.map' G 0 1)) _auto✝) : F ⟶ G

Constructor for morphisms in ComposableArrows C 1.

Equations

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

theorem CategoryTheory.ComposableArrows.hom_ext₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} {φ : F ⟶ G} {φ' : F ⟶ G} (h₀ : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) (h₁ : CategoryTheory.ComposableArrows.app' φ 1 = CategoryTheory.ComposableArrows.app' φ' 1) : φ = φ'

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₁_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (right : CategoryTheory.ComposableArrows.obj' F 1 ≅ CategoryTheory.ComposableArrows.obj' G 1) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) right.hom = CategoryTheory.CategoryStruct.comp left.hom (CategoryTheory.ComposableArrows.map' G 0 1)) _auto✝) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.isoMk₁ left right).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} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (right : CategoryTheory.ComposableArrows.obj' F 1 ≅ CategoryTheory.ComposableArrows.obj' G 1) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) right.hom = CategoryTheory.CategoryStruct.comp left.hom (CategoryTheory.ComposableArrows.map' G 0 1)) _auto✝) (i : Fin (1 + 1)) : (CategoryTheory.ComposableArrows.isoMk₁ left right).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} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (right : CategoryTheory.ComposableArrows.obj' F 1 ≅ CategoryTheory.ComposableArrows.obj' G 1) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) right.hom = CategoryTheory.CategoryStruct.comp left.hom (CategoryTheory.ComposableArrows.map' G 0 1)) _auto✝) : F ≅ G

Constructor for isomorphisms in ComposableArrows C 1.

Equations

• CategoryTheory.ComposableArrows.isoMk₁ left right = CategoryTheory.Iso.mk (CategoryTheory.ComposableArrows.homMk₁ left.hom right.hom) (CategoryTheory.ComposableArrows.homMk₁ left.inv right.inv)

theorem CategoryTheory.ComposableArrows.map'_eq_hom₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (F : CategoryTheory.ComposableArrows C 1) : CategoryTheory.ComposableArrows.map' F 0 1 = CategoryTheory.ComposableArrows.hom F

theorem CategoryTheory.ComposableArrows.ext₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.ComposableArrows C 1} {G : CategoryTheory.ComposableArrows C 1} (left : CategoryTheory.ComposableArrows.left F = CategoryTheory.ComposableArrows.left G) (right : CategoryTheory.ComposableArrows.right F = CategoryTheory.ComposableArrows.right G) (w : CategoryTheory.ComposableArrows.hom F = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom left) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.hom G) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.right G = CategoryTheory.ComposableArrows.right F)))) : F = G

theorem CategoryTheory.ComposableArrows.mk₁_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 1) : ∃ (X₀ : C) (X₁ : C) (f : X₀ ⟶ X₁), X = CategoryTheory.ComposableArrows.mk₁ f

def CategoryTheory.ComposableArrows.Precomp.obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (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

• CategoryTheory.ComposableArrows.Precomp.obj F X x = match x with | { val := 0, isLt := isLt } => X | { val := Nat.succ i, isLt := hi } => CategoryTheory.ComposableArrows.obj' F i

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C) : CategoryTheory.ComposableArrows.Precomp.obj F X 0 = X

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C) : CategoryTheory.ComposableArrows.Precomp.obj F X 1 = CategoryTheory.ComposableArrows.obj' F 0

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (X : C) (i : ℕ) (hi : i + 1 < n + 1 + 1) : CategoryTheory.ComposableArrows.Precomp.obj F X { val := i + 1, isLt := hi } = CategoryTheory.ComposableArrows.obj' F i

def CategoryTheory.ComposableArrows.Precomp.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) (i : Fin (n + 1 + 1)) (j : Fin (n + 1 + 1)) : i ≤ j → (CategoryTheory.ComposableArrows.Precomp.obj F X i ⟶ CategoryTheory.ComposableArrows.Precomp.obj F X j)

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.

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : CategoryTheory.ComposableArrows.Precomp.map F f 0 0 (_ : 0 ≤ 0) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_one_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : CategoryTheory.ComposableArrows.Precomp.map F f 1 1 (_ : 1 ≤ 1) = F.toPrefunctor.map (CategoryTheory.CategoryStruct.id { val := 0, isLt := (_ : 0 < n + 1) })

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : CategoryTheory.ComposableArrows.Precomp.map F f 0 1 (_ : 0 ≤ 1) = f

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left 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} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left 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 }) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.ComposableArrows.map' F 0 (j + 1))

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_succ_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left 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 = CategoryTheory.ComposableArrows.map' F i j

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_one_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left 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 }) = CategoryTheory.ComposableArrows.map' F 0 j

theorem CategoryTheory.ComposableArrows.Precomp.map_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) (i : Fin (n + 1 + 1)) : CategoryTheory.ComposableArrows.Precomp.map F f i i (_ : i ≤ i) = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Precomp.obj F X i)

theorem CategoryTheory.ComposableArrows.Precomp.map_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) {i : Fin (n + 1 + 1)} {j : Fin (n + 1 + 1)} {k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) : CategoryTheory.ComposableArrows.Precomp.map F f i k (_ : i ≤ k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Precomp.map F f i j hij) (CategoryTheory.ComposableArrows.Precomp.map F f j k hjk)

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : ∀ (a : Fin (n + 1 + 1)), (CategoryTheory.ComposableArrows.precomp F f).toPrefunctor.obj a = CategoryTheory.ComposableArrows.Precomp.obj F X a

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : ∀ {X_1 Y : Fin (n + 1 + 1)} (g : X_1 ⟶ Y), (CategoryTheory.ComposableArrows.precomp F f).toPrefunctor.map g = CategoryTheory.ComposableArrows.Precomp.map F f X_1 Y (_ : X_1 ≤ Y)

def CategoryTheory.ComposableArrows.precomp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : CategoryTheory.ComposableArrows C (n + 1)

"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.

def CategoryTheory.ComposableArrows.mk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : CategoryTheory.ComposableArrows C 2

Constructor for ComposableArrows C 2.

Equations

• CategoryTheory.ComposableArrows.mk₂ f g = CategoryTheory.ComposableArrows.precomp (CategoryTheory.ComposableArrows.mk₁ g) f

def CategoryTheory.ComposableArrows.mk₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : CategoryTheory.ComposableArrows C 3

Constructor for ComposableArrows C 3.

Equations

• CategoryTheory.ComposableArrows.mk₃ f g h = CategoryTheory.ComposableArrows.precomp (CategoryTheory.ComposableArrows.mk₂ g h) f

def CategoryTheory.ComposableArrows.mk₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ : C} {X₁ : C} {X₂ : C} {X₃ : C} {X₄ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) : CategoryTheory.ComposableArrows C 4

Constructor for ComposableArrows C 4.

Equations

• CategoryTheory.ComposableArrows.mk₄ f g h i = CategoryTheory.ComposableArrows.precomp (CategoryTheory.ComposableArrows.mk₃ g h i) f

def CategoryTheory.ComposableArrows.mk₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {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₅) : CategoryTheory.ComposableArrows C 5

Constructor for ComposableArrows C 5.

Equations

• CategoryTheory.ComposableArrows.mk₅ f g h i j = CategoryTheory.ComposableArrows.precomp (CategoryTheory.ComposableArrows.mk₄ g h i j) f

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} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (F : CategoryTheory.ComposableArrows C m) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (X : Fin (n + 1)) : (CategoryTheory.ComposableArrows.whiskerLeft F Φ).toPrefunctor.obj X = F.toPrefunctor.obj (Φ.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeft_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (F : CategoryTheory.ComposableArrows C m) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) : ∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.whiskerLeft F Φ).toPrefunctor.map f = F.toPrefunctor.map (Φ.toPrefunctor.map f)

def CategoryTheory.ComposableArrows.whiskerLeft {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (F : CategoryTheory.ComposableArrows C m) (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) : CategoryTheory.ComposableArrows C n

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

Equations

• CategoryTheory.ComposableArrows.whiskerLeft F Φ = CategoryTheory.Functor.comp Φ F

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) : ∀ {X Y : CategoryTheory.ComposableArrows C m} (f : X ⟶ Y) (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).toPrefunctor.map f).app X_1 = f.app (Φ.toPrefunctor.obj X_1)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : CategoryTheory.ComposableArrows C m) (X : Fin (n + 1)) : ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).toPrefunctor.obj F).toPrefunctor.obj X = F.toPrefunctor.obj (Φ.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) (F : CategoryTheory.ComposableArrows C m) : ∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).toPrefunctor.obj F).toPrefunctor.map f = F.toPrefunctor.map (Φ.toPrefunctor.map f)

def CategoryTheory.ComposableArrows.whiskerLeftFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))) : CategoryTheory.Functor (CategoryTheory.ComposableArrows C m) (CategoryTheory.ComposableArrows C n)

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.

@[simp]

theorem Fin.succFunctor_obj (n : ℕ) (i : Fin n) : (Fin.succFunctor n).toPrefunctor.obj i = Fin.succ i

@[simp]

theorem Fin.succFunctor_map (n : ℕ) {i : Fin n} {j : Fin n} (hij : i ⟶ j) : (Fin.succFunctor n).toPrefunctor.map hij = CategoryTheory.homOfLE (_ : Fin.succ i ≤ Fin.succ j)

def Fin.succFunctor (n : ℕ) : CategoryTheory.Functor (Fin n) (Fin (n + 1))

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.

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) : ∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.obj F).toPrefunctor.map f = F.toPrefunctor.map (CategoryTheory.homOfLE (_ : Fin.succ X ≤ Fin.succ Y))

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) (X : Fin (n + 1)) : (CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.obj F).toPrefunctor.obj X = F.toPrefunctor.obj (Fin.succ X)

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} : ∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.map f).app X_1 = f.app (Fin.succ X_1)

def CategoryTheory.ComposableArrows.δ₀Functor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} : CategoryTheory.Functor (CategoryTheory.ComposableArrows C (n + 1)) (CategoryTheory.ComposableArrows C n)

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

Equations

• CategoryTheory.ComposableArrows.δ₀Functor = CategoryTheory.ComposableArrows.whiskerLeftFunctor (Fin.succFunctor (n + 1))

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) : CategoryTheory.ComposableArrows C n

The ComposableArrows C n obtained by forgetting the first arrow.

Equations

• CategoryTheory.ComposableArrows.δ₀ F = CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.obj F

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C} (f : X ⟶ CategoryTheory.ComposableArrows.left F) : CategoryTheory.ComposableArrows.δ₀ (CategoryTheory.ComposableArrows.precomp F f) = F

@[simp]

theorem Fin.castSuccFunctor_map (n : ℕ) : ∀ {X Y : Fin n} (hij : X ⟶ Y), (Fin.castSuccFunctor n).toPrefunctor.map hij = hij

@[simp]

theorem Fin.castSuccFunctor_obj (n : ℕ) (i : Fin n) : (Fin.castSuccFunctor n).toPrefunctor.obj i = Fin.castSucc i

def Fin.castSuccFunctor (n : ℕ) : CategoryTheory.Functor (Fin n) (Fin (n + 1))

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

Equations

• Fin.castSuccFunctor n = CategoryTheory.Functor.mk { obj := fun (i : Fin n) => Fin.castSucc i, map := fun {X Y : Fin n} (hij : X ⟶ Y) => hij }

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) : ∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.δlastFunctor.toPrefunctor.obj F).toPrefunctor.map f = F.toPrefunctor.map f

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) (X : Fin (n + 1)) : (CategoryTheory.ComposableArrows.δlastFunctor.toPrefunctor.obj F).toPrefunctor.obj X = F.toPrefunctor.obj (Fin.castSucc X)

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_map_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} : ∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δlastFunctor.toPrefunctor.map f).app X_1 = f.app (Fin.castSucc X_1)

def CategoryTheory.ComposableArrows.δlastFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} : CategoryTheory.Functor (CategoryTheory.ComposableArrows C (n + 1)) (CategoryTheory.ComposableArrows C n)

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

Equations

• CategoryTheory.ComposableArrows.δlastFunctor = CategoryTheory.ComposableArrows.whiskerLeftFunctor (Fin.castSuccFunctor (n + 1))

@[inline, reducible]

abbrev CategoryTheory.ComposableArrows.δlast {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) : CategoryTheory.ComposableArrows C n

The ComposableArrows C n obtained by forgetting the first arrow.

Equations

• CategoryTheory.ComposableArrows.δlast F = CategoryTheory.ComposableArrows.δlastFunctor.toPrefunctor.obj F

def CategoryTheory.ComposableArrows.homMkSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ⟶ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β 0) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.ComposableArrows.map' G 0 1)) : 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.

@[simp]

theorem CategoryTheory.ComposableArrows.homMkSucc_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ⟶ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β 0) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.ComposableArrows.map' G 0 1)) : (CategoryTheory.ComposableArrows.homMkSucc α β w).app 0 = α

@[simp]

theorem CategoryTheory.ComposableArrows.homMkSucc_app_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ⟶ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ⟶ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β 0) = CategoryTheory.CategoryStruct.comp α (CategoryTheory.ComposableArrows.map' G 0 1)) (i : ℕ) (hi : i + 1 < n + 1 + 1) : (CategoryTheory.ComposableArrows.homMkSucc α β w).app { val := i + 1, isLt := hi } = CategoryTheory.ComposableArrows.app' β i

theorem CategoryTheory.ComposableArrows.hom_ext_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} {f : F ⟶ G} {g : F ⟶ G} (h₀ : CategoryTheory.ComposableArrows.app' f 0 = CategoryTheory.ComposableArrows.app' g 0) (h₁ : CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.map f = CategoryTheory.ComposableArrows.δ₀Functor.toPrefunctor.map g) : f = g

@[simp]

theorem CategoryTheory.ComposableArrows.isoMkSucc_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ≅ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β.hom 0) = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.ComposableArrows.map' G 0 1)) : (CategoryTheory.ComposableArrows.isoMkSucc α β w).hom = CategoryTheory.ComposableArrows.homMkSucc α.hom β.hom w

@[simp]

theorem CategoryTheory.ComposableArrows.isoMkSucc_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ≅ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β.hom 0) = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.ComposableArrows.map' G 0 1)) : (CategoryTheory.ComposableArrows.isoMkSucc α β w).inv = CategoryTheory.ComposableArrows.homMkSucc α.inv β.inv (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G 0 1) (CategoryTheory.ComposableArrows.app' β.inv 0) = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.ComposableArrows.map' F 0 1))

def CategoryTheory.ComposableArrows.isoMkSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (α : CategoryTheory.ComposableArrows.obj' F 0 ≅ CategoryTheory.ComposableArrows.obj' G 0) (β : CategoryTheory.ComposableArrows.δ₀ F ≅ CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F 0 1) (CategoryTheory.ComposableArrows.app' β.hom 0) = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.ComposableArrows.map' G 0 1)) : 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.

theorem CategoryTheory.ComposableArrows.ext_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {F : CategoryTheory.ComposableArrows C (n + 1)} {G : CategoryTheory.ComposableArrows C (n + 1)} (h₀ : CategoryTheory.ComposableArrows.obj' F 0 = CategoryTheory.ComposableArrows.obj' G 0) (h : CategoryTheory.ComposableArrows.δ₀ F = CategoryTheory.ComposableArrows.δ₀ G) (w : CategoryTheory.ComposableArrows.map' F 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G 0 1) (CategoryTheory.eqToHom (_ : (CategoryTheory.ComposableArrows.δ₀ G).toPrefunctor.obj 0 = (CategoryTheory.ComposableArrows.δ₀ F).toPrefunctor.obj 0)))) : F = G

theorem CategoryTheory.ComposableArrows.precomp_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)) : ∃ (F₀ : CategoryTheory.ComposableArrows C n) (X₀ : C) (f₀ : X₀ ⟶ CategoryTheory.ComposableArrows.left F₀), F = CategoryTheory.ComposableArrows.precomp F₀ f₀

def CategoryTheory.ComposableArrows.homMk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) : f ⟶ g

Constructor for morphisms in ComposableArrows C 2.

Equations

• CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁ = CategoryTheory.ComposableArrows.homMkSucc app₀ (CategoryTheory.ComposableArrows.homMk₁ app₁ app₂) w₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) : (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) : (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} {φ : f ⟶ g} {φ' : f ⟶ g} (h₀ : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) (h₁ : CategoryTheory.ComposableArrows.app' φ 1 = CategoryTheory.ComposableArrows.app' φ' 1) (h₂ : CategoryTheory.ComposableArrows.app' φ 2 = CategoryTheory.ComposableArrows.app' φ' 2) : φ = φ'

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₂_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) : (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).hom = CategoryTheory.ComposableArrows.homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) : (CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) app₁.inv = CategoryTheory.CategoryStruct.comp app₀.inv (CategoryTheory.ComposableArrows.map' f 0 1)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) app₂.inv = CategoryTheory.CategoryStruct.comp app₁.inv (CategoryTheory.ComposableArrows.map' f 1 2))

def CategoryTheory.ComposableArrows.isoMk₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 2.

Equations

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

theorem CategoryTheory.ComposableArrows.ext₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 2} {g : CategoryTheory.ComposableArrows C 2} (h₀ : CategoryTheory.ComposableArrows.obj' f 0 = CategoryTheory.ComposableArrows.obj' g 0) (h₁ : CategoryTheory.ComposableArrows.obj' f 1 = CategoryTheory.ComposableArrows.obj' g 1) (h₂ : CategoryTheory.ComposableArrows.obj' f 2 = CategoryTheory.ComposableArrows.obj' g 2) (w₀ : CategoryTheory.ComposableArrows.map' f 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 1 = CategoryTheory.ComposableArrows.obj' f 1)))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 2 = CategoryTheory.ComposableArrows.obj' f 2)))) : f = g

theorem CategoryTheory.ComposableArrows.mk₂_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 2) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂), X = CategoryTheory.ComposableArrows.mk₂ f₀ f₁

def CategoryTheory.ComposableArrows.homMk₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) : f ⟶ g

Constructor for morphisms in ComposableArrows C 3.

Equations

• CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂ = CategoryTheory.ComposableArrows.homMkSucc app₀ (CategoryTheory.ComposableArrows.homMk₂ app₁ app₂ app₃ w₁ w₂) w₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) : (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) : (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_two {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} {φ : f ⟶ g} {φ' : f ⟶ g} (h₀ : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) (h₁ : CategoryTheory.ComposableArrows.app' φ 1 = CategoryTheory.ComposableArrows.app' φ' 1) (h₂ : CategoryTheory.ComposableArrows.app' φ 2 = CategoryTheory.ComposableArrows.app' φ' 2) (h₃ : CategoryTheory.ComposableArrows.app' φ 3 = CategoryTheory.ComposableArrows.app' φ' 3) : φ = φ'

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₃_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) : (CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv = CategoryTheory.ComposableArrows.homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) app₁.inv = CategoryTheory.CategoryStruct.comp app₀.inv (CategoryTheory.ComposableArrows.map' f 0 1)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) app₂.inv = CategoryTheory.CategoryStruct.comp app₁.inv (CategoryTheory.ComposableArrows.map' f 1 2)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) app₃.inv = CategoryTheory.CategoryStruct.comp app₂.inv (CategoryTheory.ComposableArrows.map' f 2 3))

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₃_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 3.

Equations

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

theorem CategoryTheory.ComposableArrows.ext₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 3} {g : CategoryTheory.ComposableArrows C 3} (h₀ : CategoryTheory.ComposableArrows.obj' f 0 = CategoryTheory.ComposableArrows.obj' g 0) (h₁ : CategoryTheory.ComposableArrows.obj' f 1 = CategoryTheory.ComposableArrows.obj' g 1) (h₂ : CategoryTheory.ComposableArrows.obj' f 2 = CategoryTheory.ComposableArrows.obj' g 2) (h₃ : CategoryTheory.ComposableArrows.obj' f 3 = CategoryTheory.ComposableArrows.obj' g 3) (w₀ : CategoryTheory.ComposableArrows.map' f 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 1 = CategoryTheory.ComposableArrows.obj' f 1)))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 2 = CategoryTheory.ComposableArrows.obj' f 2)))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 3 = CategoryTheory.ComposableArrows.obj' f 3)))) : f = g

theorem CategoryTheory.ComposableArrows.mk₃_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 3) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃), X = CategoryTheory.ComposableArrows.mk₃ f₀ f₁ f₂

def CategoryTheory.ComposableArrows.homMk₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : f ⟶ g

Constructor for morphisms in ComposableArrows C 4.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} {φ : f ⟶ g} {φ' : f ⟶ g} (h₀ : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) (h₁ : CategoryTheory.ComposableArrows.app' φ 1 = CategoryTheory.ComposableArrows.app' φ' 1) (h₂ : CategoryTheory.ComposableArrows.app' φ 2 = CategoryTheory.ComposableArrows.app' φ' 2) (h₃ : CategoryTheory.ComposableArrows.app' φ 3 = CategoryTheory.ComposableArrows.app' φ' 3) (h₄ : CategoryTheory.ComposableArrows.app' φ 4 = CategoryTheory.ComposableArrows.app' φ' 4) : φ = φ'

theorem CategoryTheory.ComposableArrows.map'_inv_eq_inv_map' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {m : ℕ} (h : n + 1 ≤ m) {f : CategoryTheory.ComposableArrows C m} {g : CategoryTheory.ComposableArrows C m} (app : CategoryTheory.ComposableArrows.obj' f n ≅ CategoryTheory.ComposableArrows.obj' g n) (app' : CategoryTheory.ComposableArrows.obj' f (n + 1) ≅ CategoryTheory.ComposableArrows.obj' g (n + 1)) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f n (n + 1)) app'.hom = CategoryTheory.CategoryStruct.comp app.hom (CategoryTheory.ComposableArrows.map' g n (n + 1))) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g n (n + 1)) app'.inv = CategoryTheory.CategoryStruct.comp app.inv (CategoryTheory.ComposableArrows.map' f n (n + 1))

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₄_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) : (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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) app₁.inv = CategoryTheory.CategoryStruct.comp app₀.inv (CategoryTheory.ComposableArrows.map' f 0 1)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) app₂.inv = CategoryTheory.CategoryStruct.comp app₁.inv (CategoryTheory.ComposableArrows.map' f 1 2)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) app₃.inv = CategoryTheory.CategoryStruct.comp app₂.inv (CategoryTheory.ComposableArrows.map' f 2 3)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4) app₄.inv = CategoryTheory.CategoryStruct.comp app₃.inv (CategoryTheory.ComposableArrows.map' f 3 4))

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₄_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 4.

Equations

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

theorem CategoryTheory.ComposableArrows.ext₄ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 4} {g : CategoryTheory.ComposableArrows C 4} (h₀ : CategoryTheory.ComposableArrows.obj' f 0 = CategoryTheory.ComposableArrows.obj' g 0) (h₁ : CategoryTheory.ComposableArrows.obj' f 1 = CategoryTheory.ComposableArrows.obj' g 1) (h₂ : CategoryTheory.ComposableArrows.obj' f 2 = CategoryTheory.ComposableArrows.obj' g 2) (h₃ : CategoryTheory.ComposableArrows.obj' f 3 = CategoryTheory.ComposableArrows.obj' g 3) (h₄ : CategoryTheory.ComposableArrows.obj' f 4 = CategoryTheory.ComposableArrows.obj' g 4) (w₀ : CategoryTheory.ComposableArrows.map' f 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 1 = CategoryTheory.ComposableArrows.obj' f 1)))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 2 = CategoryTheory.ComposableArrows.obj' f 2)))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 3 = CategoryTheory.ComposableArrows.obj' f 3)))) (w₃ : CategoryTheory.ComposableArrows.map' f 3 4 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 4 = CategoryTheory.ComposableArrows.obj' f 4)))) : f = g

theorem CategoryTheory.ComposableArrows.mk₄_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 4) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄), X = CategoryTheory.ComposableArrows.mk₄ f₀ f₁ f₂ f₃

def CategoryTheory.ComposableArrows.homMk₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : f ⟶ g

Constructor for morphisms in ComposableArrows C 5.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ⟶ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ⟶ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ⟶ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ⟶ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ⟶ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ⟶ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁ = CategoryTheory.CategoryStruct.comp app₀ (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂ = CategoryTheory.CategoryStruct.comp app₁ (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃ = CategoryTheory.CategoryStruct.comp app₂ (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄ = CategoryTheory.CategoryStruct.comp app₃ (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅ = CategoryTheory.CategoryStruct.comp app₄ (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} {φ : f ⟶ g} {φ' : f ⟶ g} (h₀ : CategoryTheory.ComposableArrows.app' φ 0 = CategoryTheory.ComposableArrows.app' φ' 0) (h₁ : CategoryTheory.ComposableArrows.app' φ 1 = CategoryTheory.ComposableArrows.app' φ' 1) (h₂ : CategoryTheory.ComposableArrows.app' φ 2 = CategoryTheory.ComposableArrows.app' φ' 2) (h₃ : CategoryTheory.ComposableArrows.app' φ 3 = CategoryTheory.ComposableArrows.app' φ' 3) (h₄ : CategoryTheory.ComposableArrows.app' φ 4 = CategoryTheory.ComposableArrows.app' φ' 4) (h₅ : CategoryTheory.ComposableArrows.app' φ 5 = CategoryTheory.ComposableArrows.app' φ' 5) : φ = φ'

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₅_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ≅ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (CategoryTheory.ComposableArrows.map' g 4 5)) : (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 (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) app₁.inv = CategoryTheory.CategoryStruct.comp app₀.inv (CategoryTheory.ComposableArrows.map' f 0 1)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) app₂.inv = CategoryTheory.CategoryStruct.comp app₁.inv (CategoryTheory.ComposableArrows.map' f 1 2)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) app₃.inv = CategoryTheory.CategoryStruct.comp app₂.inv (CategoryTheory.ComposableArrows.map' f 2 3)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4) app₄.inv = CategoryTheory.CategoryStruct.comp app₃.inv (CategoryTheory.ComposableArrows.map' f 3 4)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 4 5) app₅.inv = CategoryTheory.CategoryStruct.comp app₄.inv (CategoryTheory.ComposableArrows.map' f 4 5))

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₅_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ≅ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (CategoryTheory.ComposableArrows.map' g 4 5)) : (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} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (app₀ : CategoryTheory.ComposableArrows.obj' f 0 ≅ CategoryTheory.ComposableArrows.obj' g 0) (app₁ : CategoryTheory.ComposableArrows.obj' f 1 ≅ CategoryTheory.ComposableArrows.obj' g 1) (app₂ : CategoryTheory.ComposableArrows.obj' f 2 ≅ CategoryTheory.ComposableArrows.obj' g 2) (app₃ : CategoryTheory.ComposableArrows.obj' f 3 ≅ CategoryTheory.ComposableArrows.obj' g 3) (app₄ : CategoryTheory.ComposableArrows.obj' f 4 ≅ CategoryTheory.ComposableArrows.obj' g 4) (app₅ : CategoryTheory.ComposableArrows.obj' f 5 ≅ CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 0 1) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (CategoryTheory.ComposableArrows.map' g 0 1)) (w₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 1 2) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (CategoryTheory.ComposableArrows.map' g 1 2)) (w₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 2 3) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (CategoryTheory.ComposableArrows.map' g 2 3)) (w₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 3 4) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (CategoryTheory.ComposableArrows.map' g 3 4)) (w₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f 4 5) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (CategoryTheory.ComposableArrows.map' g 4 5)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 5.

Equations

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

theorem CategoryTheory.ComposableArrows.ext₅ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {f : CategoryTheory.ComposableArrows C 5} {g : CategoryTheory.ComposableArrows C 5} (h₀ : CategoryTheory.ComposableArrows.obj' f 0 = CategoryTheory.ComposableArrows.obj' g 0) (h₁ : CategoryTheory.ComposableArrows.obj' f 1 = CategoryTheory.ComposableArrows.obj' g 1) (h₂ : CategoryTheory.ComposableArrows.obj' f 2 = CategoryTheory.ComposableArrows.obj' g 2) (h₃ : CategoryTheory.ComposableArrows.obj' f 3 = CategoryTheory.ComposableArrows.obj' g 3) (h₄ : CategoryTheory.ComposableArrows.obj' f 4 = CategoryTheory.ComposableArrows.obj' g 4) (h₅ : CategoryTheory.ComposableArrows.obj' f 5 = CategoryTheory.ComposableArrows.obj' g 5) (w₀ : CategoryTheory.ComposableArrows.map' f 0 1 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 0 1) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 1 = CategoryTheory.ComposableArrows.obj' f 1)))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 2 = CategoryTheory.ComposableArrows.obj' f 2)))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 3 = CategoryTheory.ComposableArrows.obj' f 3)))) (w₃ : CategoryTheory.ComposableArrows.map' f 3 4 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 4 = CategoryTheory.ComposableArrows.obj' f 4)))) (w₄ : CategoryTheory.ComposableArrows.map' f 4 5 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 4 5) (CategoryTheory.eqToHom (_ : CategoryTheory.ComposableArrows.obj' g 5 = CategoryTheory.ComposableArrows.obj' f 5)))) : f = g

theorem CategoryTheory.ComposableArrows.mk₅_surjective {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.ComposableArrows C 5) : ∃ (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₄

def CategoryTheory.ComposableArrows.arrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i : ℕ) (hi : autoParam (i < n) _auto✝) : CategoryTheory.ComposableArrows C 1

The ith arrow of F : ComposableArrows C n.

Equations

• CategoryTheory.ComposableArrows.arrow F i = CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.ComposableArrows.map' F i (i + 1))

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj (Fin.castSucc i) ⟶ obj (Fin.succ i)) : ∃ (F : CategoryTheory.ComposableArrows C n) (e : (i : Fin (n + 1)) → F.toPrefunctor.obj i ≅ obj i), ∀ (i : ℕ) (hi : i < n), mapSucc { val := i, isLt := hi } = CategoryTheory.CategoryStruct.comp (e { val := i, isLt := (_ : i < n + 1) }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1)) (e { val := i + 1, isLt := (_ : i + 1 < n + 1) }).hom)

noncomputable def CategoryTheory.ComposableArrows.mkOfObjOfMapSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj (Fin.castSucc i) ⟶ obj (Fin.succ i)) : CategoryTheory.ComposableArrows C n

Given obj : Fin (n + 1) → C and mapSucc i : obj i.castSucc ⟶ obj i.succ for all i : Fin n, this is F : ComposableArrows C n such that F.obj i is definitionally equal to obj i and such that F.map' i (i + 1) = mapSucc ⟨i, hi⟩.

Equations

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

@[simp]

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj (Fin.castSucc i) ⟶ obj (Fin.succ i)) (i : Fin (n + 1)) : (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).toPrefunctor.obj i = obj i

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj (Fin.castSucc i) ⟶ obj (Fin.succ i)) (i : ℕ) (hi : autoParam (i < n) _auto✝) : CategoryTheory.ComposableArrows.map' (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc) i (i + 1) = mapSucc { val := i, isLt := hi }

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj (Fin.castSucc i) ⟶ obj (Fin.succ i)) (i : ℕ) (hi : autoParam (i < n) _auto✝) : CategoryTheory.ComposableArrows.arrow (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc) i = CategoryTheory.ComposableArrows.mk₁ (mapSucc { val := i, isLt := hi })

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_obj_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ) (F : CategoryTheory.Functor (Fin (n + 1)) C) : ∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), ((CategoryTheory.Functor.mapComposableArrows G n).toPrefunctor.obj F).toPrefunctor.map f = G.toPrefunctor.map (F.toPrefunctor.map f)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_map_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ) : ∀ {X Y : CategoryTheory.Functor (Fin (n + 1)) C} (α : X ⟶ Y) (X_1 : Fin (n + 1)), ((CategoryTheory.Functor.mapComposableArrows G n).toPrefunctor.map α).app X_1 = G.toPrefunctor.map (α.app X_1)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_obj_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ) (F : CategoryTheory.Functor (Fin (n + 1)) C) (X : Fin (n + 1)) : ((CategoryTheory.Functor.mapComposableArrows G n).toPrefunctor.obj F).toPrefunctor.obj X = G.toPrefunctor.obj (F.toPrefunctor.obj X)

def CategoryTheory.Functor.mapComposableArrows {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (n : ℕ) : CategoryTheory.Functor (CategoryTheory.ComposableArrows C n) (CategoryTheory.ComposableArrows D n)

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

Equations

• CategoryTheory.Functor.mapComposableArrows G n = (CategoryTheory.whiskeringRight (Fin (n + 1)) C D).toPrefunctor.obj G