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_1} (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_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Congruence (homotopic V c)

Equations

• (_ : CategoryTheory.Congruence (homotopic V c)) = (_ : CategoryTheory.Congruence (homotopic V c))

def HomotopyCategory {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : Type (max (max u u_1) 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 (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] : {ι : Type u_2} → {v : ComplexShape ι} → CategoryTheory.Category.{max v u_2, max (max u v) u_2} (HomotopyCategory V v)

Equations

• instCategoryHomotopyCategory V = id inferInstance

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

Equations

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

def HomotopyCategory.quotient {ι : Type u_1} (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.instFullHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplexHomotopyCategoryInstCategoryHomotopyCategoryQuotient {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Full (HomotopyCategory.quotient V c)

Equations

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

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

Equations

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

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

Equations

• (_ : CategoryTheory.Functor.Additive (HomotopyCategory.quotient V c)) = (_ : CategoryTheory.Functor.Additive (HomotopyCategory.quotient V c))

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

Equations

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

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

Equations

• (_ : CategoryTheory.Limits.HasZeroObject (HomotopyCategory V c)) = (_ : CategoryTheory.Limits.HasZeroObject (HomotopyCategory V c))

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

@[simp]

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

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

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

def HomotopyCategory.homotopyOfEq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) (g : C ⟶ D) (w : (HomotopyCategory.quotient V c).toPrefunctor.map f = (HomotopyCategory.quotient V c).toPrefunctor.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 (_ : homotopic V c f g)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations

• HomotopyCategory.isoOfHomotopyEquiv f = CategoryTheory.Iso.mk ((HomotopyCategory.quotient V c).toPrefunctor.map f.hom) ((HomotopyCategory.quotient V c).toPrefunctor.map f.inv)

def HomotopyCategory.homotopyEquivOfIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (i : (HomotopyCategory.quotient V c).toPrefunctor.obj C ≅ (HomotopyCategory.quotient V c).toPrefunctor.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_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.MorphismProperty.IsInvertedBy (HomologicalComplex.homotopyEquivalences V c) (HomotopyCategory.quotient V c)

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

def HomotopyCategory.homology'Functor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) : CategoryTheory.Functor (HomotopyCategory V c) V

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

Equations

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

def HomotopyCategory.homology'Factors {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) : CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (HomotopyCategory.homology'Functor V c i) ≅ homology'Functor V c i

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

Equations

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

@[simp]

theorem HomotopyCategory.homology'Factors_hom_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) (C : HomologicalComplex V c) : (HomotopyCategory.homology'Factors V c i).hom.app C = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (HomotopyCategory.homology'Functor V c i)).toPrefunctor.obj C)

@[simp]

theorem HomotopyCategory.homology'Factors_inv_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) (C : HomologicalComplex V c) : (HomotopyCategory.homology'Factors V c i).inv.app C = CategoryTheory.CategoryStruct.id ((homology'Functor V c i).toPrefunctor.obj C)

theorem HomotopyCategory.homology'Functor_map_factors {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) : (homology'Functor V c i).toPrefunctor.map f = (HomotopyCategory.homology'Functor V c i).toPrefunctor.map ((HomotopyCategory.quotient V c).toPrefunctor.map f)

@[irreducible]

noncomputable def HomotopyCategory.homologyFunctor {ι : Type u_1} (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

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

@[irreducible]

noncomputable def HomotopyCategory.homologyFunctorFactors {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology V] (i : ι) : CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (HomotopyCategory.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

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

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

Equations

• (_ : CategoryTheory.Functor.Additive (HomotopyCategory.homologyFunctor V c i)) = (_ : CategoryTheory.Functor.Additive (HomotopyCategory.homologyFunctor V c i))

@[simp]

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

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

An additive functor induces a functor between homotopy categories.

Equations

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

@[simp]

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

def CategoryTheory.Functor.mapHomotopyCategoryFactors {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] (c : ComplexShape ι) : CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (CategoryTheory.Functor.mapHomotopyCategory F c) ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapHomologicalComplex F c) (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

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

@[simp]

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

def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor V W} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (c : ComplexShape ι) : CategoryTheory.Functor.mapHomotopyCategory F c ⟶ CategoryTheory.Functor.mapHomotopyCategory G 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_id {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (c : ComplexShape ι) (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] : CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.id F) c = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.mapHomotopyCategory F c)

@[simp]

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