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} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.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.

Equations

• X.objEqToHom h = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.DifferentialObject.objEqToHom_refl {β : 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 : β) : X.objEqToHom ⋯ = CategoryTheory.CategoryStruct.id (X.obj i)

@[simp]

theorem CategoryTheory.DifferentialObject.objEqToHom_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)) {x : β} {y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)

@[simp]

theorem CategoryTheory.DifferentialObject.objEqToHom_d_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)) {x : β} {y : β} (h : x = y) {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h✝) (CategoryTheory.CategoryStruct.comp (X.d y) h) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h)

@[simp]

theorem CategoryTheory.DifferentialObject.d_squared_apply {β : 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)) {x : β} : CategoryTheory.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} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.DifferentialObject.eqToHom_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)} {Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x : β} {y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h)

@[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 : Y.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h✝) (CategoryTheory.CategoryStruct.comp (f.f y) h) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h✝) h)

@[simp]

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

@[simp]

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.

Equations

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

@[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 : β) : ((HomologicalComplex.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 : β) : ((HomologicalComplex.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 : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} {Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.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.

Equations

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

@[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 : β) : ((HomologicalComplex.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 : β) : ((HomologicalComplex.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 : HomologicalComplex V (ComplexShape.up' b)} {Y : HomologicalComplex V (ComplexShape.up' b)} (f : X ⟶ Y) (i : β) : ((HomologicalComplex.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)) ≅ (HomologicalComplex.dgoToHomologicalComplex b V).comp (HomologicalComplex.homologicalComplexToDGO b V)

The unit isomorphism for dgoEquivHomologicalComplex.

Equations

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

@[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 : β) : ((HomologicalComplex.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 : β) : ((HomologicalComplex.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] : (HomologicalComplex.homologicalComplexToDGO b V).comp (HomologicalComplex.dgoToHomologicalComplex b V) ≅ CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))

The counit isomorphism for dgoEquivHomologicalComplex.

Equations

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

@[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 : β) : ((HomologicalComplex.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 : β) : ((HomologicalComplex.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.

Equations

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

@[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] : (HomologicalComplex.dgoEquivHomologicalComplex b V).functor = HomologicalComplex.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] : (HomologicalComplex.dgoEquivHomologicalComplex b V).unitIso = HomologicalComplex.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] : (HomologicalComplex.dgoEquivHomologicalComplex b V).counitIso = HomologicalComplex.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] : (HomologicalComplex.dgoEquivHomologicalComplex b V).inverse = HomologicalComplex.homologicalComplexToDGO b V