# Homology is an additive functor #

When V is preadditive, HomologicalComplex V c is also preadditive, and homologyFunctor is additive.

TODO: similarly for R-linear.

instance HomologicalComplex.hasNatScalar {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
SMul (C D)
instance HomologicalComplex.hasIntScalar {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
SMul (C D)
@[simp]
theorem HomologicalComplex.zero_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (i : ι) :
@[simp]
theorem HomologicalComplex.add_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (g : C D) (i : ι) :
@[simp]
theorem HomologicalComplex.neg_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (i : ι) :
@[simp]
theorem HomologicalComplex.sub_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (g : C D) (i : ι) :
@[simp]
theorem HomologicalComplex.nsmul_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (n : ) (f : C D) (i : ι) :
@[simp]
theorem HomologicalComplex.zsmul_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (n : ) (f : C D) (i : ι) :
@[simp]
theorem HomologicalComplex.Hom.fAddMonoidHom_apply {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (i : ι) (f : C₁ C₂) :
def HomologicalComplex.Hom.fAddMonoidHom {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (i : ι) :
(C₁ C₂) →+ ()

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

Instances For
instance HomologicalComplex.eval_additive {ι : Type u_1} {V : Type u} {c : } (i : ι) :
instance HomologicalComplex.cycles_additive {ι : Type u_1} {V : Type u} {c : } (i : ι) :
instance HomologicalComplex.boundaries_additive {ι : Type u_1} {V : Type u} {c : } (i : ι) :
instance HomologicalComplex.homology_additive {ι : Type u_1} {V : Type u} {c : } (i : ι) :
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_obj_d {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) (C : ) (i : ι) (j : ι) :
HomologicalComplex.d (().obj C) i j = F.map ()
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_map_f {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) :
∀ {X Y : } (f : X Y) (i : ι), = F.map ()
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_obj_X {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) (C : ) (i : ι) :
= F.obj ()
def CategoryTheory.Functor.mapHomologicalComplex {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f {ι : Type u_1} (V : Type u) (c : ) (X : ) (i : ι) :
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f {ι : Type u_1} (V : Type u) (c : ) (X : ) (i : ι) :

The functor on homological complexes induced by the identity functor is isomorphic to the identity functor.

Instances For
instance CategoryTheory.Functor.map_homogical_complex_additive {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) :
instance CategoryTheory.Functor.mapHomologicalComplex_reflects_iso {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_app_f {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) (C : ) (i : ι) :
= α.app ()
def CategoryTheory.NatTrans.mapHomologicalComplex {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) :

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

Instances For
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_id {ι : Type u_1} {V : Type u} {W : Type u_2} [] (c : ) (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_comp {ι : Type u_1} {V : Type u} {W : Type u_2} [] (c : ) {F : } {G : } {H : } (α : F G) (β : G H) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc {ι : Type u_1} {V : Type u} {W : Type u_2} [] {c : } {F : } {G : } (α : F G) {C : } {D : } (f : C D) {Z : } (h : ().obj D Z) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality {ι : Type u_1} {V : Type u} {W : Type u_2} [] {c : } {F : } {G : } (α : F G) {C : } {D : } (f : C D) :
@[simp]
theorem CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) (C : ) (i : ι) :
HomologicalComplex.Hom.f (.app C) i = α.hom.app ()
@[simp]
theorem CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) (C : ) (i : ι) :
HomologicalComplex.Hom.f (.app C) i = α.inv.app ()
def CategoryTheory.NatIso.mapHomologicalComplex {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) :

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

Instances For
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_inverse {ι : Type u_1} {V : Type u} {W : Type u_2} [] (e : V W) [CategoryTheory.Functor.Additive e.functor] (c : ) :
().inverse =
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_functor {ι : Type u_1} {V : Type u} {W : Type u_2} [] (e : V W) [CategoryTheory.Functor.Additive e.functor] (c : ) :
().functor =
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_unitIso {ι : Type u_1} {V : Type u} {W : Type u_2} [] (e : V W) [CategoryTheory.Functor.Additive e.functor] (c : ) :
().unitIso =
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_counitIso {ι : Type u_1} {V : Type u} {W : Type u_2} [] (e : V W) [CategoryTheory.Functor.Additive e.functor] (c : ) :
().counitIso =
def CategoryTheory.Equivalence.mapHomologicalComplex {ι : Type u_1} {V : Type u} {W : Type u_2} [] (e : V W) [CategoryTheory.Functor.Additive e.functor] (c : ) :

An equivalence of categories induces an equivalences between the respective categories of homological complex.

Instances For
theorem ChainComplex.map_chain_complex_of {V : Type u} {W : Type u_2} [] {α : Type u_3} [One α] [] (F : ) (X : αV) (d : (n : α) → X (n + 1) X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) :
().obj (ChainComplex.of X d sq) = ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) (_ : ∀ (n : α), CategoryTheory.CategoryStruct.comp ((fun n => F.map (d n)) (n + 1)) ((fun n => F.map (d n)) n) = 0)
def HomologicalComplex.singleMapHomologicalComplex {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) (j : ι) :

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

Instances For
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_self {ι : Type u_1} {V : Type u} (c : ) {W : Type u_2} [] (F : ) (j : ι) (X : V) :
HomologicalComplex.Hom.f (().hom.app X) j = CategoryTheory.eqToHom (_ : F.obj (if j = j then X else 0) = if j = j then F.obj X else 0)
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_ne {ι : Type u_1} {V : Type u} (c : ) {W : Type u_2} [] (F : ) {i : ι} {j : ι} (h : i j) (X : V) :
HomologicalComplex.Hom.f (().hom.app X) i = 0
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_self {ι : Type u_1} {V : Type u} (c : ) {W : Type u_2} [] (F : ) (j : ι) (X : V) :
HomologicalComplex.Hom.f (().inv.app X) j = CategoryTheory.eqToHom (_ : (if j = j then F.obj X else 0) = F.obj (if j = j then X else 0))
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_ne {ι : Type u_1} {V : Type u} (c : ) {W : Type u_2} [] (F : ) {i : ι} {j : ι} (h : i j) (X : V) :
HomologicalComplex.Hom.f (().inv.app X) i = 0

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.

Instances For
@[simp]
theorem ChainComplex.single₀MapHomologicalComplex_hom_app_succ {V : Type u} {W : Type u_2} [] (F : ) (X : V) (n : ) :
HomologicalComplex.Hom.f (.app X) (n + 1) = 0
@[simp]
theorem ChainComplex.single₀MapHomologicalComplex_inv_app_zero {V : Type u} {W : Type u_2} [] (F : ) (X : V) :
@[simp]
theorem ChainComplex.single₀MapHomologicalComplex_inv_app_succ {V : Type u} {W : Type u_2} [] (F : ) (X : V) (n : ) :
HomologicalComplex.Hom.f (.app X) (n + 1) = 0

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.

Instances For
@[simp]
theorem CochainComplex.single₀MapHomologicalComplex_hom_app_succ {V : Type u} {W : Type u_2} [] (F : ) (X : V) (n : ) :
HomologicalComplex.Hom.f (.app X) (n + 1) = 0
@[simp]
theorem CochainComplex.single₀MapHomologicalComplex_inv_app_zero {V : Type u} {W : Type u_2} [] (F : ) (X : V) :
@[simp]
theorem CochainComplex.single₀MapHomologicalComplex_inv_app_succ {V : Type u} {W : Type u_2} [] (F : ) (X : V) (n : ) :
HomologicalComplex.Hom.f (.app X) (n + 1) = 0