English
The shift functor on triangles is defined by shifting objects and multiplying morphisms by (-1)^n, giving a functor of triangles.
Русский
Сдвиговая величина на треугольниках задается сдвигом объектов и умножением морфизмов на (-1)^n, образуя функтор треугольников.
LaTeX
$$$\\text{def } \\text{shiftFunctor}: \\ Triangle\\ C \\to Triangle\\ C \\text{ by } n \\mapsto (\\text{morphisms multiplied by } (-1)^n, \\text{objects shifted by } n).$$$
Lean4
/-- The shift functor `Triangle C ⥤ Triangle C` by `n : ℤ` sends a triangle
to the triangle obtained by shifting the objects by `n` in `C` and by
multiplying the three morphisms by `(-1)^n`. -/
@[simps]
noncomputable def shiftFunctor (n : ℤ) : Triangle C ⥤ Triangle C
where
obj
T :=
Triangle.mk (n.negOnePow • T.mor₁⟦n⟧') (n.negOnePow • T.mor₂⟦n⟧')
(n.negOnePow • T.mor₃⟦n⟧' ≫ (shiftFunctorComm C 1 n).hom.app T.obj₁)
map
f :=
{ hom₁ := f.hom₁⟦n⟧'
hom₂ := f.hom₂⟦n⟧'
hom₃ := f.hom₃⟦n⟧'
comm₁ := by
dsimp
simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₁]
comm₂ := by
dsimp
simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₂]
comm₃ := by
dsimp
rw [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp_assoc, ← f.comm₃, Functor.map_comp,
assoc, assoc]
erw [(shiftFunctorComm C 1 n).hom.naturality]
rfl }
