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 CasComposableArrow C 1? - construct some elements in
ComposableArrows m (Fin (n + 1))for smallnthe precomposition with which shall induce functorsComposableArrows C n ⥤ ComposableArrows C mwhich correspond to simplicial operations (specifically faces) with good definitional properties (this might be necessary for up ton = 7in order to formalize spectral sequences following Verdier)
New simprocs that run even in dsimp have caused breakages in this file.
(e.g. dsimp can now simplify 2 + 3 to 5)
For now, we just turn off simprocs in this file.
We'll soon provide finer grained options here, e.g. to turn off simprocs only in dsimp, etc.
However, hopefully it is possible to refactor the material here so that no backwards compatibility
set_options are required at all
@[reducible, inline]
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
Instances For
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)
Instances For
@[reducible, inline]
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
- F.obj' i hi = F.obj ⟨i, ⋯⟩
Instances For
@[reducible, inline]
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 ⟨i, ⋯⟩ ⟶ F.obj ⟨j, ⋯⟩
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
- F.map' i j hij hjn = F.map (CategoryTheory.homOfLE ⋯)
Instances For
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✝)
:
F.map' i i ⋯ hi = CategoryTheory.CategoryStruct.id (F.obj ⟨i, ⋯⟩)
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✝)
:
F.map' i k ⋯ hk = CategoryTheory.CategoryStruct.comp (F.map' i j hij ⋯) (F.map' j k hjk hk)
@[reducible, inline]
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
- F.left = F.obj' 0 ⋯
Instances For
@[reducible, inline]
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
- F.right = F.obj' n ⋯
Instances For
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
(F : CategoryTheory.ComposableArrows C n)
:
F.left ⟶ F.right
The canonical map F.left ⟶ F.right for F : ComposableArrows C n.
Equations
- F.hom = F.map' 0 n ⋯ ⋯
Instances For
@[reducible, inline]
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✝)
:
F.obj' i hi ⟶ G.obj' 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 ⟨i, ⋯⟩
Instances For
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 (F.map' i j hij hj) (CategoryTheory.ComposableArrows.app' φ j hj) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯) (G.map' i j hij hj)
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 : G.obj' j hj ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map' i j hij hj)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ j hj) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯)
(CategoryTheory.CategoryStruct.comp (G.map' i j hij hj) h)
def
CategoryTheory.ComposableArrows.mk₀
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(X : C)
:
Constructor for ComposableArrows C 0.
Equations
- CategoryTheory.ComposableArrows.mk₀ X = (CategoryTheory.Functor.const (Fin 1)).obj X
Instances For
@[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
@[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
The map which sends 0 : Fin 2 to X₀ and 1 to X₁.
Equations
- CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨0, isLt⟩ = X₀
- CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨1, isLt⟩ = X₁
Instances For
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
- CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨0, isLt⟩)
- CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f
- CategoryTheory.ComposableArrows.Mk₁.map f ⟨1, isLt⟩ ⟨1, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨1, isLt⟩)
Instances For
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)
:
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)
:
def
CategoryTheory.ComposableArrows.mk₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X₀ : C}
{X₁ : C}
(f : X₀ ⟶ X₁)
:
Constructor for ComposableArrows C 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.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.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 (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' 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 := ⋯ }
Instances For
@[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 (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi))
(i : Fin (n + 1))
:
(CategoryTheory.ComposableArrows.homMk app w).app i = app i
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 (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' 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.
Instances For
@[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 (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' 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 (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi))
:
(CategoryTheory.ComposableArrows.isoMk app w).hom = CategoryTheory.ComposableArrows.homMk (fun (i : Fin (n + 1)) => (app i).hom) w
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),
F.map' i (i + 1) ⋯ hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map' i (i + 1) ⋯ hi) (CategoryTheory.eqToHom ⋯)))
:
F = G
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 : F.obj' 0 ⋯ ⟶ G.obj' 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 | ⟨0, isLt⟩ => f) ⋯
Instances For
@[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 : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(i : Fin (0 + 1))
:
(CategoryTheory.ComposableArrows.homMk₀ f).app i = match i with
| ⟨0, 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 ⋯)
:
φ = φ'
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 : F.obj' 0 ⋯ ≅ G.obj' 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 := ⋯ }
Instances For
@[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 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(i : Fin (0 + 1))
:
(CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i = match i with
| ⟨0, isLt⟩ => e.inv
@[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 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(i : Fin (0 + 1))
:
(CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i = match i with
| ⟨0, isLt⟩ => e.hom
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 : F.obj' 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
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 : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(right : F.obj' 1 ⋯ ⟶ G.obj' 1 ⋯)
(w : autoParam
(CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right = CategoryTheory.CategoryStruct.comp left (G.map' 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.
Instances For
@[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 : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(right : F.obj' 1 ⋯ ⟶ G.obj' 1 ⋯)
(w : autoParam
(CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right = CategoryTheory.CategoryStruct.comp left (G.map' 0 1 ⋯ ⋯))
_auto✝)
(i : Fin (1 + 1))
:
(CategoryTheory.ComposableArrows.homMk₁ left right w).app i = match i with
| ⟨0, isLt⟩ => left
| ⟨1, isLt⟩ => right
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 ⋯)
:
φ = φ'
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 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯)
(w : autoParam
(CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 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.
Instances For
@[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 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯)
(w : autoParam
(CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 ⋯ ⋯))
_auto✝)
(i : Fin (1 + 1))
:
(CategoryTheory.ComposableArrows.isoMk₁ left right w).inv.app i = match i with
| ⟨0, isLt⟩ => left.inv
| ⟨1, isLt⟩ => right.inv
@[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 : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯)
(w : autoParam
(CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 ⋯ ⋯))
_auto✝)
(i : Fin (1 + 1))
:
(CategoryTheory.ComposableArrows.isoMk₁ left right w).hom.app i = match i with
| ⟨0, isLt⟩ => left.hom
| ⟨1, isLt⟩ => right.hom
theorem
CategoryTheory.ComposableArrows.map'_eq_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(F : CategoryTheory.ComposableArrows C 1)
:
F.map' 0 1 ⋯ ⋯ = F.hom
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 : F.left = G.left)
(right : F.right = G.right)
(w : F.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom left)
(CategoryTheory.CategoryStruct.comp G.hom (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)
:
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 ⟨0, isLt⟩ = X
- CategoryTheory.ComposableArrows.Precomp.obj F X ⟨i.succ, hi⟩ = F.obj' i ⋯
Instances For
@[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)
:
@[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 = F.obj' 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 ⟨i + 1, hi⟩ = F.obj' 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 ⟶ F.left)
(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
- CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id X
- CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f
- CategoryTheory.ComposableArrows.Precomp.map F f ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x_3 = CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
- CategoryTheory.ComposableArrows.Precomp.map F f ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij = F.map' i j ⋯ ⋯
Instances For
@[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 ⟶ F.left)
:
@[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 ⟶ F.left)
:
CategoryTheory.ComposableArrows.Precomp.map F f 1 1 ⋯ = F.map (CategoryTheory.CategoryStruct.id ⟨0, ⋯⟩)
@[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 ⟶ F.left)
:
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 ⟶ F.left)
:
CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨0 + 1, ⋯⟩ ⋯ = f
@[simp]
theorem
CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
(F : CategoryTheory.ComposableArrows C n)
{X : C}
(f : X ⟶ F.left)
(j : ℕ)
(hj : j + 2 < n + 1 + 1)
:
CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨j + 2, hj⟩ ⋯ = CategoryTheory.CategoryStruct.comp f (F.map' 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 ⟶ F.left)
(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 ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' 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 ⟶ F.left)
(j : ℕ)
(hj : j + 1 < n + 1 + 1)
:
CategoryTheory.ComposableArrows.Precomp.map F f 1 ⟨j + 1, hj⟩ ⋯ = F.map' 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 ⟶ F.left)
(i : Fin (n + 1 + 1))
:
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 ⟶ F.left)
{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)
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 ⟶ F.left)
:
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.
Instances For
@[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 ⟶ F.left)
:
@[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 ⟶ F.left)
:
∀ (a : Fin (n + 1 + 1)), (F.precomp f).obj a = CategoryTheory.ComposableArrows.Precomp.obj F X a
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₂)
:
Constructor for ComposableArrows C 2.
Equations
- CategoryTheory.ComposableArrows.mk₂ f g = (CategoryTheory.ComposableArrows.mk₁ g).precomp f
Instances For
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₃)
:
Constructor for ComposableArrows C 3.
Equations
- CategoryTheory.ComposableArrows.mk₃ f g h = (CategoryTheory.ComposableArrows.mk₂ g h).precomp f
Instances For
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₄)
:
Constructor for ComposableArrows C 4.
Equations
- CategoryTheory.ComposableArrows.mk₄ f g h i = (CategoryTheory.ComposableArrows.mk₃ g h i).precomp f
Instances For
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₅)
:
Constructor for ComposableArrows C 5.
Equations
- CategoryTheory.ComposableArrows.mk₅ f g h i j = (CategoryTheory.ComposableArrows.mk₄ g h i j).precomp f
Instances For
These examples are meant to test the good definitional properties of precomp,
and that dsimp can see through.
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)))
:
The map ComposableArrows C m → ComposableArrows C n obtained by precomposition with
a functor Fin (n + 1) ⥤ Fin (m + 1).
Equations
- F.whiskerLeft Φ = Φ.comp F
Instances For
@[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)))
:
@[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))
:
(F.whiskerLeft Φ).obj X = F.obj (Φ.obj X)
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)))
:
The functor ComposableArrows C m ⥤ ComposableArrows C n obtained by precomposition with
a functor Fin (n + 1) ⥤ Fin (m + 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
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)
The functor Fin n ⥤ Fin (n + 1) which sends i to i.succ.
Equations
- Fin.succFunctor n = { obj := fun (i : Fin n) => i.succ, map := fun {x x_1 : Fin n} (hij : x ⟶ x_1) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
Instances For
@[simp]
theorem
Fin.succFunctor_map
(n : ℕ)
:
∀ {x x_1 : Fin n} (hij : x ⟶ x_1), (Fin.succFunctor n).map hij = CategoryTheory.homOfLE ⋯
def
CategoryTheory.ComposableArrows.δ₀Functor
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 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))
Instances For
@[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 X.succ
@[simp]
theorem
CategoryTheory.ComposableArrows.δ₀Functor_map_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
:
@[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 ⋯)
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.δ₀
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
(F : CategoryTheory.ComposableArrows C (n + 1))
:
The ComposableArrows C n obtained by forgetting the first arrow.
Equations
- F.δ₀ = CategoryTheory.ComposableArrows.δ₀Functor.obj F
Instances For
@[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 ⟶ F.left)
:
(F.precomp f).δ₀ = F
@[simp]
@[simp]
theorem
Fin.castSuccFunctor_map
(n : ℕ)
:
∀ {X Y : Fin n} (hij : X ⟶ Y), (Fin.castSuccFunctor n).map hij = hij
def
CategoryTheory.ComposableArrows.δlastFunctor
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 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))
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.δlastFunctor_map_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
:
@[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))
:
@[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 X.castSucc
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.δlast
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
(F : CategoryTheory.ComposableArrows C (n + 1))
:
The ComposableArrows C n obtained by forgetting the first arrow.
Equations
- F.δlast = CategoryTheory.ComposableArrows.δlastFunctor.obj F
Instances For
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)}
(α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(β : F.δ₀ ⟶ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β 0 ⋯) = CategoryTheory.CategoryStruct.comp α (G.map' 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.
Instances For
@[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)}
(α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(β : F.δ₀ ⟶ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β 0 ⋯) = CategoryTheory.CategoryStruct.comp α (G.map' 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)}
(α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯)
(β : F.δ₀ ⟶ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β 0 ⋯) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 ⋯ ⋯))
(i : ℕ)
(hi : i + 1 < n + 1 + 1)
:
(CategoryTheory.ComposableArrows.homMkSucc α β w).app ⟨i + 1, 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
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)}
(α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(β : F.δ₀ ≅ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 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.
Instances For
@[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)}
(α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(β : F.δ₀ ≅ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.isoMkSucc α β w).inv = CategoryTheory.ComposableArrows.homMkSucc α.inv β.inv ⋯
@[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)}
(α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯)
(β : F.δ₀ ≅ G.δ₀)
(w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.isoMkSucc α β w).hom = CategoryTheory.ComposableArrows.homMkSucc α.hom β.hom w
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₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯)
(h : F.δ₀ = G.δ₀)
(w : F.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
(CategoryTheory.CategoryStruct.comp (G.map' 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₀ ⟶ F₀.left), F = F₀.precomp 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 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₀
Instances For
@[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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, ⋯⟩ = 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 ⋯)
:
φ = φ'
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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
:
f ≅ g
Constructor for isomorphisms in ComposableArrows C 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv ⋯ ⋯
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₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯)
(h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯)
(h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯)
(w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
(CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
(CategoryTheory.CategoryStruct.comp (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 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₀
Instances For
@[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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨2, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨3, ⋯⟩ = 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 ⋯)
:
φ = φ'
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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
:
f ≅ g
Constructor for isomorphisms in ComposableArrows C 3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 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₂
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₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯)
(h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯)
(h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯)
(h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯)
(w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
(CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
(CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
(CategoryTheory.CategoryStruct.comp (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
:
f ⟶ g
Constructor for morphisms in ComposableArrows C 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.homMk₄_app_zero
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{f : CategoryTheory.ComposableArrows C 4}
{g : CategoryTheory.ComposableArrows C 4}
(app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨2, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨3, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨4, ⋯⟩ = 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 : f.obj' n ⋯ ≅ g.obj' n ⋯)
(app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h)
(w : CategoryTheory.CategoryStruct.comp (f.map' n (n + 1) ⋯ h) app'.hom = CategoryTheory.CategoryStruct.comp app.hom (g.map' n (n + 1) ⋯ h))
:
CategoryTheory.CategoryStruct.comp (g.map' n (n + 1) ⋯ h) app'.inv = CategoryTheory.CategoryStruct.comp app.inv (f.map' n (n + 1) ⋯ h)
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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯))
:
f ≅ g
Constructor for isomorphisms in ComposableArrows C 4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 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₃
@[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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 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 ⋯ ⋯ ⋯ ⋯
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₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯)
(h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯)
(h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯)
(h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯)
(h₄ : f.obj' 4 ⋯ = g.obj' 4 ⋯)
(w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
(CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
(CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
(CategoryTheory.CategoryStruct.comp (g.map' 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₃ : f.map' 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃)
(CategoryTheory.CategoryStruct.comp (g.map' 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)
:
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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯))
:
f ⟶ g
Constructor for morphisms in ComposableArrows C 5.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.homMk₅_app_zero
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{f : CategoryTheory.ComposableArrows C 5}
{g : CategoryTheory.ComposableArrows C 5}
(app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨2, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨3, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, ⋯⟩ = 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₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯))
:
(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨5, ⋯⟩ = 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 ⋯)
:
φ = φ'
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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 4 5 ⋯ ⋯))
:
f ≅ g
Constructor for isomorphisms in ComposableArrows C 5.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 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₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯)
(app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯)
(app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯)
(app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯)
(app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯)
(app₅ : f.obj' 5 ⋯ ≅ g.obj' 5 ⋯)
(w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯))
(w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯))
(w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯))
(w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯))
(w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅.hom = CategoryTheory.CategoryStruct.comp app₄.hom (g.map' 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₄
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₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯)
(h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯)
(h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯)
(h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯)
(h₄ : f.obj' 4 ⋯ = g.obj' 4 ⋯)
(h₅ : f.obj' 5 ⋯ = g.obj' 5 ⋯)
(w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
(CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
(CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
(CategoryTheory.CategoryStruct.comp (g.map' 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₃ : f.map' 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃)
(CategoryTheory.CategoryStruct.comp (g.map' 3 4 ⋯ ⋯) (CategoryTheory.eqToHom ⋯)))
(w₄ : f.map' 4 5 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₄)
(CategoryTheory.CategoryStruct.comp (g.map' 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)
:
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✝)
:
The ith arrow of F : ComposableArrows C n.
Equations
- F.arrow i hi = CategoryTheory.ComposableArrows.mk₁ (F.map' i (i + 1) ⋯ hi)
Instances For
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 i.castSucc ⟶ obj i.succ)
:
∃ (F : CategoryTheory.ComposableArrows C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i),
∀ (i : ℕ) (hi : i < n),
mapSucc ⟨i, hi⟩ = CategoryTheory.CategoryStruct.comp (e ⟨i, ⋯⟩).inv
(CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (e ⟨i + 1, ⋯⟩).hom)
noncomputable def
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{n : ℕ}
(obj : Fin (n + 1) → C)
(mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ)
:
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 ⋯.choose obj ⋯.choose
Instances For
@[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 i.castSucc ⟶ obj i.succ)
(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 i.castSucc ⟶ obj i.succ)
(i : ℕ)
(hi : autoParam (i < n) _auto✝)
:
(CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, 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 i.castSucc ⟶ obj i.succ)
(i : ℕ)
(hi : autoParam (i < n) _auto✝)
:
(CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).arrow i hi = CategoryTheory.ComposableArrows.mk₁ (mapSucc ⟨i, hi⟩)
noncomputable def
CategoryTheory.ComposableArrows.opEquivalence
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
:
The equivalence (ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n obtained
by reversing the arrows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_inverse_obj
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : CategoryTheory.ComposableArrows Cᵒᵖ n)
:
(CategoryTheory.ComposableArrows.opEquivalence C n).inverse.obj X = Opposite.op
((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).comp
(CategoryTheory.Functor.leftOp X))
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_functor_map_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
:
∀ {X Y : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ} (f : X ⟶ Y) (x : Fin (n + 1)),
((CategoryTheory.ComposableArrows.opEquivalence C n).functor.map f).app x = (f.unop.app x.rev).op
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
(X : Fin (n + 1))
:
((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X✝).obj X = Opposite.op ((Opposite.unop X✝).obj X.rev)
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : CategoryTheory.ComposableArrows Cᵒᵖ n)
(X : Fin (n + 1))
:
((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.hom.app X✝).app X = X✝.map
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counitInv.app
(Opposite.op X)).unop
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
:
∀ {X_1 Y : Fin (n + 1)} (f : X_1 ⟶ Y),
((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).map f = ((Opposite.unop X).map (⋯.functor.map (CategoryTheory.homOfLE ⋯))).op
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
:
(CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp
(CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor)
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp
(Opposite.unop X)).rightOpLeftOpIso.inv).op
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc
(Opposite.unop X)).inv.op
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_inverse_map
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
:
∀ {X Y : CategoryTheory.ComposableArrows Cᵒᵖ n} (f : X ⟶ Y),
(CategoryTheory.ComposableArrows.opEquivalence C n).inverse.map f = (CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor)
(CategoryTheory.NatTrans.leftOp f)).op
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : CategoryTheory.ComposableArrows Cᵒᵖ n)
(X : Fin (n + 1))
:
((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.inv.app X✝).app X = X✝.map
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counit.app
(Opposite.op X)).unop
@[simp]
theorem
CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(n : ℕ)
(X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
:
(CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc
(Opposite.unop X)).hom.op
(CategoryTheory.whiskerLeft (⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor)
(((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp
(Opposite.unop X)).rightOpLeftOpIso.hom).op
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 : ℕ)
:
The functor ComposableArrows C n ⥤ ComposableArrows D n obtained by postcomposition
with a functor C ⥤ D.
Equations
- G.mapComposableArrows n = (CategoryTheory.whiskeringRight (Fin (n + 1)) C D).obj G
Instances For
@[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 : ℕ)
:
@[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))
:
((G.mapComposableArrows n).obj F).obj X = G.obj (F.obj X)
@[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)
:
noncomputable def
CategoryTheory.Functor.mapComposableArrowsOpIso
{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 : ℕ)
:
(G.mapComposableArrows n).comp (CategoryTheory.ComposableArrows.opEquivalence D n).functor.rightOp ≅ (CategoryTheory.ComposableArrows.opEquivalence C n).functor.rightOp.comp (G.op.mapComposableArrows n).op
The functor ComposableArrows C n ⥤ ComposableArrows D n induced by G : C ⥤ D
commutes with opEquivalence.
Equations
- G.mapComposableArrowsOpIso n = CategoryTheory.Iso.refl ((G.mapComposableArrows n).comp (CategoryTheory.ComposableArrows.opEquivalence D n).functor.rightOp)