Documentation

Mathlib.Algebra.Homology.Functor

Complexes in functor categories #

We can view a complex valued in a functor category T ⥤ V as a functor from T to complexes valued in V.

Future work #

In fact this is an equivalence of categories.

@[simp]
theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_map_app_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1} {c : ComplexShape ι} {T : Type u_2} [CategoryTheory.Category.{u_3, u_2} T] :
∀ {X Y : HomologicalComplex (CategoryTheory.Functor T V) c} (f : X Y) (t : T) (i : ι), HomologicalComplex.Hom.f ((HomologicalComplex.complexOfFunctorsToFunctorToComplex.map f).app t) i = (HomologicalComplex.Hom.f f i).app t