Homology commutes with scalar multiplication of chain maps

For a linear category C, the map induced on homology by a chain map is linear in the chain map: homologyMap (a • φ) i = a • homologyMap φ i. This is the homological-complex version of Mathlib's ShortComplex.homologyMap_smul, recorded as a TODO in Mathlib/Algebra/Homology/Linear.lean. It identifies, for instance, the map induced by multiplication by a scalar on a complex of modules with multiplication by that scalar on homology, and it makes the homology functor in each degree a linear functor.

@[simp]

theorem HomologicalComplex.shortComplexFunctor_map_smul {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_3} {c : ComplexShape ι} (i : ι) (a : R) {K L : HomologicalComplex C c} (φ : K ⟶ L) : (shortComplexFunctor C c i).map (a • φ) = a • (shortComplexFunctor C c i).map φ

The short complex attached to a degree sends a scalar multiple of a chain map to the scalar multiple of the induced morphism of short complexes.

@[simp]

theorem HomologicalComplex.homologyMap_smul {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_3} {c : ComplexShape ι} (a : R) {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : homologyMap (a • φ) i = a • homologyMap φ i

The map induced on homology by a scalar multiple of a chain map is the scalar multiple of the induced map.

instance HomologicalComplex.instLinearHomologyFunctor_tauCeti {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_3} {c : ComplexShape ι} [CategoryTheory.CategoryWithHomology C] (i : ι) : CategoryTheory.Functor.Linear R (homologyFunctor C c i)

Taking homology in a fixed degree is a linear functor.