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 hi = F.obj { val := i, isLt := ⋯ }

@[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.obj { val := i, isLt := ⋯ } ⟶ F.obj { val := j, isLt := ⋯ }

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 hij hjn = F.map (CategoryTheory.homOfLE ⋯)

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 ⋯ hi = CategoryTheory.CategoryStruct.id (F.obj { val := i, isLt := ⋯ })

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 ⋯ hk = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i j hij ⋯) (CategoryTheory.ComposableArrows.map' F j k hjk hk)

@[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 hi ⟶ CategoryTheory.ComposableArrows.obj' G i hi

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 hi = φ.app { val := i, isLt := ⋯ }

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 hj ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i j hij hj) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ j hj) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G i j hij hj) 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 hij hj) (CategoryTheory.ComposableArrows.app' φ j hj) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯) (CategoryTheory.ComposableArrows.map' G i j hij hj)

@[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).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).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)).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 ⋯ = 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 ⋯ = 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).map g = CategoryTheory.ComposableArrows.Mk₁.map f 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).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.obj i ⟶ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (app { val := i + 1, isLt := ⋯ }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := ⋯ }) (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi)) (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.obj i ⟶ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (app { val := i + 1, isLt := ⋯ }) = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := ⋯ }) (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi)) : 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 = { app := app, naturality := ⋯ }

@[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.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (app { val := i + 1, isLt := ⋯ }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := ⋯ }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi)) : (CategoryTheory.ComposableArrows.isoMk app w).inv = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).inv) ⋯

@[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.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (app { val := i + 1, isLt := ⋯ }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := ⋯ }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi)) : (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.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (app { val := i + 1, isLt := ⋯ }).hom = CategoryTheory.CategoryStruct.comp (app { val := i, isLt := ⋯ }).hom (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi)) : 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.obj i = G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' G i (i + 1) ⋯ hi) (CategoryTheory.eqToHom ⋯))) : 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

• CategoryTheory.ComposableArrows.homMk₀ f = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (0 + 1)) => match i with | { val := 0, isLt := isLt } => f) ⋯

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 = { hom := CategoryTheory.ComposableArrows.homMk₀ e.hom, inv := CategoryTheory.ComposableArrows.homMk₀ e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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.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 w).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 w).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 w).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

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

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 ⋯))) : 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 ⋯ = 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 ⋯ = F.map (CategoryTheory.CategoryStruct.id { val := 0, isLt := ⋯ })

@[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 ⋯ = 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 := ⋯ } ⋯ = 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 } ⋯ = 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 } ⋯ = 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 ⋯ = 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 ⋯ = 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).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).map g = CategoryTheory.ComposableArrows.Precomp.map F f 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 Φ).obj X = F.obj (Φ.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 Φ).map f = F.map (Φ.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 Φ).map f).app X_1 = f.app (Φ.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 Φ).obj F).obj X = F.obj (Φ.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 Φ).obj F).map f = F.map (Φ.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).obj i = Fin.succ i

@[simp]

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

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

• Fin.succFunctor n = { toPrefunctor := { obj := fun (i : Fin n) => Fin.succ i, map := fun {i j : Fin n} (hij : i ⟶ j) => CategoryTheory.homOfLE ⋯ }, map_id := ⋯, map_comp := ⋯ }

@[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.obj F).map f = F.map (CategoryTheory.homOfLE ⋯)

@[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.obj F).obj X = F.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.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.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).map hij = hij

@[simp]

theorem Fin.castSuccFunctor_obj (n : ℕ) (i : Fin n) : (Fin.castSuccFunctor n).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 = { toPrefunctor := { obj := fun (i : Fin n) => Fin.castSucc i, map := fun {X Y : Fin n} (hij : X ⟶ Y) => hij }, map_id := ⋯, map_comp := ⋯ }

@[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.obj F).map f = F.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.obj F).obj X = F.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.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.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.map f = CategoryTheory.ComposableArrows.δ₀Functor.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 ⋯

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 ⋯))) : 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₁) 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 := ⋯ } = 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 ⋯ ⋯

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 ⋯))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) : 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 := ⋯ } = 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 := ⋯ } = 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 ⋯ ⋯ ⋯

@[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 ⋯))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) : 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 := ⋯ } = 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 := ⋯ } = 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 := ⋯ } = 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) h ≅ CategoryTheory.ComposableArrows.obj' g (n + 1) h) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' f n (n + 1) ⋯ h) app'.hom = CategoryTheory.CategoryStruct.comp app.hom (CategoryTheory.ComposableArrows.map' g n (n + 1) ⋯ h)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g n (n + 1) ⋯ h) app'.inv = CategoryTheory.CategoryStruct.comp app.inv (CategoryTheory.ComposableArrows.map' f n (n + 1) ⋯ h)

@[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 ⋯ ⋯ ⋯ ⋯

@[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 ⋯))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₃ : CategoryTheory.ComposableArrows.map' f 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) : 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 := ⋯ } = 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 := ⋯ } = 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 := ⋯ } = 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 := ⋯ } = 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 ⋯ ⋯ ⋯ ⋯ ⋯

@[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 ⋯))) (w₁ : CategoryTheory.ComposableArrows.map' f 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₂ : CategoryTheory.ComposableArrows.map' f 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₃ : CategoryTheory.ComposableArrows.map' f 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 3 4 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) (w₄ : CategoryTheory.ComposableArrows.map' f 4 5 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' g 4 5 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))) : 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 hi = CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi)

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.obj i ≅ obj i), ∀ (i : ℕ) (hi : i < n), mapSucc { val := i, isLt := hi } = CategoryTheory.CategoryStruct.comp (e { val := i, isLt := ⋯ }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' F i (i + 1) ⋯ hi) (e { val := i + 1, isLt := ⋯ }).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

• CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc = CategoryTheory.Functor.copyObj (Exists.choose ⋯) obj (Exists.choose ⋯)

@[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).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) ⋯ hi = 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 hi = 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).obj F).map f = G.map (F.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).map α).app X_1 = G.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).obj F).obj X = G.obj (F.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).obj G