English
For any ring R, the shift functor on the Homotopy category induced by up-graded complexes is an R-linear functor.
Русский
Для любой кольцевой области R сдвиговый функтор над гомотопической категорией индуцируется как R-линейный функтор.
LaTeX
$$$\\forall R\\;[Ring\\;R]\\;\\text{and}\\; C,\\; (\\mathrm{shiftFunctor} (\\mathrm{HomotopyCategory} (C, \\mathrm{ComplexShape.up} \\mathbb{Z}))\\; n)\\in \\mathrm{Functor.Linear}\\,R\\,C$$$
Lean4
instance {R : Type*} [Ring R] [CategoryTheory.Linear R C] (n : ℤ) :
(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Linear R where
map_smul := by
rintro ⟨X⟩ ⟨Y⟩ f r
obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective f
have h₁ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) f
have h₂ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) (r • f)
dsimp at h₁ h₂
rw [← Functor.map_smul, ← h₁, ← h₂]
simp
