English
If a, b, n are integers with a + b = n, there is a canonical isomorphism between triangle shift functors: Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b.
Русский
Пусть a, b, n ∈ ℤ и a + b = n. Тогда существует каноническое изоморождение между сдвигами треугольников: Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b.
LaTeX
$$$\\operatorname{Iso}(\\operatorname{Triangle.shiftFunctor} \\, C \\, n, \\operatorname{Triangle.shiftFunctor} \\, C \\, a \\circ \\operatorname{Triangle.shiftFunctor} \\, C \\, b)$ при $a + b = n$$$
Lean4
/-- The canonical isomorphism
`Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b`
when `a + b = n`. -/
@[simps!]
noncomputable def shiftFunctorAdd' (a b n : ℤ) (h : a + b = n) :
Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b :=
NatIso.ofComponents
(fun T =>
Triangle.isoMk _ _ ((CategoryTheory.shiftFunctorAdd' C a b n h).app _)
((CategoryTheory.shiftFunctorAdd' C a b n h).app _) ((CategoryTheory.shiftFunctorAdd' C a b n h).app _)
(by
subst h
dsimp
rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm])
(by
subst h
dsimp
rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm])
(by
subst h
dsimp
rw [Linear.units_smul_comp, Linear.comp_units_smul, Functor.map_units_smul, Linear.units_smul_comp,
Linear.comp_units_smul, smul_smul, assoc, Functor.map_comp, assoc]
erw [← NatTrans.naturality_assoc]
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add,
shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a]))
(by cat_disch)
