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
@[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
@[simp]
theorem homological_complex.nsmul_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} (n : ) (f : C D) (i : ι) :
(n f).f i = n f.f i
@[simp]
theorem homological_complex.zsmul_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} (n : ) (f : C D) (i : ι) :
(n f).f i = n f.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
Instances for category_theory.functor.map_homological_complex
@[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
theorem chain_complex.map_chain_complex_of {V : Type u} [category_theory.category V] [category_theory.preadditive V] {W : Type u_2} [category_theory.category W] [category_theory.preadditive W] {α : Type u_4} [add_right_cancel_semigroup α] [has_one α] [decidable_eq α] (F : V W) [F.additive] (X : α → V) (d : Π (n : α), X (n + 1) X n) (sq : ∀ (n : α), d (n + 1) d n = 0) :
(F.map_homological_complex (complex_shape.down α)).obj (chain_complex.of X d sq) = chain_complex.of (λ (n : α), F.obj (X n)) (λ (n : α), F.map (d n)) _

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

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

Equations