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}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{c : ComplexShape ι}
(C : HomologicalComplex V c)
[CategoryTheory.Limits.HasKernels V]
(i : ι)
:
The cycles at index i, as a subobject.
Instances For
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 : ComplexShape.Rel c i j)
:
def
HomologicalComplex.cyclesIsoKernel
{ι : 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 : ComplexShape.Rel c i j)
:
CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i) ≅ CategoryTheory.Limits.kernel (HomologicalComplex.d C 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.
Instances For
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 : ¬ComplexShape.Rel c i (ComplexShape.next c i))
:
@[inline, reducible]
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 : ι)
:
The boundaries at index i, as a subobject.
Instances For
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 : ComplexShape.Rel c 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 : ComplexShape.Rel c i j)
:
CategoryTheory.Subobject.underlying.obj (HomologicalComplex.boundaries C j) ≅ CategoryTheory.Limits.image (HomologicalComplex.d C 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.
Instances For
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 : ¬ComplexShape.Rel c (ComplexShape.prev c j) 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 : ι)
:
@[inline, reducible]
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 (HomologicalComplex.boundaries C i) ⟶ CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i)
The canonical map from boundaries i to cycles i.
Instances For
@[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 : HomologicalComplex.boundaries C i ≤ HomologicalComplex.cycles C i)
:
Prefer boundariesToCycles.
@[inline, reducible]
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.
Instances For
def
HomologicalComplex.homologyIso
{ι : 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 : ComplexShape.Rel c i j)
(hjk : ComplexShape.Rel c j k)
:
HomologicalComplex.homology C j ≅ homology (HomologicalComplex.d C i j) (HomologicalComplex.d C j k)
(_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C i j) (HomologicalComplex.d C j k) = 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
def
ChainComplex.homologyZeroIso
{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 (HomologicalComplex.d C 1 0))]
:
The 0th homology of a chain complex is isomorphic to the cokernel of d : C₁ ⟶ C₀.
Instances For
def
CochainComplex.homologyZeroIso
{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 ℕ)
:
The 0th cohomology of a cochain complex is isomorphic to the kernel of d : C₀ → C₁.
Instances For
def
ChainComplex.homologySuccIso
{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 (HomologicalComplex.d C (n + 2) (n + 1)) (HomologicalComplex.d C (n + 1) n)
(_ :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C (n + 2) (n + 1)) (HomologicalComplex.d C (n + 1) n) = 0)
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
def
CochainComplex.homologySuccIso
{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 (HomologicalComplex.d C n (n + 1)) (HomologicalComplex.d C (n + 1) (n + 2))
(_ :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.d C n (n + 1)) (HomologicalComplex.d C (n + 1) (n + 2)) = 0)
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}
[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 (HomologicalComplex.cycles C₁ i) ⟶ CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C₂ i)
The morphism between cycles induced by a chain map.
Instances For
@[simp]
theorem
cyclesMap_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 : HomologicalComplex.X C₂ i ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (cyclesMap f i)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₂ i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₁ i))
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f i) h)
@[simp]
theorem
cyclesMap_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 (HomologicalComplex.cycles C₁ i)))
:
↑(CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₂ i))
(↑(CategoryTheory.Subobject.factorThru (HomologicalComplex.cycles C₂ i)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₁ i))
(HomologicalComplex.Hom.f f i))
(_ :
CategoryTheory.Subobject.Factors (CategoryTheory.Limits.kernelSubobject (HomologicalComplex.dFrom C₂ i))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₁ i))
(HomologicalComplex.Hom.f f i))))
x) = ↑(HomologicalComplex.Hom.f f i) (↑(CategoryTheory.Subobject.arrow (HomologicalComplex.cycles C₁ i)) x)
theorem
cyclesMap_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 : ι)
:
@[simp]
theorem
cyclesMap_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 : ι)
:
cyclesMap (CategoryTheory.CategoryStruct.id C₁) i = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C₁ i))
@[simp]
theorem
cyclesMap_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 : ι)
:
cyclesMap (CategoryTheory.CategoryStruct.comp f g) i = CategoryTheory.CategoryStruct.comp (cyclesMap f i) (cyclesMap g i)
@[simp]
theorem
cyclesFunctor_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)
:
(cyclesFunctor V c i).obj C = CategoryTheory.Subobject.underlying.obj (HomologicalComplex.cycles C i)
@[simp]
theorem
cyclesFunctor_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₂)
:
(cyclesFunctor V c i).map f = cyclesMap f i
def
cyclesFunctor
{ι : Type u_1}
(V : Type u)
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
(c : ComplexShape ι)
[CategoryTheory.Limits.HasKernels V]
(i : ι)
:
Cycles as a functor.
Instances For
Computing the boundaries is functorial.
@[inline, reducible]
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 (HomologicalComplex.boundaries C₁ i) ⟶ CategoryTheory.Subobject.underlying.obj (HomologicalComplex.boundaries C₂ i)
The morphism between boundaries induced by a chain map.
Instances For
@[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 (HomologicalComplex.boundaries C 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 : ι)
:
Boundaries as a functor.
Instances For
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 (HomologicalComplex.cycles C₂ i) ⟶ Z)
:
@[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 : ι)
:
@[simp]
theorem
boundariesToCyclesNatTrans_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)
:
(boundariesToCyclesNatTrans V c i).app C = HomologicalComplex.boundariesToCycles C i
def
boundariesToCyclesNatTrans
{ι : 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 ⟶ cyclesFunctor V 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)
[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₂)
:
(homologyFunctor V c i).map f = homology.map
(_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo C₁ i) (HomologicalComplex.dFrom C₁ i) = 0)
(_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.dTo C₂ i) (HomologicalComplex.dFrom C₂ i) = 0)
(HomologicalComplex.Hom.sqTo f i) (HomologicalComplex.Hom.sqFrom f i)
(_ : (HomologicalComplex.Hom.sqTo f i).right = (HomologicalComplex.Hom.sqTo f i).right)
@[simp]
theorem
homologyFunctor_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)
:
(homologyFunctor V c i).obj C = HomologicalComplex.homology C i
def
homologyFunctor
{ι : 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 : ι)
:
The i-th homology, as a functor to V.
Instances For
@[simp]
theorem
gradedHomologyFunctor_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 : ι)
:
(HomologicalComplex V c).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject ι V)
CategoryTheory.CategoryStruct.toQuiver (gradedHomologyFunctor V c).toPrefunctor C C' f i = (homologyFunctor V c i).map f
@[simp]
theorem
gradedHomologyFunctor_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 : ι)
:
(HomologicalComplex V c).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject ι V)
CategoryTheory.CategoryStruct.toQuiver (gradedHomologyFunctor V c).toPrefunctor C i = HomologicalComplex.homology C i
def
gradedHomologyFunctor
{ι : 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]
:
The homology functor from ι-indexed complexes to ι-graded objects in V.