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} {ι : Type u_1} [] (c : ) (j : ι) (A : C) (i : ι) :
(.obj A).HasHomology i
Equations
• =
theorem HomologicalComplex.exactAt_single_obj {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) (i : ι) (hi : i j) :
(.obj A).ExactAt i
theorem HomologicalComplex.isZero_single_obj_homology {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) (i : ι) (hi : i j) :
CategoryTheory.Limits.IsZero ((.obj A).homology i)
noncomputable def HomologicalComplex.singleObjCyclesSelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
(.obj A).cycles j A

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

Equations
• = (.obj A).iCyclesIso j (c.next j) ≪≫
Instances For
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
= CategoryTheory.CategoryStruct.comp ((.obj A).iCycles j)
theorem HomologicalComplex.singleObjCyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
.hom = CategoryTheory.CategoryStruct.comp ((.obj A).iCycles j) .hom
noncomputable def HomologicalComplex.singleObjOpcyclesSelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
A (.obj A).opcycles j

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

Equations
• = .symm ≪≫ (.obj A).pOpcyclesIso (c.prev j) j
Instances For
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).opcycles j Z) :
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
.hom = CategoryTheory.CategoryStruct.comp .inv ((.obj A).pOpcycles j)
noncomputable def HomologicalComplex.singleObjHomologySelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
(.obj A).homology j A

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

Equations
• = ((.obj A).isoHomologyπ (c.prev j) j ).symm ≪≫
Instances For
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).X j Z) :
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
CategoryTheory.CategoryStruct.comp .inv ((.obj A).iCycles j) = .inv
@[simp]
theorem HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
CategoryTheory.CategoryStruct.comp ((.obj A).homologyπ j) =
@[simp]
theorem HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
CategoryTheory.CategoryStruct.comp ((.obj A).homologyπ j) .hom = .hom
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).homology j Z) :
= CategoryTheory.CategoryStruct.comp ((.obj A).homologyπ j) h
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
= (.obj A).homologyπ j
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).opcycles j Z) :
= CategoryTheory.CategoryStruct.comp ((.obj A).iCycles j) (CategoryTheory.CategoryStruct.comp ((.obj A).pOpcycles j) h)
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
= CategoryTheory.CategoryStruct.comp ((.obj A).iCycles j) ((.obj A).pOpcycles j)
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).homology j Z) :
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
CategoryTheory.CategoryStruct.comp .inv ((.obj A).homologyπ j) = .inv
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).opcycles j Z) :
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_inv_homologyι {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
CategoryTheory.CategoryStruct.comp .inv ((.obj A).homologyι j) = .hom
@[simp]
theorem HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
CategoryTheory.CategoryStruct.comp ((.obj A).homologyι j) =
@[simp]
theorem HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
CategoryTheory.CategoryStruct.comp ((.obj A).homologyι j) .inv = .hom
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : (.obj A).opcycles j Z) :
= CategoryTheory.CategoryStruct.comp ((.obj A).homologyι j) h
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
= (.obj A).homologyι j
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : B Z) :
=
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : (.obj B).cycles j Z) :
=
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : B Z) :
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_inv_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : (.obj B).homology j Z) :
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_inv_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : (.obj B).opcycles j Z) :
@[simp]
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) {Z : C} (h : B Z) :
@[simp]
theorem HomologicalComplex.singleObjOpcyclesSelfIso_inv_naturality {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) {A : C} {B : C} (f : A B) :
@[simp]
theorem HomologicalComplex.homologyFunctorSingleIso_inv_app (C : Type u) {ι : Type u_1} [] (c : ) (j : ι) (X : C) :
.inv.app X = .inv
@[simp]
theorem HomologicalComplex.homologyFunctorSingleIso_hom_app (C : Type u) {ι : Type u_1} [] (c : ) (j : ι) (X : C) :
.hom.app X = .hom
noncomputable def HomologicalComplex.homologyFunctorSingleIso (C : Type u) {ι : Type u_1} [] (c : ) (j : ι) :
.comp

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

Equations
Instances For