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' := ⋯ } }

source

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' := ⋯ } }

source

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' := ⋯ } }

source

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' := ⋯ } }

source

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' := ⋯ } }

source

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' := ⋯ } }

source

@[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 : ι) :

Hom.f 0 i = 0

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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 := ⋯ }

source

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) ⋯

Instances For

source

@[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₂) :

(fAddMonoidHom i) f = f.f i

source

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

(eval V c i).Additive

source

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

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.

Instances For

source

@[simp]

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

source

@[simp]

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

source

@[simp]

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

((F.mapHomologicalComplex c).obj C).X i = F.obj (C.X i)

source

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

(F.mapHomologicalComplex c).PreservesZeroMorphisms

source

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

(F.mapHomologicalComplex c).Additive

source

def CategoryTheory.Functor.mapHomologicalComplexIdIso {ι : Type u_1} (W₁ : Type u_3) [Category.{u_5, u_3} W₁] [Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) :

(Functor.id W₁).mapHomologicalComplex c ≅ 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.

Instances For

source

@[simp]

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

((mapHomologicalComplexIdIso W₁ c).inv.app X).f i = CategoryStruct.id (X.X i)

source

@[simp]

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

((mapHomologicalComplexIdIso W₁ c).hom.app X).f i = CategoryStruct.id (X.X i)

source

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

(F.mapHomologicalComplex c).ReflectsIsomorphisms

source

def CategoryTheory.NatTrans.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [Category.{u_5, u_3} W₁] [Category.{u_6, u_4} W₂] [Limits.HasZeroMorphisms W₁] [Limits.HasZeroMorphisms W₂] {F G : 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 := ⋯ }

Instances For

source

@[simp]

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

((mapHomologicalComplex α c).app C).f x✝ = α.app (C.X x✝)

source

@[simp]

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

mapHomologicalComplex (CategoryStruct.id F) c = CategoryStruct.id (F.mapHomologicalComplex c)

source

@[simp]

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

mapHomologicalComplex (CategoryStruct.comp α β) c = CategoryStruct.comp (mapHomologicalComplex α c) (mapHomologicalComplex β c)

source

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

CategoryStruct.comp ((F.mapHomologicalComplex c).map f) ((mapHomologicalComplex α c).app D) = CategoryStruct.comp ((mapHomologicalComplex α c).app C) ((G.mapHomologicalComplex c).map f)

source

theorem CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [Category.{u_5, u_3} W₁] [Category.{u_6, u_4} W₂] [Limits.HasZeroMorphisms W₁] [Limits.HasZeroMorphisms W₂] {c : ComplexShape ι} {F G : 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) :

CategoryStruct.comp ((F.mapHomologicalComplex c).map f) (CategoryStruct.comp ((mapHomologicalComplex α c).app D) h) = CategoryStruct.comp ((mapHomologicalComplex α c).app C) (CategoryStruct.comp ((G.mapHomologicalComplex c).map f) h)

source

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

Instances For

source

@[simp]

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

((mapHomologicalComplex α c).hom.app C).f x✝ = α.hom.app (C.X x✝)

source

@[simp]

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

((mapHomologicalComplex α c).inv.app C).f x✝ = α.inv.app (C.X x✝)

source

def CategoryTheory.Equivalence.mapHomologicalComplex {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [Category.{u_5, u_3} W₁] [Category.{u_6, u_4} W₂] [Limits.HasZeroMorphisms W₁] [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.

Instances For

source

@[simp]

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

(e.mapHomologicalComplex c).inverse = e.inverse.mapHomologicalComplex c

source

@[simp]

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

(e.mapHomologicalComplex c).unitIso = (Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ NatIso.mapHomologicalComplex e.unitIso c

source

@[simp]

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

(e.mapHomologicalComplex c).functor = e.functor.mapHomologicalComplex c

source

@[simp]

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

(e.mapHomologicalComplex c).counitIso = NatIso.mapHomologicalComplex e.counitIso c ≪≫ Functor.mapHomologicalComplexIdIso W₂ c

source

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 (of X d sq) = of (fun (n : α) => F.obj (X n)) (fun (n : α) => F.map (d n)) ⋯

source

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 : ι) :

(single W c j).Additive

source

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 : ι) :

(single W₁ c j).comp (F.mapHomologicalComplex c) ≅ F.comp (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.

Instances For

source

@[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₁) :

((singleMapHomologicalComplex F c j).hom.app X).f j = CategoryTheory.CategoryStruct.comp (F.map (singleObjXSelf c j X).hom) (singleObjXSelf c j (F.obj X)).inv

source

@[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₁) :

((singleMapHomologicalComplex F c j).hom.app X).f i = 0

source

@[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₁) :

((singleMapHomologicalComplex F c j).inv.app X).f j = CategoryTheory.CategoryStruct.comp (singleObjXSelf c j (F.obj X)).hom (F.map (singleObjXSelf c j X).inv)

source

@[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₁) :

((singleMapHomologicalComplex F c j).inv.app X).f i = 0

Documentation

Mathlib.Algebra.Homology.Additive

Homology is an additive functor #