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.

@[reducible, inline]

abbrev CategoryTheory.DifferentialObject.objEqToHom {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {i j : β} (h : i = j) : X.obj i ⟶ X.obj j

Since eqToHom only preserves the fact that X.X i = X.X j but not i = j, this definition is used to aid the simplifier.

@[simp]

theorem CategoryTheory.DifferentialObject.objEqToHom_refl {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) (i : β) : X.objEqToHom ⋯ = CategoryStruct.id (X.obj i)

theorem CategoryTheory.DifferentialObject.objEqToHom_d {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x y : β} (h : x = y) : CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)

theorem CategoryTheory.DifferentialObject.objEqToHom_d_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h✝ : (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z) : CategoryStruct.comp (X.objEqToHom h) (CategoryStruct.comp (X.d y) h✝) = CategoryStruct.comp (X.d x) (CategoryStruct.comp (X.objEqToHom ⋯) h✝)

@[simp]

theorem CategoryTheory.DifferentialObject.d_squared_apply {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x : β} : CategoryStruct.comp (X.d x) (X.d ((fun (b_1 : β) => b_1 + { as := 1 }.as • b) x)) = 0

@[simp]

theorem CategoryTheory.DifferentialObject.d_squared_apply_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] (X : DifferentialObject ℤ (GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) : CategoryStruct.comp (X.d x) (CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.DifferentialObject.eqToHom_f' {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) : CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryStruct.comp (f.f x) (Y.objEqToHom h)

theorem CategoryTheory.DifferentialObject.eqToHom_f'_assoc {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [Category.{u_3, u_2} V] [Limits.HasZeroMorphisms V] {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h✝ : Y.obj y ⟶ Z) : CategoryStruct.comp (X.objEqToHom h) (CategoryStruct.comp (f.f y) h✝) = CategoryStruct.comp (f.f x) (CategoryStruct.comp (Y.objEqToHom h) h✝)

theorem HomologicalComplex.d_eqToHom {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) : CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.eqToHom ⋯) = X.d x z

theorem HomologicalComplex.d_eqToHom_assoc {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) {Z : V} (h✝ : X.X z ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d x y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝) = CategoryTheory.CategoryStruct.comp (X.d x z) h✝

def HomologicalComplex.dgoToHomologicalComplex {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (HomologicalComplex V (ComplexShape.up' b))

The functor from differential graded objects to homological complexes.

@[simp]

theorem HomologicalComplex.dgoToHomologicalComplex_obj_d {β : 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)) (i j : β) : ((dgoToHomologicalComplex b V).obj X).d i j = if h : i + b = j then CategoryTheory.CategoryStruct.comp (X.d i) (X.objEqToHom ⋯) else 0

@[simp]

theorem HomologicalComplex.dgoToHomologicalComplex_obj_X {β : 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)) (i : β) : ((dgoToHomologicalComplex b V).obj X).X i = X.obj i

@[simp]

theorem HomologicalComplex.dgoToHomologicalComplex_map_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β) : ((dgoToHomologicalComplex b V).map f).f i = f.f i

def HomologicalComplex.homologicalComplexToDGO {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor (HomologicalComplex V (ComplexShape.up' b)) (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V))

The functor from homological complexes to differential graded objects.

@[simp]

theorem HomologicalComplex.homologicalComplexToDGO_obj_obj {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((homologicalComplexToDGO b V).obj X).obj i = X.X i

@[simp]

theorem HomologicalComplex.homologicalComplexToDGO_obj_d {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((homologicalComplexToDGO b V).obj X).d i = X.d i ((fun (b_1 : β) => b_1 + { as := 1 }.as • b) i)

@[simp]

theorem HomologicalComplex.homologicalComplexToDGO_map_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y) (i : β) : ((homologicalComplexToDGO b V).map f).f i = f.f i

def HomologicalComplex.dgoEquivHomologicalComplexUnitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.Functor.id (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) ≅ (dgoToHomologicalComplex b V).comp (homologicalComplexToDGO b V)

The unit isomorphism for dgoEquivHomologicalComplex.

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f {β : 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)) (i : β) : ((dgoEquivHomologicalComplexUnitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f {β : 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)) (i : β) : ((dgoEquivHomologicalComplexUnitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.obj i)

def HomologicalComplex.dgoEquivHomologicalComplexCounitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (homologicalComplexToDGO b V).comp (dgoToHomologicalComplex b V) ≅ CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))

The counit isomorphism for dgoEquivHomologicalComplex.

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((dgoEquivHomologicalComplexCounitIso b V).inv.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β) : ((dgoEquivHomologicalComplexCounitIso b V).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)

def HomologicalComplex.dgoEquivHomologicalComplex {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V) ≌ HomologicalComplex V (ComplexShape.up' b)

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

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplex_functor {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (dgoEquivHomologicalComplex b V).functor = dgoToHomologicalComplex b V

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplex_unitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (dgoEquivHomologicalComplex b V).unitIso = dgoEquivHomologicalComplexUnitIso b V

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplex_counitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (dgoEquivHomologicalComplex b V).counitIso = dgoEquivHomologicalComplexCounitIso b V

@[simp]

theorem HomologicalComplex.dgoEquivHomologicalComplex_inverse {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] : (dgoEquivHomologicalComplex b V).inverse = homologicalComplexToDGO b V