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} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι} {X Y : HomologicalComplex C c} : 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} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι} {X Y : HomologicalComplex C c} (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} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι} {X Y : HomologicalComplex C c} (r : Rˣ) (f : X ⟶ Y) (n : ι) : (r • f).f n = r • f.f n

instance HomologicalComplex.instModuleHom {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι} (X Y : HomologicalComplex C c) : Module R (X ⟶ Y)

Equations

• X.instModuleHom Y = Module.mk ⋯ ⋯

instance HomologicalComplex.instLinear {R : Type u_1} [Semiring R] {C : Type u_2} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {ι : Type u_4} {c : ComplexShape ι} : CategoryTheory.Linear R (HomologicalComplex C c)

Equations

• HomologicalComplex.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

instance CategoryTheory.Functor.mapHomologicalComplex_linear {R : Type u_1} [Semiring R] {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_5, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Category.{u_6, u_3} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] {ι : Type u_4} (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear R F] (c : ComplexShape ι) : CategoryTheory.Functor.Linear R (F.mapHomologicalComplex c)