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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] (i : ι) : CategoryTheory.Subobject (C.X i)

The cycles at index i, as a subobject.

Equations

• C.cycles' i = CategoryTheory.Limits.kernelSubobject (C.dFrom i)

theorem HomologicalComplex.cycles'_eq_kernelSubobject {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i : ι} {j : ι} (r : c.Rel i j) : C.cycles' i = CategoryTheory.Limits.kernelSubobject (C.d i j)

def HomologicalComplex.cycles'IsoKernel {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {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 (CategoryTheory.Limits.kernelSubobject (C.d i j)) ⋯ ≪≫ CategoryTheory.Limits.kernelSubobjectIso (C.d i j)

theorem HomologicalComplex.cycles_eq_top {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i : ι} (h : ¬c.Rel i (c.next i)) : C.cycles' i = ⊤

@[reducible, inline]

abbrev HomologicalComplex.boundaries {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V c) (j : ι) : CategoryTheory.Subobject (C.X j)

The boundaries at index i, as a subobject.

Equations

• C.boundaries j = CategoryTheory.Limits.imageSubobject (C.dTo j)

theorem HomologicalComplex.boundaries_eq_imageSubobject {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {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

• C.boundariesIsoImage r = (C.boundaries j).isoOfEq (CategoryTheory.Limits.imageSubobject (C.d i j)) ⋯ ≪≫ CategoryTheory.Limits.imageSubobjectIso (C.d i j)

theorem HomologicalComplex.boundaries_eq_bot {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasZeroObject V] {j : ι} (h : ¬c.Rel (c.prev j) j) : C.boundaries j = ⊥

theorem HomologicalComplex.boundaries_le_cycles' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V c) (i : ι) : C.boundaries i ≤ C.cycles' i

@[reducible, inline]

abbrev HomologicalComplex.boundariesToCycles' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V 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

• C.boundariesToCycles' i = imageToKernel (C.dTo i) (C.dFrom i) ⋯

@[simp]

theorem HomologicalComplex.imageToKernel_as_boundariesToCycles' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V 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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : HomologicalComplex V c) (i : ι) : V

The homology of a complex at index i.

Equations

• C.homology' i = homology' (C.dTo i) (C.dFrom i) ⋯

def HomologicalComplex.homology'Iso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : HomologicalComplex V 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.

def ChainComplex.homology'ZeroIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : ChainComplex V ℕ) [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage (C.d 1 0))] : HomologicalComplex.homology' C 0 ≅ CategoryTheory.Limits.cokernel (C.d 1 0)

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.

def CochainComplex.homology'ZeroIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasZeroObject V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : CochainComplex V ℕ) : HomologicalComplex.homology' C 0 ≅ CategoryTheory.Limits.kernel (C.d 0 1)

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.

def ChainComplex.homology'SuccIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : ChainComplex V ℕ) (n : ℕ) : HomologicalComplex.homology' C (n + 1) ≅ 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 = HomologicalComplex.homology'Iso C ⋯ ⋯

def CochainComplex.homology'SuccIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasCokernels V] (C : CochainComplex V ℕ) (n : ℕ) : HomologicalComplex.homology' C (n + 1) ≅ 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 = HomologicalComplex.homology'Iso C ⋯ ⋯

Computing the cycles is functorial.

@[reducible, inline]

abbrev cycles'Map {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V 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

• cycles'Map f i = (C₂.cycles' i).factorThru (CategoryTheory.CategoryStruct.comp (C₁.cycles' i).arrow (f.f i)) ⋯

@[simp]

theorem cycles'Map_arrow_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (i : ι) {Z : V} (h : C₂.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (cycles'Map f i) (CategoryTheory.CategoryStruct.comp (C₂.cycles' i).arrow h) = CategoryTheory.CategoryStruct.comp (C₁.cycles' i).arrow (CategoryTheory.CategoryStruct.comp (f.f i) h)

@[simp]

theorem cycles'Map_arrow_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (i : ι) [inst : CategoryTheory.ConcreteCategory V] (x : (CategoryTheory.forget V).obj (CategoryTheory.Subobject.underlying.obj (C₁.cycles' i))) : (C₂.cycles' i).arrow ((cycles'Map f i) x) = (f.f i) ((C₁.cycles' i).arrow x)

theorem cycles'Map_arrow {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (i : ι) : CategoryTheory.CategoryStruct.comp (cycles'Map f i) (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} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} (i : ι) : cycles'Map (CategoryTheory.CategoryStruct.id C₁) i = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (C₁.cycles' i))

@[simp]

theorem cycles'Map_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasKernels V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} {C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) : cycles'Map (CategoryTheory.CategoryStruct.comp f g) i = CategoryTheory.CategoryStruct.comp (cycles'Map f i) (cycles'Map g i)

@[simp]

theorem cycles'Functor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasKernels V] (i : ι) (C : HomologicalComplex V c) : (cycles'Functor V c i).obj C = CategoryTheory.Subobject.underlying.obj (C.cycles' i)

@[simp]

theorem cycles'Functor_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasKernels V] (i : ι) {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) : (cycles'Functor V c i).map f = cycles'Map f i

def cycles'Functor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasKernels V] (i : ι) : CategoryTheory.Functor (HomologicalComplex V c) V

Cycles as a functor.

Equations

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

Computing the boundaries is functorial.

@[reducible, inline]

abbrev boundariesMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V 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

• boundariesMap f i = CategoryTheory.Limits.imageSubobjectMap (HomologicalComplex.Hom.sqTo f i)

@[simp]

theorem boundariesFunctor_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) : (boundariesFunctor V c i).map f = CategoryTheory.Limits.imageSubobjectMap (HomologicalComplex.Hom.sqTo f i)

@[simp]

theorem boundariesFunctor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) (C : HomologicalComplex V c) : (boundariesFunctor V c i).obj C = CategoryTheory.Subobject.underlying.obj (C.boundaries i)

def boundariesFunctor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) : CategoryTheory.Functor (HomologicalComplex V c) V

Boundaries as a functor.

Equations

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

The boundariesToCycles morphisms are natural.

@[simp]

theorem boundariesToCycles'_naturality_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (i : ι) {Z : V} (h : CategoryTheory.Subobject.underlying.obj (C₂.cycles' i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (boundariesMap f i) (CategoryTheory.CategoryStruct.comp (C₂.boundariesToCycles' i) h) = CategoryTheory.CategoryStruct.comp (C₁.boundariesToCycles' i) (CategoryTheory.CategoryStruct.comp (cycles'Map f i) h)

@[simp]

theorem boundariesToCycles'_naturality {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (i : ι) : CategoryTheory.CategoryStruct.comp (boundariesMap f i) (C₂.boundariesToCycles' i) = CategoryTheory.CategoryStruct.comp (C₁.boundariesToCycles' i) (cycles'Map f i)

@[simp]

theorem boundariesToCycles'NatTrans_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) (C : HomologicalComplex V c) : (boundariesToCycles'NatTrans V c i).app C = C.boundariesToCycles' i

def boundariesToCycles'NatTrans {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] (i : ι) : boundariesFunctor V c i ⟶ cycles'Functor V c i

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

Equations

• boundariesToCycles'NatTrans V c i = { app := fun (C : HomologicalComplex V c) => C.boundariesToCycles' i, naturality := ⋯ }

@[simp]

theorem homology'Functor_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) : (homology'Functor V c i).map f = homology'.map ⋯ ⋯ (HomologicalComplex.Hom.sqTo f i) (HomologicalComplex.Hom.sqFrom f i) ⋯

@[simp]

theorem homology'Functor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) (C : HomologicalComplex V c) : (homology'Functor V c i).obj C = C.homology' i

def homology'Functor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) : CategoryTheory.Functor (HomologicalComplex V c) V

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

Equations

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

@[simp]

theorem gradedHomology'Functor_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] {C : HomologicalComplex V c} {C' : HomologicalComplex V c} (f : C ⟶ C') (i : ι) : (gradedHomology'Functor V c).map f i = (homology'Functor V c i).map f

@[simp]

theorem gradedHomology'Functor_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (C : HomologicalComplex V c) (i : ι) : (gradedHomology'Functor V c).obj C i = C.homology' i

def gradedHomology'Functor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] : CategoryTheory.Functor (HomologicalComplex V c) (CategoryTheory.GradedObject ι V)

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

Equations

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