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}
[add_comm_group β]
{b : β}
{V : Type u_2}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
{i j : β}
(h : i = 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}
[add_comm_group β]
{b : β}
{V : Type u_2}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
(i : β) :
X.X_eq_to_hom _ = 𝟙 (X.X i)
@[simp]
theorem
homological_complex.eq_to_hom_d
{β : Type u_1}
[add_comm_group β]
{b : β}
{V : Type u_2}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
{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}
[add_comm_group β]
{b : β}
{V : Type u_2}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
{x y : β}
(h : x = y)
{X' : V}
(f' : (category_theory.shift_functor (category_theory.graded_object_with_shift b V) 1).obj X.X y ⟶ 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}
[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.d x y ≫ category_theory.eq_to_hom _ = X.d x 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') :
@[simp]
theorem
homological_complex.eq_to_hom_f'
{β : 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.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}
[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'
noncomputable
def
homological_complex.dgo_to_homological_complex
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
The functor from differential graded objects to homological complexes.
Equations
- homological_complex.dgo_to_homological_complex b V = {obj := λ (X : category_theory.differential_object (category_theory.graded_object_with_shift b V)), {X := λ (i : β), X.X i, d := λ (i j : β), dite (i + b = j) (λ (h : i + b = j), X.d i ≫ X.X_eq_to_hom _) (λ (h : ¬i + b = j), 0), shape' := _, d_comp_d' := _}, map := λ (X Y : category_theory.differential_object (category_theory.graded_object_with_shift b V)) (f : X ⟶ Y), {f := f.f, comm' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
homological_complex.dgo_to_homological_complex_obj_d
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
(i j : β) :
@[simp]
theorem
homological_complex.dgo_to_homological_complex_obj_X
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
(i : β) :
((homological_complex.dgo_to_homological_complex b V).obj X).X i = X.X i
@[simp]
theorem
homological_complex.dgo_to_homological_complex_map_f
{β : 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)
(i : β) :
((homological_complex.dgo_to_homological_complex b V).map f).f i = f.f i
@[simp]
theorem
homological_complex.homological_complex_to_dgo_obj_X
{β : 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))
(i : β) :
((homological_complex.homological_complex_to_dgo b V).obj X).X i = X.X i
@[simp]
theorem
homological_complex.homological_complex_to_dgo_map_f
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X Y : homological_complex V (complex_shape.up' b))
(f : X ⟶ Y)
(i : β) :
((homological_complex.homological_complex_to_dgo b V).map f).f i = f.f i
@[simp]
theorem
homological_complex.homological_complex_to_dgo_obj_d
{β : 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))
(i : β) :
def
homological_complex.homological_complex_to_dgo
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
The functor from homological complexes to differential graded objects.
Equations
- homological_complex.homological_complex_to_dgo b V = {obj := λ (X : homological_complex V (complex_shape.up' b)), {X := λ (i : β), X.X i, d := λ (i : β), X.d i (i + 1 • b), d_squared' := _}, map := λ (X Y : homological_complex V (complex_shape.up' b)) (f : X ⟶ Y), {f := f.f, comm' := _}, map_id' := _, map_comp' := _}
noncomputable
def
homological_complex.dgo_equiv_homological_complex_unit_iso
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
The unit isomorphism for dgo_equiv_homological_complex.
Equations
- homological_complex.dgo_equiv_homological_complex_unit_iso b V = category_theory.nat_iso.of_components (λ (X : category_theory.differential_object (category_theory.graded_object_with_shift b V)), {hom := {f := λ (i : β), 𝟙 (X.X i), comm' := _}, inv := {f := λ (i : β), 𝟙 (X.X i), comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_unit_iso_inv_app_f
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
(i : β) :
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_unit_iso_hom_app_f
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
(X : category_theory.differential_object (category_theory.graded_object_with_shift b V))
(i : β) :
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_counit_iso_hom_app_f
{β : 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))
(i : β) :
noncomputable
def
homological_complex.dgo_equiv_homological_complex_counit_iso
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
The counit isomorphism for dgo_equiv_homological_complex.
Equations
- homological_complex.dgo_equiv_homological_complex_counit_iso b V = category_theory.nat_iso.of_components (λ (X : homological_complex V (complex_shape.up' b)), {hom := {f := λ (i : β), 𝟙 (X.X i), comm' := _}, inv := {f := λ (i : β), 𝟙 (X.X i), comm' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_counit_iso_inv_app_f
{β : 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))
(i : β) :
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_functor
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
noncomputable
def
homological_complex.dgo_equiv_homological_complex
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
The category of differential graded objects in V is equivalent
to the category of homological complexes in V.
Equations
- homological_complex.dgo_equiv_homological_complex b V = {functor := homological_complex.dgo_to_homological_complex b V _inst_3, inverse := homological_complex.homological_complex_to_dgo b V _inst_3, unit_iso := homological_complex.dgo_equiv_homological_complex_unit_iso b V _inst_3, counit_iso := homological_complex.dgo_equiv_homological_complex_counit_iso b V _inst_3, functor_unit_iso_comp' := _}
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_inverse
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_unit_iso_2
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :
@[simp]
theorem
homological_complex.dgo_equiv_homological_complex_counit_iso_2
{β : Type u_1}
[add_comm_group β]
(b : β)
(V : Type u_2)
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V] :