The homotopy category

HomotopyCategory 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_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : HomRel (HomologicalComplex V c)

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

Equations

• homotopic V c f g = Nonempty (Homotopy f g)

instance homotopy_congruence {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Congruence (homotopic V c)

def HomotopyCategory {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : Type (max (max u u_2) v)

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

Equations

• HomotopyCategory V c = CategoryTheory.Quotient (homotopic V c)

instance instCategoryHomotopyCategory {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Category.{max u_2 v, max (max u_2 u) v} (HomotopyCategory V c)

Equations

• instCategoryHomotopyCategory V c = id inferInstance

instance HomotopyCategory.instPreadditive {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Preadditive (HomotopyCategory V c)

Equations

• HomotopyCategory.instPreadditive V c = CategoryTheory.Quotient.preadditive (homotopic V c) ⋯

def HomotopyCategory.quotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex V c) (HomotopyCategory V c)

The quotient functor from complexes to the homotopy category.

Equations

• HomotopyCategory.quotient V c = CategoryTheory.Quotient.functor (homotopic V c)

instance HomotopyCategory.instFullHomologicalComplexQuotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : (quotient V c).Full

instance HomotopyCategory.instEssSurjHomologicalComplexQuotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : (quotient V c).EssSurj

instance HomotopyCategory.instAdditiveHomologicalComplexQuotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : (quotient V c).Additive

instance HomotopyCategory.instPreadditiveQuotientHomologicalComplexHomotopic {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Preadditive (CategoryTheory.Quotient (homotopic V c))

Equations

• HomotopyCategory.instPreadditiveQuotientHomologicalComplexHomotopic V c = inferInstance

instance HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : (CategoryTheory.Quotient.functor (homotopic V c)).Additive

instance HomotopyCategory.instLinear {R : Type u_1} [Semiring R] {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Linear R V] : CategoryTheory.Linear R (HomotopyCategory V c)

Equations

• HomotopyCategory.instLinear V c = CategoryTheory.Quotient.linear R (homotopic V c) ⋯

instance HomotopyCategory.instLinearHomologicalComplexQuotient {R : Type u_1} [Semiring R] {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Linear R V] : CategoryTheory.Functor.Linear R (quotient V c)

instance HomotopyCategory.instInhabitedOfHasZeroObject {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroObject V] : Inhabited (HomotopyCategory V c)

Equations

• HomotopyCategory.instInhabitedOfHasZeroObject V c = { default := (HomotopyCategory.quotient V c).obj 0 }

instance HomotopyCategory.instHasZeroObject {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.HasZeroObject (HomotopyCategory V c)

instance HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] : ((CategoryTheory.whiskeringLeft (HomologicalComplex V c) (HomotopyCategory V c) D).obj (quotient V c)).Full

instance HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] : ((CategoryTheory.whiskeringLeft (HomologicalComplex V c) (HomotopyCategory V c) D).obj (quotient V c)).Faithful

theorem HomotopyCategory.quotient_obj_surjective {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (X : HomotopyCategory V c) : ∃ (K : HomologicalComplex V c), (quotient V c).obj K = X

theorem HomotopyCategory.quotient_obj_as {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) : ((quotient V c).obj C).as = C

@[simp]

theorem HomotopyCategory.quotient_map_out {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomotopyCategory V c} (f : C ⟶ D) : (quotient V c).map (Quot.out f) = f

theorem HomotopyCategory.quot_mk_eq_quotient_map {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) : Quot.mk (CategoryTheory.Quotient.CompClosure (homotopic V c)) f = (quotient V c).map f

theorem HomotopyCategory.eq_of_homotopy {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (h : Homotopy f g) : (quotient V c).map f = (quotient V c).map g

def HomotopyCategory.homotopyOfEq {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (w : (quotient V c).map f = (quotient V c).map g) : Homotopy f g

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

Equations

• HomotopyCategory.homotopyOfEq f g w = Nonempty.some ⋯

def HomotopyCategory.homotopyOutMap {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D) : Homotopy (Quot.out ((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

• HomotopyCategory.homotopyOutMap f = HomotopyCategory.homotopyOfEq (Quot.out ((HomotopyCategory.quotient V c).map f)) f ⋯

theorem HomotopyCategory.quotient_map_out_comp_out {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D E : HomotopyCategory V c} (f : C ⟶ D) (g : D ⟶ E) : (quotient V c).map (CategoryTheory.CategoryStruct.comp (Quot.out f) (Quot.out g)) = CategoryTheory.CategoryStruct.comp f g

def HomotopyCategory.isoOfHomotopyEquiv {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (quotient V c).obj C ≅ (quotient V c).obj D

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations

• HomotopyCategory.isoOfHomotopyEquiv f = { hom := (HomotopyCategory.quotient V c).map f.hom, inv := (HomotopyCategory.quotient V c).map f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem HomotopyCategory.isoOfHomotopyEquiv_hom {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (isoOfHomotopyEquiv f).hom = (quotient V c).map f.hom

@[simp]

theorem HomotopyCategory.isoOfHomotopyEquiv_inv {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (isoOfHomotopyEquiv f).inv = (quotient V c).map f.inv

def HomotopyCategory.homotopyEquivOfIso {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : (quotient V c).obj C ≅ (quotient V c).obj D) : HomotopyEquiv C D

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

Equations

• One or more equations did not get rendered due to their size.

theorem HomotopyCategory.quotient_inverts_homotopyEquivalences {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : (HomologicalComplex.homotopyEquivalences V c).IsInvertedBy (quotient V c)

theorem HomotopyCategory.isZero_quotient_obj_iff {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) : CategoryTheory.Limits.IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id C) 0)

@[irreducible]

noncomputable def HomotopyCategory.homologyFunctor {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology V] (i : ι) : CategoryTheory.Functor (HomotopyCategory V c) V

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

Equations

• HomotopyCategory.homologyFunctor V c i = CategoryTheory.Quotient.lift (homotopic V c) (HomologicalComplex.homologyFunctor V c i) ⋯

@[irreducible]

noncomputable def HomotopyCategory.homologyFunctorFactors {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology V] (i : ι) : (quotient V c).comp (homologyFunctor V c i) ≅ HomologicalComplex.homologyFunctor V c i

The homology functor on the homotopy category is induced by the homology functor on homological complexes.

Equations

• HomotopyCategory.homologyFunctorFactors V c i = CategoryTheory.Quotient.lift.isLift (homotopic V c) (HomologicalComplex.homologyFunctor V c i) ⋯

instance HomotopyCategory.instAdditiveHomologyFunctor {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology V] (i : ι) : (homologyFunctor V c i).Additive

def CategoryTheory.Functor.mapHomotopyCategory {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (F : Functor V W) [F.Additive] (c : ComplexShape ι) : Functor (HomotopyCategory V c) (HomotopyCategory W c)

An additive functor induces a functor between homotopy categories.

Equations

• F.mapHomotopyCategory c = CategoryTheory.Quotient.lift (homotopic V c) ((F.mapHomologicalComplex c).comp (HomotopyCategory.quotient W c)) ⋯

@[simp]

theorem CategoryTheory.Functor.mapHomotopyCategory_obj {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (F : Functor V W) [F.Additive] (c : ComplexShape ι) (a : Quotient (homotopic V c)) : (F.mapHomotopyCategory c).obj a = (HomotopyCategory.quotient W c).obj ((F.mapHomologicalComplex c).obj a.as)

@[simp]

theorem CategoryTheory.Functor.mapHomotopyCategory_map {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (F : Functor V W) [F.Additive] {c : ComplexShape ι} {K L : HomologicalComplex V c} (f : K ⟶ L) : (F.mapHomotopyCategory c).map ((HomotopyCategory.quotient V c).map f) = (HomotopyCategory.quotient W c).map ((F.mapHomologicalComplex c).map f)

def CategoryTheory.Functor.mapHomotopyCategoryFactors {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (F : Functor V W) [F.Additive] (c : ComplexShape ι) : (HomotopyCategory.quotient V c).comp (F.mapHomotopyCategory c) ≅ (F.mapHomologicalComplex c).comp (HomotopyCategory.quotient W c)

The obvious isomorphism between HomotopyCategory.quotient V c ⋙ F.mapHomotopyCategory c and F.mapHomologicalComplex c ⋙ HomotopyCategory.quotient W c when F : V ⥤ W is an additive functor.

Equations

• F.mapHomotopyCategoryFactors c = CategoryTheory.Quotient.lift.isLift (homotopic V c) ((F.mapHomologicalComplex c).comp (HomotopyCategory.quotient W c)) ⋯

def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] {F G : Functor V W} [F.Additive] [G.Additive] (α : F ⟶ G) (c : ComplexShape ι) : F.mapHomotopyCategory c ⟶ G.mapHomotopyCategory c

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_app {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] {F G : Functor V W} [F.Additive] [G.Additive] (α : F ⟶ G) (c : ComplexShape ι) (C : HomotopyCategory V c) : (mapHomotopyCategory α c).app C = (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app C.as)

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_id {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (c : ComplexShape ι) (F : Functor V W) [F.Additive] : mapHomotopyCategory (CategoryStruct.id F) c = CategoryStruct.id (F.mapHomotopyCategory c)

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_comp {ι : Type u_2} {V : Type u} [Category.{v, u} V] [Preadditive V] {W : Type u_3} [Category.{u_4, u_3} W] [Preadditive W] (c : ComplexShape ι) {F G H : Functor V W} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) : mapHomotopyCategory (CategoryStruct.comp α β) c = CategoryStruct.comp (mapHomotopyCategory α c) (mapHomotopyCategory β c)