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.
@[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 : ι)
:
CategoryTheory.Subobject (C.X i)
The cycles at index i, as a subobject.
Equations
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 : c.Rel i j)
:
HomologicalComplex.cycles' C 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.toPrefunctor.obj (HomologicalComplex.cycles' C 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
- One or more equations did not get rendered due to their size.
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 : ¬c.Rel 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 : ι)
:
CategoryTheory.Subobject (C.X j)
The boundaries at index i, as a subobject.
Equations
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 : c.Rel 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.toPrefunctor.obj (HomologicalComplex.boundaries C 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
- One or more equations did not get rendered due to their size.
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 : ¬c.Rel (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.toPrefunctor.obj (HomologicalComplex.boundaries C i) ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj (HomologicalComplex.cycles' C i)
The canonical map from boundaries i to cycles' i.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
HomologicalComplex.homology' C j ≅ homology' (C.d i j) (C.d j k) (_ : CategoryTheory.CategoryStruct.comp (C.d i j) (C.d 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
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 : ℕ)
:
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
Instances For
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 : ℕ)
:
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
Instances For
Computing the cycles is functorial.
@[inline, reducible]
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.toPrefunctor.obj (HomologicalComplex.cycles' C₁ i) ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj (HomologicalComplex.cycles' C₂ i)
The morphism between cycles induced by a chain map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles' C₂ i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles' C₁ i))
(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).toPrefunctor.obj
(CategoryTheory.Subobject.underlying.toPrefunctor.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)) (f.f i))
(_ :
CategoryTheory.Subobject.Factors (CategoryTheory.Limits.kernelSubobject (HomologicalComplex.dFrom C₂ i))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (HomologicalComplex.cycles' C₁ i))
(f.f i))))
x) = (f.f i) ((CategoryTheory.Subobject.arrow (HomologicalComplex.cycles' C₁ i)) 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 : ι)
:
@[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.toPrefunctor.obj (HomologicalComplex.cycles' C₁ 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).toPrefunctor.obj C = CategoryTheory.Subobject.underlying.toPrefunctor.obj (HomologicalComplex.cycles' C 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).toPrefunctor.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 : ι)
:
Cycles as a functor.
Equations
- One or more equations did not get rendered due to their size.
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.toPrefunctor.obj (HomologicalComplex.boundaries C₁ i) ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj (HomologicalComplex.boundaries C₂ i)
The morphism between boundaries induced by a chain map.
Equations
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).toPrefunctor.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).toPrefunctor.obj C = CategoryTheory.Subobject.underlying.toPrefunctor.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.
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}
[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.toPrefunctor.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
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 = HomologicalComplex.boundariesToCycles' C 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 = CategoryTheory.NatTrans.mk fun (C : HomologicalComplex V c) => HomologicalComplex.boundariesToCycles' C i
Instances For
@[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).toPrefunctor.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
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).toPrefunctor.obj C = HomologicalComplex.homology' C 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 : ι)
:
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)
[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).toPrefunctor.map f i = (homology'Functor V c i).toPrefunctor.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).toPrefunctor.obj C i = HomologicalComplex.homology' C 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]
:
The homology functor from ι-indexed complexes to ι-graded objects in V.
Equations
- One or more equations did not get rendered due to their size.