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
asComposableArrow C 1
? - construct some elements in
ComposableArrows m (Fin (n + 1))
for smalln
the precomposition with which shall induce functorsComposableArrows C n ⥤ ComposableArrows C m
which correspond to simplicial operations (specifically faces) with good definitional properties (this might be necessary for up ton = 7
in 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_option
s are required at all
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
The i
th object (with i : ℕ
such that i ≤ n
) of F : ComposableArrows C n
.
Equations
- F.obj' i hi = F.obj ⟨i, ⋯⟩
Instances For
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
The leftmost object of F : ComposableArrows C n
.
Equations
- F.left = F.obj' 0 ⋯
Instances For
The rightmost object of F : ComposableArrows C n
.
Equations
- F.right = F.obj' n ⋯
Instances For
The canonical map F.left ⟶ F.right
for F : ComposableArrows C n
.
Equations
- F.hom = F.map' 0 n ⋯ ⋯
Instances For
The map F.obj' i ⟶ G.obj' i
induced on i
th 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
Constructor for ComposableArrows C 0
.
Equations
- CategoryTheory.ComposableArrows.mk₀ X = (CategoryTheory.Functor.const (Fin 1)).obj X
Instances For
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
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
Constructor for ComposableArrows C 1
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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
Constructor for morphisms in ComposableArrows C 1
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for isomorphisms in ComposableArrows C 1
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
"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
Constructor for ComposableArrows C 2
.
Equations
- CategoryTheory.ComposableArrows.mk₂ f g = (CategoryTheory.ComposableArrows.mk₁ g).precomp f
Instances For
Constructor for ComposableArrows C 3
.
Equations
- CategoryTheory.ComposableArrows.mk₃ f g h = (CategoryTheory.ComposableArrows.mk₂ g h).precomp f
Instances For
Constructor for ComposableArrows C 4
.
Equations
- CategoryTheory.ComposableArrows.mk₄ f g h i = (CategoryTheory.ComposableArrows.mk₃ g h i).precomp f
Instances For
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.
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
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
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 {i j : Fin n} (hij : i ⟶ j) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
Instances For
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
The ComposableArrows C n
obtained by forgetting the first arrow.
Equations
- F.δ₀ = CategoryTheory.ComposableArrows.δ₀Functor.obj F
Instances For
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
The ComposableArrows C n
obtained by forgetting the first arrow.
Equations
- F.δlast = CategoryTheory.ComposableArrows.δlastFunctor.obj F
Instances For
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
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
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
Constructor for isomorphisms in ComposableArrows C 2
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Constructor for isomorphisms in ComposableArrows C 3
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for morphisms in ComposableArrows C 4
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for isomorphisms in ComposableArrows C 4
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for morphisms in ComposableArrows C 5
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for isomorphisms in ComposableArrows C 5
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i
th arrow of F : ComposableArrows C n
.
Equations
- F.arrow i hi = CategoryTheory.ComposableArrows.mk₁ (F.map' i (i + 1) ⋯ hi)
Instances For
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
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
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
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)