# The category of homological complexes is linear #

In this file, we define the instance Linear R (HomologicalComplex C c) when the category C is R-linear.

## TODO #

• show lemmas like HomologicalComplex.homologyMap_smul (after doing the same for short complexes in Mathlib.Algebra.Homology.ShortComplex.Linear)
instance HomologicalComplex.instSMulHom {R : Type u_1} [] {C : Type u_2} [] [] {ι : Type u_4} {c : } {X : } {Y : } :
SMul R (X Y)
Equations
• HomologicalComplex.instSMulHom = { smul := fun (r : R) (f : X Y) => { f := fun (n : ι) => r f.f n, comm' := } }
@[simp]
theorem HomologicalComplex.smul_f_apply {R : Type u_1} [] {C : Type u_2} [] [] {ι : Type u_4} {c : } {X : } {Y : } (r : R) (f : X Y) (n : ι) :
(r f).f n = r f.f n
@[simp]
theorem HomologicalComplex.units_smul_f_apply {R : Type u_1} [] {C : Type u_2} [] [] {ι : Type u_4} {c : } {X : } {Y : } (r : Rˣ) (f : X Y) (n : ι) :
(r f).f n = r f.f n
instance HomologicalComplex.instModuleHom {R : Type u_1} [] {C : Type u_2} [] [] {ι : Type u_4} {c : } (X : ) (Y : ) :
Module R (X Y)
Equations
• X.instModuleHom Y =
instance HomologicalComplex.instLinear {R : Type u_1} [] {C : Type u_2} [] [] {ι : Type u_4} {c : } :
Equations
• HomologicalComplex.instLinear = { homModule := inferInstance, smul_comp := , comp_smul := }
instance CategoryTheory.Functor.mapHomologicalComplex_linear {R : Type u_1} [] {C : Type u_2} {D : Type u_3} [] [] [] [] {ι : Type u_4} (F : ) [F.Additive] (c : ) :
CategoryTheory.Functor.Linear R (F.mapHomologicalComplex c)
Equations
• =