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):
- 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 the offending simprocs in this file.
However, hopefully it is possible to refactor the material here so that no disabling of simprocs is needed.
See issue #27382.
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
.
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
.
Instances For
The rightmost object of F : ComposableArrows C n
.
Instances For
The canonical map F.left ⟶ F.right
for F : ComposableArrows C 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
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
Instances For
Constructor for ComposableArrows C 3
.
Equations
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 ComposableArrows C (n + 1) ⥤ ComposableArrows C n
which forgets
the first arrow.
Equations
Instances For
The ComposableArrows C n
obtained by forgetting the first arrow.
Equations
Instances For
The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n
which forgets
the last arrow.
Equations
Instances For
The ComposableArrows C n
obtained by forgetting the first arrow.
Equations
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.Functor.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
.