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.

source

@[inline, reducible]

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) :

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.

Instances For

source

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

CategoryTheory.DifferentialObject.objEqToHom X (_ : i = i) = CategoryTheory.CategoryStruct.id (CategoryTheory.DifferentialObject.obj ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) X i)

source

@[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.GradedObjectWithShift b V).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObjectWithShift b V) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).toPrefunctor X.obj y ⟶ Z) :

source

@[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) :

source

@[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.GradedObjectWithShift b V).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObjectWithShift b V) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).toPrefunctor X.obj ((fun b => b + { as := 1 }.as • b) x) ⟶ Z) :

source

@[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 : β} :

source

@[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) :

source

@[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) :

source

@[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 : HomologicalComplex.X X z ⟶ Z) :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.d X x y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X z)) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d X x z) h

source

@[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 (HomologicalComplex.d X x y) (CategoryTheory.eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X z)) = HomologicalComplex.d X x z

source

@[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.X ((HomologicalComplex.dgoToHomologicalComplex b V).obj X) i = CategoryTheory.DifferentialObject.obj ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) X i

source

@[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.d ((HomologicalComplex.dgoToHomologicalComplex b V).obj X) i j = if h : i + b = j then CategoryTheory.CategoryStruct.comp (CategoryTheory.DifferentialObject.d ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) X i) (CategoryTheory.DifferentialObject.objEqToHom X (_ : i + 1 • b = j)) else 0

source

@[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.Hom.f ((HomologicalComplex.dgoToHomologicalComplex b V).map f) i = CategoryTheory.DifferentialObject.Hom.f ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) X Y f i

source

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.

Instances For

source

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

CategoryTheory.DifferentialObject.Hom.f ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) ((fun X => CategoryTheory.DifferentialObject.mk (fun i => HomologicalComplex.X X i) fun i => HomologicalComplex.d X i ((fun b => b + { as := 1 }.as • b) i)) X) ((fun X => CategoryTheory.DifferentialObject.mk (fun i => HomologicalComplex.X X i) fun i => HomologicalComplex.d X i ((fun b => b + { as := 1 }.as • b) i)) Y) ((HomologicalComplex.homologicalComplexToDGO b V).map f) i = HomologicalComplex.Hom.f f i

source

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

source

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

CategoryTheory.DifferentialObject.d ℤ AddGroupWithOne.toAddMonoidWithOne (CategoryTheory.GradedObjectWithShift b V) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.hasZeroMorphisms β) (CategoryTheory.GradedObject.hasShift b) ((HomologicalComplex.homologicalComplexToDGO b V).obj X) i = HomologicalComplex.d X i ((fun b => b + { as := 1 }.as • b) i)

source

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.

Instances For

source

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

source

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

source

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)) ≅ CategoryTheory.Functor.comp (HomologicalComplex.dgoToHomologicalComplex b V) (HomologicalComplex.homologicalComplexToDGO b V)

The unit isomorphism for dgoEquivHomologicalComplex.

Instances For

source

@[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.Hom.f ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).inv.app X) i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X i)

source

@[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.Hom.f ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).hom.app X) i = CategoryTheory.CategoryStruct.id (HomologicalComplex.X X i)

source

def HomologicalComplex.dgoEquivHomologicalComplexCounitIso {β : Type u_1} [AddCommGroup β] (b : β) (V : Type u_2) [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] :

CategoryTheory.Functor.comp (HomologicalComplex.homologicalComplexToDGO b V) (HomologicalComplex.dgoToHomologicalComplex b V) ≅ CategoryTheory.Functor.id (HomologicalComplex V (ComplexShape.up' b))

The counit isomorphism for dgoEquivHomologicalComplex.

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Instances For