English
Consider a commutative diagram of functors with squares e12, e23, e13 and a shift by A; if e13 is determined by α, e23, e12, and β as in the statement, then the outer square e13 commutes with the shift when α, e23, e12, β do. This is the formal vertical composition principle for CommShift.
Русский
Рассмотрим рисунок из квадратов функторов, где горизонтальные и вертикальные связи образуют сдвиги по A; если внешний квадрат e13 задан через α, e23, e12, β, то этот внешний квадрат коммути сдвигами, если соответствуют условиям на α, e23, e12, β.
LaTeX
$$$e_{13} = Functor.whiskerRight α L_3 \\; \\circ \\; (Functor.associator _ _ _).hom \\; \\circ \\; \\mathrm{whiskerLeft} F_{12} e_{23} \\circ (Functor.associator _ _ _).inv \\circ \\mathrm{whiskerRight} e_{12} G_23 \\circ (Functor.associator _ _ _).hom \\circ \\mathrm{whiskerLeft} L_1 β$$$
Lean4
/-- Assume that we have a diagram of categories
```
C₁ ⥤ D₁
‖ ‖
v v
C₂ ⥤ D₂
‖ ‖
v v
C₃ ⥤ D₃
```
with functors `F₁₂ : C₁ ⥤ C₂`, `F₂₃ : C₂ ⥤ C₃` and `F₁₃ : C₁ ⥤ C₃` on the first
column that are related by a natural transformation `α : F₁₃ ⟶ F₁₂ ⋙ F₂₃`
and similarly `β : G₁₂ ⋙ G₂₃ ⟶ G₁₃` on the second column. Assume that we have
natural transformations
`e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂` (top square), `e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃` (bottom square),
and `e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃` (outer square), where the horizontal functors
are denoted `L₁`, `L₂` and `L₃`. Assume that `e₁₃` is determined by the other
natural transformations `α`, `e₂₃`, `e₁₂` and `β`. Then, if all these categories
are equipped with a shift by an additive monoid `A`, and all these functors commute with
these shifts, then the natural transformation `e₁₃` of the outer square commutes with the
shift if all `α`, `e₂₃`, `e₁₂` and `β` do. -/
theorem verticalComposition {C₁ C₂ C₃ D₁ D₂ D₃ : Type*} [Category C₁] [Category C₂] [Category C₃] [Category D₁]
[Category D₂] [Category D₃] {F₁₂ : C₁ ⥤ C₂} {F₂₃ : C₂ ⥤ C₃} {F₁₃ : C₁ ⥤ C₃} (α : F₁₃ ⟶ F₁₂ ⋙ F₂₃) {G₁₂ : D₁ ⥤ D₂}
{G₂₃ : D₂ ⥤ D₃} {G₁₃ : D₁ ⥤ D₃} (β : G₁₂ ⋙ G₂₃ ⟶ G₁₃) {L₁ : C₁ ⥤ D₁} {L₂ : C₂ ⥤ D₂} {L₃ : C₃ ⥤ D₃}
(e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂) (e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃) (e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃) (A : Type*) [AddMonoid A]
[HasShift C₁ A] [HasShift C₂ A] [HasShift C₃ A] [HasShift D₁ A] [HasShift D₂ A] [HasShift D₃ A] [F₁₂.CommShift A]
[F₂₃.CommShift A] [F₁₃.CommShift A] [CommShift α A] [G₁₂.CommShift A] [G₂₃.CommShift A] [G₁₃.CommShift A]
[CommShift β A] [L₁.CommShift A] [L₂.CommShift A] [L₃.CommShift A] [CommShift e₁₂ A] [CommShift e₂₃ A]
(h₁₃ :
e₁₃ =
Functor.whiskerRight α L₃ ≫
(Functor.associator _ _ _).hom ≫
Functor.whiskerLeft F₁₂ e₂₃ ≫
(Functor.associator _ _ _).inv ≫
Functor.whiskerRight e₁₂ G₂₃ ≫ (Functor.associator _ _ _).hom ≫ Functor.whiskerLeft L₁ β) :
CommShift e₁₃ A := by
subst h₁₃
infer_instance
