The homology of single complexes

The main definition in this file is HomologicalComplex.homologyFunctorSingleIso which is a natural isomorphism single C c j ⋙ homologyFunctor C c j ≅ 𝟭 C.

theorem HomologicalComplex.instHasHomologyObjSingle {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) (i : ι) : ((single C c j).obj A).HasHomology i

theorem HomologicalComplex.exactAt_single_obj {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) (i : ι) (hi : Ne i j) : ((single C c j).obj A).ExactAt i

theorem HomologicalComplex.isZero_single_obj_homology {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) (i : ι) (hi : Ne i j) : CategoryTheory.Limits.IsZero (((single C c j).obj A).homology i)

noncomputable def HomologicalComplex.singleObjCyclesSelfIso {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : CategoryTheory.Iso (((single C c j).obj A).cycles j) A

The canonical isomorphism ((single C c j).obj A).cycles j ≅ A

Equations

• Eq (HomologicalComplex.singleObjCyclesSelfIso c j A) ((((HomologicalComplex.single C c j).obj A).iCyclesIso j (c.next j) ⋯ ⋯).trans (HomologicalComplex.singleObjXSelf c j A))

theorem HomologicalComplex.singleObjCyclesSelfIso_hom {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (singleObjCyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).iCycles j) (singleObjXSelf c j A).hom)

theorem HomologicalComplex.singleObjCyclesSelfIso_hom_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom A Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom h) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).iCycles j) (CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).hom h))

noncomputable def HomologicalComplex.singleObjOpcyclesSelfIso {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : CategoryTheory.Iso A (((single C c j).obj A).opcycles j)

The canonical isomorphism ((single C c j).obj A).opcycles j ≅ A

Equations

• Eq (HomologicalComplex.singleObjOpcyclesSelfIso c j A) ((HomologicalComplex.singleObjXSelf c j A).symm.trans (((HomologicalComplex.single C c j).obj A).pOpcyclesIso (c.prev j) j ⋯ ⋯))

theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (singleObjOpcyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).inv (((single C c j).obj A).pOpcycles j))

theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).opcycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom h) (CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).inv (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).pOpcycles j) h))

noncomputable def HomologicalComplex.singleObjHomologySelfIso {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : CategoryTheory.Iso (((single C c j).obj A).homology j) A

The canonical isomorphism ((single C c j).obj A).homology j ≅ A

Equations

• Eq (HomologicalComplex.singleObjHomologySelfIso c j A) ((((HomologicalComplex.single C c j).obj A).isoHomologyπ (c.prev j) j ⋯ ⋯).symm.trans (HomologicalComplex.singleObjCyclesSelfIso c j A))

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (((single C c j).obj A).iCycles j)) (singleObjXSelf c j A).inv

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).X j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).iCycles j) h)) (CategoryTheory.CategoryStruct.comp (singleObjXSelf c j A).inv h)

theorem HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyπ j) (singleObjHomologySelfIso c j A).hom) (singleObjCyclesSelfIso c j A).hom

theorem HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom A Z) : Eq (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyπ j) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom h)) (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom h)

theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom (singleObjHomologySelfIso c j A).inv) (((single C c j).obj A).homologyπ j)

theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).homology j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv h)) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyπ j) h)

theorem HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom (singleObjOpcyclesSelfIso c j A).hom) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).iCycles j) (((single C c j).obj A).pOpcycles j))

theorem HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).opcycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom h)) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).iCycles j) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).pOpcycles j) h))

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (((single C c j).obj A).homologyπ j)) (singleObjHomologySelfIso c j A).inv

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).homology j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyπ j) h)) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv h)

theorem HomologicalComplex.singleObjHomologySelfIso_inv_homologyι {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv (((single C c j).obj A).homologyι j)) (singleObjOpcyclesSelfIso c j A).hom

theorem HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).opcycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyι j) h)) (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom h)

theorem HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyι j) (singleObjOpcyclesSelfIso c j A).inv) (singleObjHomologySelfIso c j A).hom

theorem HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom A Z) : Eq (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyι j) (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).inv h)) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom h)

theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom (singleObjOpcyclesSelfIso c j A).hom) (((single C c j).obj A).homologyι j)

theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) {Z : C} (h : Quiver.Hom (((single C c j).obj A).opcycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom h)) (CategoryTheory.CategoryStruct.comp (((single C c j).obj A).homologyι j) h)

theorem HomologicalComplex.singleObjCyclesSelfIso_hom_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (cyclesMap ((single C c j).map f) j) (singleObjCyclesSelfIso c j B).hom) (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom f)

theorem HomologicalComplex.singleObjCyclesSelfIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom B Z) : Eq (CategoryTheory.CategoryStruct.comp (cyclesMap ((single C c j).map f) j) (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j B).hom h)) (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp f h))

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (cyclesMap ((single C c j).map f) j)) (CategoryTheory.CategoryStruct.comp f (singleObjCyclesSelfIso c j B).inv)

theorem HomologicalComplex.singleObjCyclesSelfIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom (((single C c j).obj B).cycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (cyclesMap ((single C c j).map f) j) h)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (singleObjCyclesSelfIso c j B).inv h))

theorem HomologicalComplex.singleObjHomologySelfIso_hom_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (homologyMap ((single C c j).map f) j) (singleObjHomologySelfIso c j B).hom) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom f)

theorem HomologicalComplex.singleObjHomologySelfIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom B Z) : Eq (CategoryTheory.CategoryStruct.comp (homologyMap ((single C c j).map f) j) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j B).hom h)) (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).hom (CategoryTheory.CategoryStruct.comp f h))

theorem HomologicalComplex.singleObjHomologySelfIso_inv_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv (homologyMap ((single C c j).map f) j)) (CategoryTheory.CategoryStruct.comp f (singleObjHomologySelfIso c j B).inv)

theorem HomologicalComplex.singleObjHomologySelfIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom (((single C c j).obj B).homology j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (homologyMap ((single C c j).map f) j) h)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (singleObjHomologySelfIso c j B).inv h))

theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom (opcyclesMap ((single C c j).map f) j)) (CategoryTheory.CategoryStruct.comp f (singleObjOpcyclesSelfIso c j B).hom)

theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom (((single C c j).obj B).opcycles j) Z) : Eq (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (opcyclesMap ((single C c j).map f) j) h)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j B).hom h))

theorem HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) : Eq (CategoryTheory.CategoryStruct.comp (opcyclesMap ((single C c j).map f) j) (singleObjOpcyclesSelfIso c j B).inv) (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).inv f)

theorem HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) {A B : C} (f : Quiver.Hom A B) {Z : C} (h : Quiver.Hom B Z) : Eq (CategoryTheory.CategoryStruct.comp (opcyclesMap ((single C c j).map f) j) (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j B).inv h)) (CategoryTheory.CategoryStruct.comp (singleObjOpcyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp f h))

noncomputable def HomologicalComplex.homologyFunctorSingleIso (C : Type u) [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Iso ((single C c j).comp (homologyFunctor C c j)) (CategoryTheory.Functor.id C)

The computation of the homology of single complexes, as a natural isomorphism single C c j ⋙ homologyFunctor C c j ≅ 𝟭 C.

Equations

• Eq (HomologicalComplex.homologyFunctorSingleIso C c j) (CategoryTheory.NatIso.ofComponents (fun (A : C) => HomologicalComplex.singleObjHomologySelfIso c j A) ⋯)

theorem HomologicalComplex.homologyFunctorSingleIso_hom_app (C : Type u) [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) [CategoryTheory.CategoryWithHomology C] (X : C) : Eq ((homologyFunctorSingleIso C c j).hom.app X) (singleObjHomologySelfIso c j X).hom

theorem HomologicalComplex.homologyFunctorSingleIso_inv_app (C : Type u) [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) [CategoryTheory.CategoryWithHomology C] (X : C) : Eq ((homologyFunctorSingleIso C c j).inv.app X) (singleObjHomologySelfIso c j X).inv

theorem ChainComplex.exactAt_succ_single_obj {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : Nat) : HomologicalComplex.ExactAt ((single₀ C).obj A) (HAdd.hAdd n 1)

theorem CochainComplex.exactAt_succ_single_obj {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : Nat) : HomologicalComplex.ExactAt ((single₀ C).obj A) (HAdd.hAdd n 1)