# Documentation

Mathlib.Algebra.Homology.SingleHomology

# 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.

Equations
• One or more equations did not get rendered due to their size.
theorem HomologicalComplex.exactAt_single_obj {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) (i : ι) (hi : i j) :
theorem HomologicalComplex.isZero_single_obj_homology {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) (i : ι) (hi : i j) :
noncomputable def HomologicalComplex.singleObjCyclesSelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :

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.
Instances For
theorem HomologicalComplex.singleObjCyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
theorem HomologicalComplex.singleObjCyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
noncomputable def HomologicalComplex.singleObjOpcyclesSelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :

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.
Instances For
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.opcycles (().obj A) j Z) :
=
theorem HomologicalComplex.singleObjOpcyclesSelfIso_hom {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
noncomputable def HomologicalComplex.singleObjHomologySelfIso {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :

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.
Instances For
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.X (().obj A) j Z) :
=
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) :
@[simp]
theorem HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
@[simp]
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.homology (().obj A) j Z) :
@[simp]
@[simp]
theorem HomologicalComplex.singleObjCyclesSelfIso_inv_homologyπ_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.homology (().obj A) j Z) :
@[simp]
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.opcycles (().obj A) j Z) :
@[simp]
@[simp]
theorem HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : A Z) :
@[simp]
@[simp]
theorem HomologicalComplex.singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc {C : Type u} {ι : Type u_1} [] (c : ) (j : ι) (A : C) {Z : C} (h : HomologicalComplex.opcycles (().obj A) j Z) :
@[simp]
@[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 : HomologicalComplex.cycles (().obj B) 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 : HomologicalComplex.homology (().obj B) 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 : HomologicalComplex.opcycles (().obj B) 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 : ι) :

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

Equations
Instances For

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.
Instances For

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.
Instances For

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.
Instances For

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.
Instances For