cyclesMap_zero — Mathlib

English

For any two HomologicalComplex objects K and L connected by a morphism, the induced map on cycles sends the zero morphism at index i to the zero morphism there.

Русский

Для двух гомологических комплексов K и L, связанных морфизмом, индуцированное отображение на циклах отправляет нулевой морфизм в позиции i в нулевой морфизм.

LaTeX

$$$$ \\, \\mathrm{cyclesMap}(0,i) = 0 $$$$

Lean4

@[simp]
theorem cyclesMap_zero : cyclesMap (0 : K ⟶ L) i = 0 :=
  ShortComplex.cyclesMap_zero _ _

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