# The homology of a complex #

Given C : HomologicalComplex V c, we have C.cycles' i and C.boundaries i, both defined as subobjects of C.X i.

We show these are functorial with respect to chain maps, as cyclesMap' f i and boundariesMap f i.

As a consequence we construct homologyFunctor' i : HomologicalComplex V c ⥤ V, computing the i-th homology.

Note: Some definitions (specifically, names containing components homology, cycles) in this file have the suffix ' so as to allow the development of the new homology API of homological complex (starting from Algebra.Homology.ShortComplex.HomologicalComplex). It is planned that these definitions shall be removed and replaced by the new API.

@[reducible, inline]
abbrev HomologicalComplex.cycles' {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) :

The cycles at index i, as a subobject.

Equations
Instances For
theorem HomologicalComplex.cycles'_eq_kernelSubobject {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : c.Rel i j) :
C.cycles' i =
def HomologicalComplex.cycles'IsoKernel {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : c.Rel i j) :
CategoryTheory.Subobject.underlying.obj (C.cycles' i) CategoryTheory.Limits.kernel (C.d i j)

The underlying object of C.cycles' i is isomorphic to kernel (C.d i j), for any j such that Rel i j.

Equations
• C.cycles'IsoKernel r = ((C.cycles' i).isoOfEq () ).trans ()
Instances For
theorem HomologicalComplex.cycles_eq_top {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} (h : ¬c.Rel i (c.next i)) :
C.cycles' i =
@[reducible, inline]
abbrev HomologicalComplex.boundaries {ι : Type u_1} {V : Type u} {c : } (C : ) (j : ι) :

The boundaries at index i, as a subobject.

Equations
Instances For
theorem HomologicalComplex.boundaries_eq_imageSubobject {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : c.Rel i j) :
C.boundaries j = CategoryTheory.Limits.imageSubobject (C.d i j)
def HomologicalComplex.boundariesIsoImage {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : c.Rel i j) :
CategoryTheory.Subobject.underlying.obj (C.boundaries j) CategoryTheory.Limits.image (C.d i j)

The underlying object of C.boundaries j is isomorphic to image (C.d i j), for any i such that Rel i j.

Equations
Instances For
theorem HomologicalComplex.boundaries_eq_bot {ι : Type u_1} {V : Type u} {c : } (C : ) {j : ι} (h : ¬c.Rel (c.prev j) j) :
C.boundaries j =
theorem HomologicalComplex.boundaries_le_cycles' {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) :
C.boundaries i C.cycles' i
@[reducible, inline]
abbrev HomologicalComplex.boundariesToCycles' {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) :
CategoryTheory.Subobject.underlying.obj (C.boundaries i) CategoryTheory.Subobject.underlying.obj (C.cycles' i)

The canonical map from boundaries i to cycles' i.

Equations
Instances For
@[simp]
theorem HomologicalComplex.imageToKernel_as_boundariesToCycles' {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) (h : C.boundaries i C.cycles' i) :
(C.boundaries i).ofLE (C.cycles' i) h = C.boundariesToCycles' i

Prefer boundariesToCycles'.

@[reducible, inline]
abbrev HomologicalComplex.homology' {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) :
V

The homology of a complex at index i.

Equations
• C.homology' i = homology' (C.dTo i) (C.dFrom i)
Instances For
def HomologicalComplex.homology'Iso {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} {k : ι} (hij : c.Rel i j) (hjk : c.Rel j k) :
C.homology' j homology' (C.d i j) (C.d j k)

The jth homology of a homological complex (as kernel of 'the differential from Cⱼ' modulo the image of 'the differential to Cⱼ') is isomorphic to the kernel of d : Cⱼ → Cₖ modulo the image of d : Cᵢ → Cⱼ when Rel i j and Rel j k.

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

The 0th homology of a chain complex is isomorphic to the cokernel of d : C₁ ⟶ C₀.

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

The 0th cohomology of a cochain complex is isomorphic to the kernel of d : C₀ → C₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def ChainComplex.homology'SuccIso {V : Type u} (C : ) (n : ) :
homology' (C.d (n + 2) (n + 1)) (C.d (n + 1) n)

The n + 1th homology of a chain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ modulo the image of d : Cₙ₊₂ → Cₙ₊₁.

Equations
• C.homology'SuccIso n =
Instances For
def CochainComplex.homology'SuccIso {V : Type u} (C : ) (n : ) :
homology' (C.d n (n + 1)) (C.d (n + 1) (n + 2))

The n + 1th cohomology of a cochain complex (as kernel of 'the differential from Cₙ₊₁' modulo the image of 'the differential to Cₙ₊₁') is isomorphic to the kernel of d : Cₙ₊₁ → Cₙ₊₂ modulo the image of d : Cₙ → Cₙ₊₁.

Equations
• C.homology'SuccIso n =
Instances For

Computing the cycles is functorial.

@[reducible, inline]
abbrev cycles'Map {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
CategoryTheory.Subobject.underlying.obj (C₁.cycles' i) CategoryTheory.Subobject.underlying.obj (C₂.cycles' i)

The morphism between cycles induced by a chain map.

Equations
Instances For
@[simp]
theorem cycles'Map_arrow_assoc {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) {Z : V} (h : C₂.X i Z) :
@[simp]
theorem cycles'Map_arrow_apply {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) [inst : ] (x : .obj (CategoryTheory.Subobject.underlying.obj (C₁.cycles' i))) :
(C₂.cycles' i).arrow (((C₂.cycles' i).factorThru (CategoryTheory.CategoryStruct.comp (C₁.cycles' i).arrow (f.f i)) ) x) = (f.f i) ((C₁.cycles' i).arrow x)
theorem cycles'Map_arrow {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
CategoryTheory.CategoryStruct.comp () (C₂.cycles' i).arrow = CategoryTheory.CategoryStruct.comp (C₁.cycles' i).arrow (f.f i)
@[simp]
theorem cycles'Map_id {ι : Type u_1} {V : Type u} {c : } {C₁ : } (i : ι) :
= CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (C₁.cycles' i))
@[simp]
theorem cycles'Map_comp {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } {C₃ : } (f : C₁ C₂) (g : C₂ C₃) (i : ι) :
@[simp]
theorem cycles'Functor_obj {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().obj C = CategoryTheory.Subobject.underlying.obj (C.cycles' i)
@[simp]
theorem cycles'Functor_map {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C₁ : } {C₂ : } (f : C₁ C₂) :
().map f =
def cycles'Functor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

Cycles as a functor.

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

Computing the boundaries is functorial.

@[reducible, inline]
abbrev boundariesMap {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
CategoryTheory.Subobject.underlying.obj (C₁.boundaries i) CategoryTheory.Subobject.underlying.obj (C₂.boundaries i)

The morphism between boundaries induced by a chain map.

Equations
Instances For
@[simp]
theorem boundariesFunctor_map {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C₁ : } {C₂ : } (f : C₁ C₂) :
().map f =
@[simp]
theorem boundariesFunctor_obj {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().obj C = CategoryTheory.Subobject.underlying.obj (C.boundaries i)
def boundariesFunctor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

Boundaries as a functor.

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

The boundariesToCycles morphisms are natural.

@[simp]
theorem boundariesToCycles'_naturality_assoc {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) {Z : V} (h : CategoryTheory.Subobject.underlying.obj (C₂.cycles' i) Z) :
CategoryTheory.CategoryStruct.comp () (CategoryTheory.CategoryStruct.comp (C₂.boundariesToCycles' i) h) = CategoryTheory.CategoryStruct.comp (C₁.boundariesToCycles' i) ()
@[simp]
theorem boundariesToCycles'_naturality {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
CategoryTheory.CategoryStruct.comp () (C₂.boundariesToCycles' i) = CategoryTheory.CategoryStruct.comp (C₁.boundariesToCycles' i) ()
@[simp]
theorem boundariesToCycles'NatTrans_app {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().app C = C.boundariesToCycles' i
def boundariesToCycles'NatTrans {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

The natural transformation from the boundaries functor to the cycles functor.

Equations
• = { app := fun (C : ) => C.boundariesToCycles' i, naturality := }
Instances For
@[simp]
theorem homology'Functor_map {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C₁ : } {C₂ : } (f : C₁ C₂) :
().map f =
@[simp]
theorem homology'Functor_obj {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().obj C = C.homology' i
def homology'Functor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

The i-th homology, as a functor to V.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem gradedHomology'Functor_map {ι : Type u_1} (V : Type u) (c : ) {C : } {C' : } (f : C C') (i : ι) :
().map f i = ().map f
@[simp]
theorem gradedHomology'Functor_obj {ι : Type u_1} (V : Type u) (c : ) (C : ) (i : ι) :
().obj C i = C.homology' i

The homology functor from ι-indexed complexes to ι-graded objects in V.

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