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)
:
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))
Instances For
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 ⋯ ⋯))
Instances For
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))
Instances For
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) ⋯)
Instances For
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)