# Documentation

Mathlib.Algebra.Homology.Homology

# 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 C.cyclesMap f i and C.boundariesMap f i.

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

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

The cycles at index i, as a subobject.

Instances For
theorem HomologicalComplex.cycles_eq_kernelSubobject {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : ) :
def HomologicalComplex.cyclesIsoKernel {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : ) :
CategoryTheory.Subobject.underlying.obj ()

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

Instances For
theorem HomologicalComplex.cycles_eq_top {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} (h : ¬) :
@[inline, reducible]
abbrev HomologicalComplex.boundaries {ι : Type u_1} {V : Type u} {c : } (C : ) (j : ι) :

The boundaries at index i, as a subobject.

Instances For
theorem HomologicalComplex.boundaries_eq_imageSubobject {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : ) :
def HomologicalComplex.boundariesIsoImage {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} (r : ) :
CategoryTheory.Subobject.underlying.obj ()

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

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

The canonical map from boundaries i to cycles i.

Instances For
@[simp]
theorem HomologicalComplex.imageToKernel_as_boundariesToCycles {ι : Type u_1} {V : Type u} {c : } (C : ) (i : ι) (h : ) :

Prefer boundariesToCycles.

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

The homology of a complex at index i.

Instances For
def HomologicalComplex.homologyIso {ι : Type u_1} {V : Type u} {c : } (C : ) {i : ι} {j : ι} {k : ι} (hij : ) (hjk : ) :
homology () () (_ : = 0)

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.

Instances For

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

Instances For

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

Instances For

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ₙ₊₁.

Instances For

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ₙ₊₁.

Instances For

Computing the cycles is functorial.

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

The morphism between cycles induced by a chain map.

Instances For
@[simp]
theorem cyclesMap_arrow_assoc {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) {Z : V} (h : Z) :
@[simp]
theorem cyclesMap_arrow_apply {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) [inst : ] (x : ().obj (CategoryTheory.Subobject.underlying.obj ())) :
theorem cyclesMap_arrow {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
@[simp]
theorem cyclesMap_id {ι : Type u_1} {V : Type u} {c : } {C₁ : } (i : ι) :
= CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj ())
@[simp]
theorem cyclesMap_comp {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } {C₃ : } (f : C₁ C₂) (g : C₂ C₃) (i : ι) :
@[simp]
theorem cyclesFunctor_obj {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().obj C = CategoryTheory.Subobject.underlying.obj ()
@[simp]
theorem cyclesFunctor_map {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C₁ : } {C₂ : } (f : C₁ C₂) :
().map f =
def cyclesFunctor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

Cycles as a functor.

Instances For

Computing the boundaries is functorial.

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

The morphism between boundaries induced by a chain map.

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 ()
def boundariesFunctor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

Boundaries as a functor.

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 () Z) :
@[simp]
theorem boundariesToCycles_naturality {ι : Type u_1} {V : Type u} {c : } {C₁ : } {C₂ : } (f : C₁ C₂) (i : ι) :
@[simp]
theorem boundariesToCyclesNatTrans_app {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().app C =
def boundariesToCyclesNatTrans {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

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

Instances For
@[simp]
theorem homologyFunctor_map {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C₁ : } {C₂ : } (f : C₁ C₂) :
().map f = homology.map (_ : ) (_ : ) () () (_ : ().right = ().right)
@[simp]
theorem homologyFunctor_obj {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().obj C =
def homologyFunctor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

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

Instances For
@[simp]
theorem gradedHomologyFunctor_map {ι : Type u_1} (V : Type u) (c : ) {C : } {C' : } (f : C C') (i : ι) :
().map CategoryTheory.CategoryStruct.toQuiver () CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor C C' f i = ().map f
@[simp]
theorem gradedHomologyFunctor_obj {ι : Type u_1} (V : Type u) (c : ) (C : ) (i : ι) :
().obj CategoryTheory.CategoryStruct.toQuiver () CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor C i =

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

Instances For