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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Zero (C ⟶ D)

Equations

• HomologicalComplex.instZeroHom_1 = { zero := { f := fun (x : ι) => 0, comm' := ⋯ } }

instance HomologicalComplex.instAddHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : Add (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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι) : HomologicalComplex.Hom.f 0 i = 0

@[simp]

theorem HomologicalComplex.add_f_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) (i : ι) : (-f).f i = -f.f i

@[simp]

theorem HomologicalComplex.sub_f_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (n : ℤ) (f : C ⟶ D) (i : ι) : (n • f).f i = n • f.f i

instance HomologicalComplex.instAddCommGroupHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} : AddCommGroup (C ⟶ D)

Equations

• HomologicalComplex.instAddCommGroupHom = Function.Injective.addCommGroup HomologicalComplex.Hom.f ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance HomologicalComplex.instPreadditive {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} : CategoryTheory.Preadditive (HomologicalComplex V c)

Equations

• HomologicalComplex.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

def HomologicalComplex.Hom.fAddMonoidHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex 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

• HomologicalComplex.Hom.fAddMonoidHom i = AddMonoidHom.mk' (fun (f : C₁ ⟶ C₂) => f.f i) ⋯

@[simp]

theorem HomologicalComplex.Hom.fAddMonoidHom_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (i : ι) (f : C₁ ⟶ C₂) : (HomologicalComplex.Hom.fAddMonoidHom i) f = f.f i

instance HomologicalComplex.eval_additive {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (i : ι) : (HomologicalComplex.eval V c i).Additive

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex W₁ c) (HomologicalComplex W₂ 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.

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_obj_d {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i j : ι) : ((F.mapHomologicalComplex c).obj C).d i j = F.map (C.d i j)

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplex_map_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) {X✝ Y✝ : HomologicalComplex W₁ c} (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} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (i : ι) : ((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)

instance CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) : (F.mapHomologicalComplex c).PreservesZeroMorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.map_homogical_complex_additive {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_5, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (c : ComplexShape ι) : (F.mapHomologicalComplex c).Additive

Equations

• ⋯ = ⋯

def CategoryTheory.Functor.mapHomologicalComplexIdIso {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) : (CategoryTheory.Functor.id W₁).mapHomologicalComplex c ≅ CategoryTheory.Functor.id (HomologicalComplex W₁ 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.

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) : ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

@[simp]

theorem CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f {ι : Type u_1} (W₁ : Type u_3) [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι) : ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

instance CategoryTheory.Functor.mapHomologicalComplex_reflects_iso {ι : Type u_1} (W₁ : Type u_3) {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ComplexShape ι) : (F.mapHomologicalComplex c).ReflectsIsomorphisms

Equations

• ⋯ = ⋯

def CategoryTheory.NatTrans.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) (c : ComplexShape ι) : F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c

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

Equations

• CategoryTheory.NatTrans.mapHomologicalComplex α c = { app := fun (C : HomologicalComplex W₁ c) => { f := fun (x : ι) => α.app (C.X x), comm' := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C).f x✝ = α.app (C.X x✝)

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_id {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] : CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id F) c = CategoryTheory.CategoryStruct.id (F.mapHomologicalComplex c)

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_comp {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) {F G H : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.comp α β) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomologicalComplex α c) (CategoryTheory.NatTrans.mapHomologicalComplex β c)

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {c : ComplexShape ι} {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) : CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f) ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C) ((G.mapHomologicalComplex c).map f)

@[simp]

theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {c : ComplexShape ι} {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) {Z : HomologicalComplex W₂ c} (h : (G.mapHomologicalComplex c).obj D ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C) (CategoryTheory.CategoryStruct.comp ((G.mapHomologicalComplex c).map f) h)

def CategoryTheory.NatIso.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) : 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.

@[simp]

theorem CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatIso.mapHomologicalComplex α c).hom.app C).f x✝ = α.hom.app (C.X x✝)

@[simp]

theorem CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) (C : HomologicalComplex W₁ c) (x✝ : ι) : ((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f x✝ = α.inv.app (C.X x✝)

def CategoryTheory.Equivalence.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : HomologicalComplex W₁ c ≌ HomologicalComplex W₂ 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.

@[simp]

theorem CategoryTheory.Equivalence.mapHomologicalComplex_inverse {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (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} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).unitIso = (CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c

@[simp]

theorem CategoryTheory.Equivalence.mapHomologicalComplex_functor {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c

@[simp]

theorem CategoryTheory.Equivalence.mapHomologicalComplex_counitIso {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) : (e.mapHomologicalComplex c).counitIso = CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c ≪≫ CategoryTheory.Functor.mapHomologicalComplexIdIso W₂ c

theorem ChainComplex.map_chain_complex_of {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_7, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] {α : Type u_5} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (X : α → W₁) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) : (F.mapHomologicalComplex (ComplexShape.down α)).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 : ComplexShape ι} (W : Type u_5) [CategoryTheory.Category.{u_6, u_5} W] [CategoryTheory.Preadditive W] [CategoryTheory.Limits.HasZeroObject W] [DecidableEq ι] (j : ι) : (HomologicalComplex.single W c j).Additive

Equations

• ⋯ = ⋯

noncomputable def HomologicalComplex.singleMapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_5, u_3} W₁] [CategoryTheory.Category.{u_6, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] (j : ι) : (HomologicalComplex.single W₁ c j).comp (F.mapHomologicalComplex c) ≅ F.comp (HomologicalComplex.single W₂ 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.singleMapHomologicalComplex_hom_app_self {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_5, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] (j : ι) (X : W₁) : ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f j = CategoryTheory.CategoryStruct.comp (F.map (HomologicalComplex.singleObjXSelf c j X).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} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_5, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] {i j : ι} (h : i ≠ j) (X : W₁) : ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f i = 0

@[simp]

theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_self {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_5, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] (j : ι) (X : W₁) : ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f j = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j (F.obj X)).hom (F.map (HomologicalComplex.singleObjXSelf c j X).inv)

@[simp]

theorem HomologicalComplex.singleMapHomologicalComplex_inv_app_ne {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [CategoryTheory.Category.{u_6, u_3} W₁] [CategoryTheory.Category.{u_5, u_4} W₂] [CategoryTheory.Limits.HasZeroMorphisms W₁] [CategoryTheory.Limits.HasZeroMorphisms W₂] [CategoryTheory.Limits.HasZeroObject W₁] [CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) [DecidableEq ι] {i j : ι} (h : i ≠ j) (X : W₁) : ((HomologicalComplex.singleMapHomologicalComplex F c j).inv.app X).f i = 0