mapHomologicalComplex_linear — Mathlib

English

If F: C → D is a linear functor, then it sends maps of chain complexes to linear maps of their images, preserving R-linearity.

Русский

Если F: C → D линейный, он переводит отображения между комплексами в линейные отображения между их образами, сохраняя линейность по R.

LaTeX

$$$F.mapHomologicalComplex(c)$ is linear in the sense of category theory over R.$$

Lean4

instance mapHomologicalComplex_linear (F : C ⥤ D) [F.Additive] [Functor.Linear R F] (c : ComplexShape ι) :
    Functor.Linear R (F.mapHomologicalComplex c) where

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