Single functors from the homotopy category

Let C be a preadditive category with a zero object. In this file, we put together all the single functors C ⥤ CochainComplex C ℤ along with their compatibilities with shifts into the definition CochainComplex.singleFunctors C : SingleFunctors C (CochainComplex C ℤ) ℤ. Similarly, we define HomotopyCategory.singleFunctors C : SingleFunctors C (HomotopyCategory C (ComplexShape.up ℤ)) ℤ.

noncomputable def CochainComplex.singleFunctors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.SingleFunctors C (CochainComplex C ℤ) ℤ

The collection of all single functors C ⥤ CochainComplex C ℤ along with their compatibilites with shifts. (This definition has purposely no simps attribute, as the generated lemmas would not be very useful.)

Equations

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

instance CochainComplex.instAdditiveIntFunctorSingleFunctors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : ((CochainComplex.singleFunctors C).functor n).Additive

@[reducible, inline]

noncomputable abbrev CochainComplex.singleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : CategoryTheory.Functor C (CochainComplex C ℤ)

The single functor C ⥤ CochainComplex C ℤ which sends X to the complex consisting of X in degree n : ℤ and zero otherwise. (This is definitionally equal to HomologicalComplex.single C (up ℤ) n, but singleFunctor C n is the preferred term when interactions with shifts are relevant.)

Equations

• CochainComplex.singleFunctor C n = (CochainComplex.singleFunctors C).functor n

noncomputable def HomotopyCategory.singleFunctors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.SingleFunctors C (HomotopyCategory C (ComplexShape.up ℤ)) ℤ

The collection of all single functors C ⥤ HomotopyCategory C (ComplexShape.up ℤ)) for n : ℤ along with their compatibilites with shifts.

Equations

• HomotopyCategory.singleFunctors C = (CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

@[reducible, inline]

noncomputable abbrev HomotopyCategory.singleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.up ℤ))

The single functor C ⥤ HomotopyCategory C (ComplexShape.up ℤ) which sends X to the complex consisting of X in degree n : ℤ and zero otherwise.

Equations

• HomotopyCategory.singleFunctor C n = (HomotopyCategory.singleFunctors C).functor n

instance HomotopyCategory.instAdditiveIntUpSingleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : (HomotopyCategory.singleFunctor C n).Additive

noncomputable def HomotopyCategory.singleFunctorsPostcompQuotientIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : HomotopyCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

The isomorphism given by the very definition of singleFunctors C.

Equations

• HomotopyCategory.singleFunctorsPostcompQuotientIso C = CategoryTheory.Iso.refl (HomotopyCategory.singleFunctors C)

noncomputable def HomotopyCategory.singleFunctorPostcompQuotientIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (n : ℤ) : HomotopyCategory.singleFunctor C n ≅ (CochainComplex.singleFunctor C n).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))

HomotopyCategory.singleFunctor C n is induced by CochainComplex.singleFunctor C n.

Equations

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