mathlib documentation

algebra.homology.additive

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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem homological_complex.zero_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (i : ι) :
0.f i = 0
@[simp]
theorem homological_complex.add_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V 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} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : C D) (i : ι) :
(-f).f i = -f.f i
@[simp]
theorem homological_complex.sub_f_apply {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f g : C D) (i : ι) :
(f - g).f i = f.f i - g.f i
@[protected, instance]
Equations
def homological_complex.hom.f_add_monoid_hom {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ : homological_complex V 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} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C₁ C₂ : homological_complex V c} (i : ι) (f : C₁ C₂) :
@[protected, instance]
@[simp]
theorem category_theory.functor.map_homological_complex_map_f {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V W) [F.additive] (c : complex_shape ι) (C D : homological_complex V c) (f : C D) (i : ι) :
((F.map_homological_complex c).map f).f i = F.map (f.f i)

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

Equations
@[simp]
@[simp]
theorem category_theory.functor.map_homological_complex_obj_d {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] (F : V W) [F.additive] (c : complex_shape ι) (C : homological_complex V c) (i j : ι) :
((F.map_homological_complex c).obj C).d i j = F.map (C.d i j)

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

Equations

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

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