# 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 ℤ)) ℤ`

.

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.

## Instances For

## Equations

- ⋯ = ⋯

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

## Instances For

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 ℤ))

## Instances For

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

## Instances For

## Equations

- ⋯ = ⋯

The isomorphism given by the very definition of `singleFunctors C`

.

## Equations

## Instances For

`HomotopyCategory.singleFunctor C n`

is induced by `CochainComplex.singleFunctor C n`

.

## Equations

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