The homotopy category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι) :
hom_rel (homological_complex V c)
The congruence on homological_complex V c given by the existence of a homotopy.
Instances for homotopic
@[protected, instance]
def
homotopy_congruence
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι) :
@[protected, instance]
def
homotopy_category.category
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι) :
def
homotopy_category
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(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
- homotopy_category V c = category_theory.quotient (homotopic V c)
Instances for homotopy_category
def
homotopy_category.quotient
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι) :
homological_complex V c ⥤ homotopy_category V c
The quotient functor from complexes to the homotopy category.
Equations
@[protected, instance]
noncomputable
def
homotopy_category.inhabited
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_zero_object V] :
inhabited (homotopy_category V c)
Equations
- homotopy_category.inhabited V c = {default := (homotopy_category.quotient V c).obj 0}
@[simp]
theorem
homotopy_category.quotient_obj_as
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
(C : homological_complex V c) :
((homotopy_category.quotient V c).obj C).as = C
@[simp]
theorem
homotopy_category.quotient_map_out
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homotopy_category V c}
(f : C ⟶ D) :
(homotopy_category.quotient V c).map (quot.out f) = f
theorem
homotopy_category.eq_of_homotopy
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f g : C ⟶ D)
(h : homotopy f g) :
(homotopy_category.quotient V c).map f = (homotopy_category.quotient V c).map g
noncomputable
def
homotopy_category.homotopy_of_eq
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f g : C ⟶ D)
(w : (homotopy_category.quotient V c).map f = (homotopy_category.quotient V c).map g) :
homotopy f 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}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : C ⟶ D) :
homotopy (quot.out ((homotopy_category.quotient V c).map f)) f
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}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D E : homotopy_category V c}
(f : C ⟶ D)
(g : D ⟶ E) :
@[simp]
theorem
homotopy_category.iso_of_homotopy_equiv_hom
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : homotopy_equiv C D) :
@[simp]
theorem
homotopy_category.iso_of_homotopy_equiv_inv
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : homotopy_equiv C D) :
def
homotopy_category.iso_of_homotopy_equiv
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : homotopy_equiv C D) :
(homotopy_category.quotient V c).obj C ≅ (homotopy_category.quotient V c).obj D
Homotopy equivalent complexes become isomorphic in the homotopy category.
Equations
- homotopy_category.iso_of_homotopy_equiv f = {hom := (homotopy_category.quotient V c).map f.hom, inv := (homotopy_category.quotient V c).map f.inv, hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
homotopy_category.homotopy_equiv_of_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{c : complex_shape ι}
{C D : homological_complex V c}
(i : (homotopy_category.quotient V c).obj C ≅ (homotopy_category.quotient V c).obj D) :
homotopy_equiv C D
If two complexes become isomorphic in the homotopy category, then they were homotopy equivalent.
Equations
- homotopy_category.homotopy_equiv_of_iso i = {hom := quot.out i.hom, inv := quot.out i.inv, homotopy_hom_inv_id := homotopy_category.homotopy_of_eq (quot.out i.hom ≫ quot.out i.inv) (𝟙 C) _, homotopy_inv_hom_id := homotopy_category.homotopy_of_eq (quot.out i.inv ≫ quot.out i.hom) (𝟙 D) _}
noncomputable
def
homotopy_category.homology_functor
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι) :
homotopy_category V c ⥤ V
The i-th homology, as a functor from the homotopy category.
Equations
- homotopy_category.homology_functor V c i = category_theory.quotient.lift (homotopic V c) (homology_functor V c i) _
noncomputable
def
homotopy_category.homology_factors
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι) :
homotopy_category.quotient V c ⋙ homotopy_category.homology_functor V c i ≅ homology_functor V c i
The homology functor on the homotopy category is just the usual homology functor.
Equations
- homotopy_category.homology_factors V c i = category_theory.quotient.lift.is_lift (homotopic V c) (homology_functor V c i) _
@[simp]
theorem
homotopy_category.homology_factors_hom_app
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι)
(C : homological_complex V c) :
(homotopy_category.homology_factors V c i).hom.app C = 𝟙 ((homotopy_category.quotient V c ⋙ homotopy_category.homology_functor V c i).obj C)
@[simp]
theorem
homotopy_category.homology_factors_inv_app
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι)
(C : homological_complex V c) :
(homotopy_category.homology_factors V c i).inv.app C = 𝟙 ((homology_functor V c i).obj C)
theorem
homotopy_category.homology_functor_map_factors
{ι : Type u_1}
(V : Type u)
[category_theory.category V]
[category_theory.preadditive V]
(c : complex_shape ι)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
(i : ι)
{C D : homological_complex V c}
(f : C ⟶ D) :
(homology_functor V c i).map f = (homotopy_category.homology_functor V c i).map ((homotopy_category.quotient V c).map f)
@[simp]
theorem
category_theory.functor.map_homotopy_category_obj
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(c : complex_shape ι)
(F : V ⥤ W)
[F.additive]
(C : homotopy_category V c) :
(category_theory.functor.map_homotopy_category c F).obj C = (homotopy_category.quotient W c).obj ((F.map_homological_complex c).obj C.as)
@[simp]
theorem
category_theory.functor.map_homotopy_category_map
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(c : complex_shape ι)
(F : V ⥤ W)
[F.additive]
(C D : homotopy_category V c)
(f : C ⟶ D) :
(category_theory.functor.map_homotopy_category c F).map f = (homotopy_category.quotient W c).map ((F.map_homological_complex c).map (quot.out f))
noncomputable
def
category_theory.functor.map_homotopy_category
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(c : complex_shape ι)
(F : V ⥤ W)
[F.additive] :
homotopy_category V c ⥤ homotopy_category W c
An additive functor induces a functor between homotopy categories.
Equations
- category_theory.functor.map_homotopy_category c F = {obj := λ (C : homotopy_category V c), (homotopy_category.quotient W c).obj ((F.map_homological_complex c).obj C.as), map := λ (C D : homotopy_category V c) (f : C ⟶ D), (homotopy_category.quotient W c).map ((F.map_homological_complex c).map (quot.out f)), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.nat_trans.map_homotopy_category_app
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
{F G : V ⥤ W}
[F.additive]
[G.additive]
(α : F ⟶ G)
(c : complex_shape ι)
(C : homotopy_category V c) :
def
category_theory.nat_trans.map_homotopy_category
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
{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
- category_theory.nat_trans.map_homotopy_category α c = {app := λ (C : homotopy_category V c), (homotopy_category.quotient W c).map ((category_theory.nat_trans.map_homological_complex α c).app C.as), naturality' := _}
@[simp]
theorem
category_theory.nat_trans.map_homotopy_category_id
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(c : complex_shape ι)
(F : V ⥤ W)
[F.additive] :
@[simp]
theorem
category_theory.nat_trans.map_homotopy_category_comp
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.preadditive V]
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
(c : complex_shape ι)
{F G H : V ⥤ W}
[F.additive]
[G.additive]
[H.additive]
(α : F ⟶ G)
(β : G ⟶ H) :