Lean/Mathlib: homology functors on D(A) are linear via Localization.functor_linear_iff

Mathlib (late 2026) has Linear R (DerivedCategory C) and linearity of Q, shifts and singleFunctor, but no Functor.Linear R (DerivedCategory.homologyFunctor C n), and not even HomologicalComplex.homologyMap_smul (it is listed as a TODO). Fix in three steps. (1) homologyMap_smul: dsimp [homologyMap]; rw [← ShortComplex.homologyMap_smul]; rfl (needs import Mathlib.Algebra.Homology.ShortComplex.Linear and set_option backward.isDefEq.respectTransparency false in), which gives the instance on HomologicalComplex.homologyFunctor. (2) Make a local Localization.Lifting Q (HomologicalComplex.quasiIso C (.up ℤ)) (HomologicalComplex.homologyFunctor C (.up ℤ) n) (homologyFunctor C n) := ⟨homologyFunctorFactors C n⟩. (3) exact (Localization.functor_linear_iff Q (HomologicalComplex.quasiIso C (.up ℤ)) R F G).1 inferInstance, passing F and G explicitly or the instance problem gets stuck. Related: shifts on P.FullSubcategory are irreducible, so prove their linearity through P.ι.map_injective + cancel_mono ((P.ι.commShiftIso n).hom.app Y) + Functor.commShiftIso_hom_naturality.