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.

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

Equations

• ⋯ = ⋯

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

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

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

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

Equations

• HomologicalComplex.singleObjCyclesSelfIso c j A = ((HomologicalComplex.single C c j).obj A).iCyclesIso j (c.next j) ⋯ ⋯ ≪≫ HomologicalComplex.singleObjXSelf c j A

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

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

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

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

Equations

• HomologicalComplex.singleObjOpcyclesSelfIso c j A = (HomologicalComplex.singleObjXSelf c j A).symm ≪≫ ((HomologicalComplex.single C c j).obj A).pOpcyclesIso (c.prev j) j ⋯ ⋯

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

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

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

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

Equations

• HomologicalComplex.singleObjHomologySelfIso c j A = (((HomologicalComplex.single C c j).obj A).isoHomologyπ (c.prev j) j ⋯ ⋯).symm ≪≫ HomologicalComplex.singleObjCyclesSelfIso c j A

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def HomologicalComplex.homologyFunctorSingleIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [DecidableEq ι] (c : ComplexShape ι) (j : ι) [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.single C c j).comp (HomologicalComplex.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

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

noncomputable def ChainComplex.homology'Functor0Single₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] : (ChainComplex.single₀ C).comp (homology'Functor C (ComplexShape.down ℕ) 0) ≅ CategoryTheory.Functor.id C

Sending objects to chain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

Equations

• ChainComplex.homology'Functor0Single₀ C = CategoryTheory.NatIso.ofComponents (fun (X : C) => homology'.congr ⋯ ⋯ ⋯ ⋯ ≪≫ homology'ZeroZero) ⋯

noncomputable def ChainComplex.homology'FunctorSuccSingle₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] (n : ℕ) : (ChainComplex.single₀ C).comp (homology'Functor C (ComplexShape.down ℕ) (n + 1)) ≅ 0

Sending objects to chain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

Equations

• ChainComplex.homology'FunctorSuccSingle₀ C n = CategoryTheory.NatIso.ofComponents (fun (X : C) => homology'.congr ⋯ ⋯ ⋯ ⋯ ≪≫ homology'ZeroZero ≪≫ ⋯.isoZero.symm) ⋯

noncomputable def CochainComplex.homologyFunctor0Single₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] : (CochainComplex.single₀ C).comp (homology'Functor C (ComplexShape.up ℕ) 0) ≅ CategoryTheory.Functor.id C

Sending objects to cochain complexes supported at 0 then taking 0-th homology is the same as doing nothing.

Equations

• CochainComplex.homologyFunctor0Single₀ C = CategoryTheory.NatIso.ofComponents (fun (X : C) => homology'.congr ⋯ ⋯ ⋯ ⋯ ≪≫ homology'ZeroZero) ⋯

noncomputable def CochainComplex.homology'FunctorSuccSingle₀ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.Limits.HasImages C] [CategoryTheory.Limits.HasImageMaps C] (n : ℕ) : (CochainComplex.single₀ C).comp (homology'Functor C (ComplexShape.up ℕ) (n + 1)) ≅ 0

Sending objects to cochain complexes supported at 0 then taking (n+1)-st homology is the same as the zero functor.

Equations

• CochainComplex.homology'FunctorSuccSingle₀ C n = CategoryTheory.NatIso.ofComponents (fun (X : C) => homology'.congr ⋯ ⋯ ⋯ ⋯ ≪≫ homology'ZeroZero ≪≫ ⋯.isoZero.symm) ⋯

theorem ChainComplex.exactAt_succ_single_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℕ) : HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj A) (n + 1)

theorem CochainComplex.exactAt_succ_single_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℕ) : HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj A) (n + 1)