instCommShiftIntUpMapHomotopyCategory

English

The Int-indexed shift by integers is linear: the shift functor by n ∈ Int is additive and R-linear for any ring R with a linear structure on C.

Русский

Сдвиг по целочисленному индексу Int линейный: функтор сдвига на n ∈ Int аддитивен и линейный над R для любой кольцевой структуры на C.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; \\text{the }(\\mathrm{shiftFunctor}\\; (\\mathrm{HomotopyCategory} (C, \\mathrm{ComplexShape.up} \\mathbb{Z}))\\, n)\\; \\text{is } R\\text{-linear}$$$

Lean4

noncomputable instance : (F.mapHomotopyCategory (ComplexShape.up ℤ)).CommShift ℤ :=
  Quotient.liftCommShift _ _ _ _

Похожие утверждения