# Homology is an additive functor #

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

instance HomologicalComplex.instZeroHom_1 {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
Zero (C D)
Equations
• HomologicalComplex.instZeroHom_1 = { zero := { f := fun (i : ι) => 0, comm' := } }
instance HomologicalComplex.instAddHom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
Equations
• HomologicalComplex.instAddHom = { add := fun (f g : C D) => { f := fun (i : ι) => f.f i + g.f i, comm' := } }
instance HomologicalComplex.instNegHom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
Neg (C D)
Equations
• HomologicalComplex.instNegHom = { neg := fun (f : C D) => { f := fun (i : ι) => -f.f i, comm' := } }
instance HomologicalComplex.instSubHom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
Sub (C D)
Equations
• HomologicalComplex.instSubHom = { sub := fun (f g : C D) => { f := fun (i : ι) => f.f i - g.f i, comm' := } }
instance HomologicalComplex.hasNatScalar {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
SMul (C D)
Equations
• HomologicalComplex.hasNatScalar = { smul := fun (n : ) (f : C D) => { f := fun (i : ι) => n f.f i, comm' := } }
instance HomologicalComplex.hasIntScalar {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
SMul (C D)
Equations
• HomologicalComplex.hasIntScalar = { smul := fun (n : ) (f : C D) => { f := fun (i : ι) => n f.f i, comm' := } }
@[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 : ι) :
(f + g).f i = f.f i + g.f i
@[simp]
theorem HomologicalComplex.neg_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (i : ι) :
(-f).f i = -f.f i
@[simp]
theorem HomologicalComplex.sub_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) (g : C D) (i : ι) :
(f - g).f i = f.f i - g.f i
@[simp]
theorem HomologicalComplex.nsmul_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (n : ) (f : C D) (i : ι) :
(n f).f i = n f.f i
@[simp]
theorem HomologicalComplex.zsmul_f_apply {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (n : ) (f : C D) (i : ι) :
(n f).f i = n f.f i
instance HomologicalComplex.instAddCommGroupHom {ι : Type u_1} {V : Type u} {c : } {C : } {D : } :
Equations
instance HomologicalComplex.instPreadditive {ι : Type u_1} {V : Type u} {c : } :
Equations
@[simp]
theorem HomologicalComplex.Hom.fAddMonoidHom_apply {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (i : ι) (f : C₁ C₂) :
= f.f i
def HomologicalComplex.Hom.fAddMonoidHom {ι : Type u_1} {V : Type u} {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
Instances For
instance HomologicalComplex.eval_additive {ι : Type u_1} {V : Type u} {c : } (i : ι) :
Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_map_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) :
∀ {X Y : } (f : X Y) (i : ι), ((F.mapHomologicalComplex c).map f).f i = F.map (f.f i)
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_obj_X {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) (C : ) (i : ι) :
((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplex_obj_d {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) (C : ) (i : ι) (j : ι) :
((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j)
def CategoryTheory.Functor.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) :
(F.mapHomologicalComplex c).PreservesZeroMorphisms
Equations
• =
instance CategoryTheory.Functor.map_homogical_complex_additive {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) [F.Additive] (c : ) :
Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f {ι : Type u_1} (W₁ : Type u_3) [] (c : ) (X : ) (i : ι) :
(.app X).f i =
@[simp]
theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f {ι : Type u_1} (W₁ : Type u_3) [] (c : ) (X : ) (i : ι) :
(.app X).f i =
def CategoryTheory.Functor.mapHomologicalComplexIdIso {ι : Type u_1} (W₁ : Type u_3) [] (c : ) :
.mapHomologicalComplex c

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Functor.mapHomologicalComplex_reflects_iso {ι : Type u_1} (W₁ : Type u_3) {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ) :
(F.mapHomologicalComplex c).ReflectsIsomorphisms
Equations
• =
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ) (C : ) (i : ι) :
( C).f i = α.app (C.X i)
def CategoryTheory.NatTrans.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ) :
F.mapHomologicalComplex c G.mapHomologicalComplex c

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

Equations
• = { app := fun (C : ) => { f := fun (i : ι) => α.app (C.X i), comm' := }, naturality := }
Instances For
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_id {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (c : ) (F : ) [F.PreservesZeroMorphisms] :
= CategoryTheory.CategoryStruct.id (F.mapHomologicalComplex c)
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_comp {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (c : ) {F : } {G : } {H : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (α : F G) (β : G H) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {c : } {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) {C : } {D : } (f : C D) {Z : } (h : (G.mapHomologicalComplex c).obj D Z) :
CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f) = CategoryTheory.CategoryStruct.comp ( C) (CategoryTheory.CategoryStruct.comp ((G.mapHomologicalComplex c).map f) h)
@[simp]
theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {c : } {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) {C : } {D : } (f : C D) :
CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f) ( D) = CategoryTheory.CategoryStruct.comp ( C) ((G.mapHomologicalComplex c).map f)
@[simp]
theorem CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ) (C : ) (i : ι) :
(.app C).f i = α.hom.app (C.X i)
@[simp]
theorem CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ) (C : ) (i : ι) :
(.app C).f i = α.inv.app (C.X i)
def CategoryTheory.NatIso.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F G) (c : ) :
F.mapHomologicalComplex c G.mapHomologicalComplex c

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_functor {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ) :
(e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_inverse {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ) :
(e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex c
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_unitIso {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ) :
(e.mapHomologicalComplex c).unitIso = ≪≫
@[simp]
theorem CategoryTheory.Equivalence.mapHomologicalComplex_counitIso {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ) :
(e.mapHomologicalComplex c).counitIso =
def CategoryTheory.Equivalence.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (e : W₁ W₂) [e.functor.PreservesZeroMorphisms] (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem ChainComplex.map_chain_complex_of {W₁ : Type u_3} {W₂ : Type u_4} [] [] {α : Type u_5} [One α] [] (F : ) [F.PreservesZeroMorphisms] (X : αW₁) (d : (n : α) → X (n + 1) X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) :
(F.mapHomologicalComplex ).obj (ChainComplex.of X d sq) = ChainComplex.of (fun (n : α) => F.obj (X n)) (fun (n : α) => F.map (d n))
instance HomologicalComplex.instAdditiveSingle {ι : Type u_1} {c : } (W : Type u_5) [] [] (j : ι) :
Equations
• =
noncomputable def HomologicalComplex.singleMapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) [] (j : ι) :
.comp (F.mapHomologicalComplex c) F.comp

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_self {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) [] (j : ι) (X : W₁) :
(.hom.app X).f j = CategoryTheory.CategoryStruct.comp (F.map .hom) (HomologicalComplex.singleObjXSelf c j (F.obj X)).inv
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_ne {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) [] {i : ι} {j : ι} (h : i j) (X : W₁) :
(.hom.app X).f i = 0
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_self {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) [] (j : ι) (X : W₁) :
(.inv.app X).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j (F.obj X)).hom (F.map .inv)
@[simp]
theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_ne {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [] [] (F : ) [F.PreservesZeroMorphisms] (c : ) [] {i : ι} {j : ι} (h : i j) (X : W₁) :
(.inv.app X).f i = 0