instPreservesZeroMorphismsShift — Mathlib

English

Let F : C ⥤ A be a functor between categories with a shift sequence indexed by a monoid M, such that every shift functor (C, n) preserves zero morphisms and F preserves zero morphisms. Then for every n ∈ M, the shifted functor F.shift n = F ∘ shift_C(n) preserves zero morphisms.

Русский

Пусть F: C ⥤ A — функтор между категориями, у которых есть последовательность сдвигов индексируемая моноидом M, причём каждый сдвиговый функтор (C, n) сохраняет нулевые морфизмы, и F сохраняет нулевые морфизмы. Тогда для каждого n ∈ M обращение F.shift n = F ∘ shift_C(n) сохраняет нулевые морфизмы.

LaTeX

$$$\\forall n \\in M\\;\\forall X,Y,\\ f:X\\to Y,\\ f=0 \\Rightarrow (F \\circ \\mathrm{shift}_C(n))(f) = 0$$$

Lean4

instance (n : M) : (F.shift n).PreservesZeroMorphisms :=
  preservesZeroMorphisms_of_iso (F.isoShift n)

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