mathlibdocumentation

algebra.homology.homotopy_category

The homotopy category #

homotopy_category V c gives the category of chain complexes of shape c in V, with chain maps identified when they are homotopic.

def homotopic {ι : Type u_1} (V : Type u) (c : complex_shape ι) :

The congruence on homological_complex V c given by the existence of a homotopy.

Equations
Instances for homotopic
@[protected, instance]
def homotopy_congruence {ι : Type u_1} (V : Type u) (c : complex_shape ι) :
@[protected, instance]
def homotopy_category.category {ι : Type u_1} (V : Type u) (c : complex_shape ι) :
def homotopy_category {ι : Type u_1} (V : Type u) (c : complex_shape ι) :
Type (max u u_1 v)

homotopy_category V c is the category of chain complexes of shape c in V, with chain maps identified when they are homotopic.

Equations
Instances for homotopy_category
def homotopy_category.quotient {ι : Type u_1} (V : Type u) (c : complex_shape ι) :

The quotient functor from complexes to the homotopy category.

Equations
@[protected, instance]
noncomputable def homotopy_category.inhabited {ι : Type u_1} (V : Type u) (c : complex_shape ι)  :
Equations
@[simp]
theorem homotopy_category.quotient_obj_as {ι : Type u_1} {V : Type u} {c : complex_shape ι} (C : c) :
.obj C).as = C
@[simp]
theorem homotopy_category.quotient_map_out {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : C D) :
(quot.out f) = f
theorem homotopy_category.eq_of_homotopy {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f g : C D) (h : g) :
f = g
noncomputable def homotopy_category.homotopy_of_eq {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f g : C D) (w : f = g) :
g

If two chain maps become equal in the homotopy category, then they are homotopic.

Equations
noncomputable def homotopy_category.homotopy_out_map {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : C D) :

An arbitrarily chosen representation of the image of a chain map in the homotopy category is homotopic to the original chain map.

Equations
@[simp]
theorem homotopy_category.quotient_map_out_comp_out {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D E : c} (f : C D) (g : D E) :
@[simp]
theorem homotopy_category.iso_of_homotopy_equiv_hom {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : D) :
@[simp]
theorem homotopy_category.iso_of_homotopy_equiv_inv {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : D) :
def homotopy_category.iso_of_homotopy_equiv {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (f : D) :
C D

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations
noncomputable def homotopy_category.homotopy_equiv_of_iso {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D : c} (i : C D) :

If two complexes become isomorphic in the homotopy category, then they were homotopy equivalent.

Equations
noncomputable def homotopy_category.homology_functor {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :
V

The i-th homology, as a functor from the homotopy category.

Equations
• = c i) _
noncomputable def homotopy_category.homology_factors {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) :

The homology functor on the homotopy category is just the usual homology functor.

Equations
@[simp]
theorem homotopy_category.homology_factors_hom_app {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
.app C = 𝟙 .obj C)
@[simp]
theorem homotopy_category.homology_factors_inv_app {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) (C : c) :
.app C = 𝟙 c i).obj C)
theorem homotopy_category.homology_functor_map_factors {ι : Type u_1} (V : Type u) (c : complex_shape ι) (i : ι) {C D : c} (f : C D) :
c i).map f = .map f)
@[simp]
theorem category_theory.functor.map_homotopy_category_obj {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) (F : V W) [F.additive] (C : c) :
@[simp]
theorem category_theory.functor.map_homotopy_category_map {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) (F : V W) [F.additive] (C D : c) (f : C D) :
noncomputable def category_theory.functor.map_homotopy_category {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) (F : V W) [F.additive] :

An additive functor induces a functor between homotopy categories.

Equations
@[simp]
theorem category_theory.nat_trans.map_homotopy_category_app {ι : Type u_1} {V : Type u} {W : Type u_2} {F G : V W} [F.additive] [G.additive] (α : F G) (c : complex_shape ι) (C : c) :
def category_theory.nat_trans.map_homotopy_category {ι : Type u_1} {V : Type u} {W : Type u_2} {F G : V W} [F.additive] [G.additive] (α : F G) (c : complex_shape ι) :

A natural transformation induces a natural transformation between the induced functors on the homotopy category.

Equations
@[simp]
theorem category_theory.nat_trans.map_homotopy_category_id {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) (F : V W) [F.additive] :
@[simp]
theorem category_theory.nat_trans.map_homotopy_category_comp {ι : Type u_1} {V : Type u} {W : Type u_2} (c : complex_shape ι) {F G H : V W} [F.additive] [G.additive] [H.additive] (α : F G) (β : G H) :