# 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.asFunctor_obj {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] (C : ) (t : T) :
().obj t = HomologicalComplex.mk (fun i => ().obj t) fun i j => ().app t
@[simp]
theorem HomologicalComplex.asFunctor_map {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] (C : ) :
∀ {X Y : T} (h : X Y), ().map h = HomologicalComplex.Hom.mk fun i => ().map h
def HomologicalComplex.asFunctor {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] (C : ) :

A complex of functors gives a functor to complexes.

Instances For
@[simp]
theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_obj {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] (C : ) :
HomologicalComplex.complexOfFunctorsToFunctorToComplex.obj C =
@[simp]
theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_map_app_f {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] :
∀ {X Y : } (f : X Y) (t : T) (i : ι), HomologicalComplex.Hom.f ((HomologicalComplex.complexOfFunctorsToFunctorToComplex.map f).app t) i = ().app t
def HomologicalComplex.complexOfFunctorsToFunctorToComplex {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] :

The functorial version of HomologicalComplex.asFunctor.

Instances For