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.instHasHomologyObjToQuiverToCategoryStructHomologicalComplexToQuiverToCategoryStructInstCategoryHomologicalComplexToPrefunctorSingle {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.HasHomology ((HomologicalComplex.single C c j).toPrefunctor.obj A) i

Equations

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

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.ExactAt ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homology ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.cycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) j ≅ A

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

Equations

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

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.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) j

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

Equations

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

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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.pOpcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.pOpcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homology ((HomologicalComplex.single C c j).toPrefunctor.obj A) j ≅ A

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

Equations

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

@[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).toPrefunctor.obj A).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homology ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.iCycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) j) (HomologicalComplex.pOpcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homology ((HomologicalComplex.single C c j).toPrefunctor.obj A) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyπ ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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.homologyι ((HomologicalComplex.single C c j).toPrefunctor.obj A) 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).toPrefunctor.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).toPrefunctor.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.cycles ((HomologicalComplex.single C c j).toPrefunctor.obj B) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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.homology ((HomologicalComplex.single C c j).toPrefunctor.obj B) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).toPrefunctor.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).toPrefunctor.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.opcycles ((HomologicalComplex.single C c j).toPrefunctor.obj B) j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.map f) j) (HomologicalComplex.singleObjOpcyclesSelfIso c j B).inv = CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv f

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

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

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] : CategoryTheory.Functor.comp (HomologicalComplex.single C c j) (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] : CategoryTheory.Functor.comp (ChainComplex.single₀ C) (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

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

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 : ℕ) : CategoryTheory.Functor.comp (ChainComplex.single₀ C) (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

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

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] : CategoryTheory.Functor.comp (CochainComplex.single₀ C) (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

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

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 : ℕ) : CategoryTheory.Functor.comp (CochainComplex.single₀ C) (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

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

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).toPrefunctor.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).toPrefunctor.obj A) (n + 1)