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.lean)

@[instance_reducible]

instance HomologicalComplex.instSMulHom {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_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.{v_1, 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.{v_1, 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_reducible]

instance HomologicalComplex.instModuleHom {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_4} {c : ComplexShape ι} (X Y : HomologicalComplex C c) : Module R (X ⟶ Y)

Equations

• X.instModuleHom Y = { toSMul := HomologicalComplex.instSMulHom, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance HomologicalComplex.instLinear {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_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} [Category.{v_1, u_2} C] [Preadditive C] [Category.{v_2, u_3} D] [Preadditive D] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] {ι : Type u_4} (F : Functor C D) [F.Additive] [Linear R F] (c : ComplexShape ι) : Linear R (F.mapHomologicalComplex c)