Documentation

Mathlib.Algebra.Homology.DifferentialObject

Homological complexes are differential graded objects. #

We verify that a HomologicalComplex indexed by an AddCommGroup is essentially the same thing as a differential graded object.

This equivalence is probably not particularly useful in practice; it's here to check that definitions match up as expected.

We first prove some results about differential graded objects.

Porting note: after the port, move these to their own file.

@[simp]
theorem CategoryTheory.DifferentialObject.eqToHom_f'_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X : CategoryTheory.DifferentialObject (CategoryTheory.GradedObjectWithShift b V)} {Y : CategoryTheory.DifferentialObject (CategoryTheory.GradedObjectWithShift b V)} (f : X Y) {x : β} {y : β} (h : x = y) {Z : V} (h : CategoryTheory.DifferentialObject.obj AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) Y y Z) :

The category of differential graded objects in V is equivalent to the category of homological complexes in V.

Instances For