# mathlib3documentation

algebra.homology.differential_object

# Homological complexes are differential graded objects. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[reducible]
def category_theory.differential_object.X_eq_to_hom {β : Type u_1} {b : β} {V : Type u_2} {i j : β} (h : i = j) :
X.X i X.X j

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 category_theory.differential_object.X_eq_to_hom_refl {β : Type u_1} {b : β} {V : Type u_2} (i : β) :
X.X_eq_to_hom _ = 𝟙 (X.X i)
@[simp]
theorem homological_complex.eq_to_hom_d {β : Type u_1} {b : β} {V : Type u_2} {x y : β} (h : x = y) :
X.X_eq_to_hom h X.d y = X.d x X.X_eq_to_hom _
@[simp]
theorem homological_complex.eq_to_hom_d_assoc {β : Type u_1} {b : β} {V : Type u_2} {x y : β} (h : x = y) {X' : V} (f' : X') :
X.X_eq_to_hom h X.d y f' = X.d x X.X_eq_to_hom _ f'
@[simp]
theorem homological_complex.d_eq_to_hom {β : Type u_1} {b : β} {V : Type u_2} (X : ) {x y z : β} (h : y = z) :
X.d x y = X.d x z
@[simp]
theorem homological_complex.d_eq_to_hom_assoc {β : Type u_1} {b : β} {V : Type u_2} (X : ) {x y z : β} (h : y = z) {X' : V} (f' : X.X z X') :
X.d x y = X.d x z f'
@[simp]
theorem homological_complex.eq_to_hom_f' {β : Type u_1} {b : β} {V : Type u_2} (f : X Y) {x y : β} (h : x = y) :
X.X_eq_to_hom h f.f y = f.f x Y.X_eq_to_hom h
@[simp]
theorem homological_complex.eq_to_hom_f'_assoc {β : Type u_1} {b : β} {V : Type u_2} (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'
noncomputable def homological_complex.dgo_to_homological_complex {β : Type u_1} (b : β) (V : Type u_2)  :

The functor from differential graded objects to homological complexes.

Equations
@[simp]
theorem homological_complex.dgo_to_homological_complex_obj_d {β : Type u_1} (b : β) (V : Type u_2) (i j : β) :
i j = dite (i + b = j) (λ (h : i + b = j), X.d i X.X_eq_to_hom _) (λ (h : ¬i + b = j), 0)
@[simp]
theorem homological_complex.dgo_to_homological_complex_obj_X {β : Type u_1} (b : β) (V : Type u_2) (i : β) :
i = X.X i
@[simp]
theorem homological_complex.dgo_to_homological_complex_map_f {β : Type u_1} (b : β) (V : Type u_2) (f : X Y) (i : β) :
i = f.f i
@[simp]
theorem homological_complex.homological_complex_to_dgo_obj_X {β : Type u_1} (b : β) (V : Type u_2) (X : ) (i : β) :
i = X.X i
@[simp]
theorem homological_complex.homological_complex_to_dgo_map_f {β : Type u_1} (b : β) (V : Type u_2) (X Y : ) (f : X Y) (i : β) :
i = f.f i
@[simp]
theorem homological_complex.homological_complex_to_dgo_obj_d {β : Type u_1} (b : β) (V : Type u_2) (X : ) (i : β) :
i = X.d i (i + 1 b)

The functor from homological complexes to differential graded objects.

Equations

The unit isomorphism for dgo_equiv_homological_complex.

Equations
@[simp]
theorem homological_complex.dgo_equiv_homological_complex_unit_iso_inv_app_f {β : Type u_1} (b : β) (V : Type u_2) (i : β) :
= 𝟙 (X.X i)
@[simp]
theorem homological_complex.dgo_equiv_homological_complex_unit_iso_hom_app_f {β : Type u_1} (b : β) (V : Type u_2) (i : β) :
= 𝟙 (X.X i)
@[simp]
theorem homological_complex.dgo_equiv_homological_complex_counit_iso_hom_app_f {β : Type u_1} (b : β) (V : Type u_2) (X : ) (i : β) :
= 𝟙 (X.X i)
noncomputable def homological_complex.dgo_equiv_homological_complex_counit_iso {β : Type u_1} (b : β) (V : Type u_2)  :

The counit isomorphism for dgo_equiv_homological_complex.

Equations
@[simp]
theorem homological_complex.dgo_equiv_homological_complex_counit_iso_inv_app_f {β : Type u_1} (b : β) (V : Type u_2) (X : ) (i : β) :
= 𝟙 (X.X i)
@[simp]
noncomputable def homological_complex.dgo_equiv_homological_complex {β : Type u_1} (b : β) (V : Type u_2)  :

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

Equations
@[simp]
@[simp]
@[simp]