instAdditiveOppositeShiftFunctorInt

English

Shifts on opposite category are additive given additive structure on original category.

Русский

Сдвиги в противоположной категории адаптированы к аддитивной структуре исходной категории.

LaTeX

$$$(\text{shiftFunctor } C^\mathrm{op} n)\text{ is additive }$$$

Lean4

instance [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] (n : ℤ) : (shiftFunctor Cᵒᵖ n).Additive :=
  (inferInstance : (shiftFunctor (OppositeShiftAux C) n).Additive)

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