# Homology is an additive functor #

When V is preadditive, homological_complex V c is also preadditive, and homology_functor is additive.

TODO: similarly for R-linear.

@[protected, instance]
def homological_complex.quiver.hom.has_zero {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} :
Equations
@[protected, instance]
def homological_complex.quiver.hom.has_add {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} :
Equations
@[protected, instance]
def homological_complex.quiver.hom.has_neg {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} :
has_neg (C D)
Equations
@[protected, instance]
def homological_complex.quiver.hom.has_sub {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} :
has_sub (C D)
Equations
@[simp]
theorem homological_complex.zero_f_apply {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (i : ι) :
0.f i = 0
@[simp]
theorem homological_complex.add_f_apply {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f g : C D) (i : ι) :
(f + g).f i = f.f i + g.f i
@[simp]
theorem homological_complex.neg_f_apply {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : C D) (i : ι) :
(-f).f i = -f.f i
@[simp]
theorem homological_complex.sub_f_apply {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f g : C D) (i : ι) :
(f - g).f i = f.f i - g.f i
@[protected, instance]
def homological_complex.quiver.hom.add_comm_group {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} :
Equations
@[protected, instance]
def homological_complex.category_theory.preadditive {ι : Type u_1} {V : Type u} {c : complex_shape ι} :
Equations
def homological_complex.hom.f_add_monoid_hom {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (i : ι) :
(C₁ C₂) →+ (C₁.X i C₂.X i)

The i-th component of a chain map, as an additive map from chain maps to morphisms.

Equations
@[simp]
theorem homological_complex.hom.f_add_monoid_hom_apply {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C₁ C₂ : c} (i : ι) (f : C₁ C₂) :
@[protected, instance]
def homological_complex.eval_additive {ι : Type u_1} {V : Type u} {c : complex_shape ι} (i : ι) :
@[protected, instance]
def homological_complex.cycles_additive {ι : Type u_1} {V : Type u} {c : complex_shape ι} (i : ι)  :
@[protected, instance]
def homological_complex.boundaries_additive {ι : Type u_1} {V : Type u} {c : complex_shape ι} (i : ι)  :
@[protected, instance]
def homological_complex.homology_additive {ι : Type u_1} {V : Type u} {c : complex_shape ι} (i : ι)  :
@[simp]
theorem category_theory.functor.map_homological_complex_map_f {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) (C D : c) (f : C D) (i : ι) :
((F.map_homological_complex c).map f).f i = F.map (f.f i)
def category_theory.functor.map_homological_complex {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) :

An additive functor induces a functor between homological complexes. This is sometimes called the "prolongation".

Equations
@[simp]
theorem category_theory.functor.map_homological_complex_obj_X {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) (C : c) (i : ι) :
((F.map_homological_complex c).obj C).X i = F.obj (C.X i)
@[simp]
theorem category_theory.functor.map_homological_complex_obj_d {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) (C : c) (i j : ι) :
((F.map_homological_complex c).obj C).d i j = F.map (C.d i j)
@[protected, instance]
def category_theory.functor.map_homogical_complex_additive {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) :
def category_theory.nat_trans.map_homological_complex {ι : Type u_1} {V : Type u} {W : Type u_2} {F G : V W} [F.additive] [G.additive] (α : F G) (c : complex_shape ι) :

A natural transformation between functors induces a natural transformation between those functors applied to homological complexes.

Equations
@[simp]
theorem category_theory.nat_trans.map_homological_complex_app_f {ι : Type u_1} {V : Type u} {W : Type u_2} {F G : V W} [F.additive] [G.additive] (α : F G) (c : complex_shape ι) (C : c) (i : ι) :
= α.app (C.X i)
@[simp]
theorem category_theory.nat_trans.map_homological_complex_id {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) (F : V W) [F.additive] :
@[simp]
theorem category_theory.nat_trans.map_homological_complex_comp {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) {F G H : V W} [F.additive] [G.additive] [H.additive] (α : F G) (β : G H) :
@[simp]
theorem category_theory.nat_trans.map_homological_complex_naturality {ι : Type u_1} {V : Type u} {W : Type u_2} {c : complex_shape ι} {F G : V W} [F.additive] [G.additive] (α : F G) {C D : c} (f : C D) :
=
@[simp]
theorem category_theory.nat_trans.map_homological_complex_naturality_assoc {ι : Type u_1} {V : Type u} {W : Type u_2} {c : complex_shape ι} {F G : V W} [F.additive] [G.additive] (α : F G) {C D : c} (f : C D) {X' : c} (f' : .obj D X') :
.map f = .map f f'
noncomputable def homological_complex.single_map_homological_complex {ι : Type u_1} {V : Type u} {W : Type u_2} (F : V W) [F.additive] (c : complex_shape ι) (j : ι) :
F

Turning an object into a complex supported at j then applying a functor is the same as applying the functor then forming the complex.

Equations
@[simp]
theorem homological_complex.single_map_homological_complex_hom_app_self {ι : Type u_1} {V : Type u} (c : complex_shape ι) {W : Type u_2} (F : V W) [F.additive] (j : ι) (X : V) :
@[simp]
theorem homological_complex.single_map_homological_complex_hom_app_ne {ι : Type u_1} {V : Type u} (c : complex_shape ι) {W : Type u_2} (F : V W) [F.additive] {i j : ι} (h : i j) (X : V) :
.f i = 0
@[simp]
theorem homological_complex.single_map_homological_complex_inv_app_self {ι : Type u_1} {V : Type u} (c : complex_shape ι) {W : Type u_2} (F : V W) [F.additive] (j : ι) (X : V) :
@[simp]
theorem homological_complex.single_map_homological_complex_inv_app_ne {ι : Type u_1} {V : Type u} (c : complex_shape ι) {W : Type u_2} (F : V W) [F.additive] {i j : ι} (h : i j) (X : V) :
.f i = 0
def chain_complex.single₀_map_homological_complex {V : Type u} {W : Type u_2} (F : V W) [F.additive] :

Turning an object into a chain complex supported at zero then applying a functor is the same as applying the functor then forming the complex.

Equations
@[simp]
theorem chain_complex.single₀_map_homological_complex_hom_app_zero {V : Type u} {W : Type u_2} (F : V W) [F.additive] (X : V) :
= 𝟙 X).X 0)
@[simp]
theorem chain_complex.single₀_map_homological_complex_hom_app_succ {V : Type u} {W : Type u_2} (F : V W) [F.additive] (X : V) (n : ) :
(n + 1) = 0
@[simp]
theorem chain_complex.single₀_map_homological_complex_inv_app_zero {V : Type u} {W : Type u_2} (F : V W) [F.additive] (X : V) :
= 𝟙 (((F .obj X).X 0)
@[simp]
theorem chain_complex.single₀_map_homological_complex_inv_app_succ {V : Type u} {W : Type u_2} (F : V W) [F.additive] (X : V) (n : ) :
(n + 1) = 0