mathlib documentation

algebra.homology.differential_object

Homological complexes are differential graded objects. #

We verify that a homological_complex indexed by an add_comm_group 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.

Since eq_to_hom 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 homological_complex.d_eq_to_hom {β : Type u_1} [add_comm_group β] {b : β} {V : Type u_2} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (X : homological_complex V (complex_shape.up' b)) {x y z : β} (h : y = z) :
@[simp]
theorem homological_complex.d_eq_to_hom_assoc {β : Type u_1} [add_comm_group β] {b : β} {V : Type u_2} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] (X : homological_complex V (complex_shape.up' b)) {x y z : β} (h : y = z) {X' : V} (f' : X.X z X') :
X.d x y category_theory.eq_to_hom _ f' = X.d x z f'
@[simp]
theorem homological_complex.eq_to_hom_f'_assoc {β : Type u_1} [add_comm_group β] {b : β} {V : Type u_2} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {X Y : category_theory.differential_object (category_theory.graded_object_with_shift b V)} (f : X Y) {x y : β} (h : x = y) {X' : V} (f' : Y.X y X') :
X.X_eq_to_hom h f.f y f' = f.f x Y.X_eq_to_hom h f'

The functor from differential graded objects to homological complexes.

Equations

The functor from homological complexes to differential graded objects.

Equations