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

A complex of functors gives a functor to complexes.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_obj {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] (C : ) :
HomologicalComplex.complexOfFunctorsToFunctorToComplex.obj C = C.asFunctor
@[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.complexOfFunctorsToFunctorToComplex.map f).app t).f i = (f.f i).app t
def HomologicalComplex.complexOfFunctorsToFunctorToComplex {V : Type u} {ι : Type u_1} {c : } {T : Type u_2} [] :

The functorial version of HomologicalComplex.asFunctor.

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