map_homogical_complex_additive — Mathlib

English

If F is additive, then the induced map on maps of homological complexes is additive: (F.mapHomologicalComplex c).map(f+g) = (F.mapHomologicalComplex c).map f + (F.mapHomologicalComplex c).map g.

Русский

Если F аддитивен, то отображение на отображениях гомологических комплексов сохраняет сложение: map(f+g) = map f + map g.

LaTeX

$$$\big( (F.mapHomologicalComplex c).map(f+g) \big) = \big( (F.mapHomologicalComplex c).map f \big) + \big( (F.mapHomologicalComplex c).map g \big)$$$

Lean4

instance map_homogical_complex_additive (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
    (F.mapHomologicalComplex c).Additive where

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