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.

def HomologicalComplex.asFunctor {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] (C : HomologicalComplex (CategoryTheory.Functor T V) c) : CategoryTheory.Functor T (HomologicalComplex V c)

A complex of functors gives a functor to complexes.

Equations

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

@[simp]

theorem HomologicalComplex.asFunctor_map {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] (C : HomologicalComplex (CategoryTheory.Functor T V) c) : ∀ {X Y : T} (h : X ⟶ Y), C.asFunctor.map h = { f := fun (i : ι) => (C.X i).map h, comm' := ⋯ }

@[simp]

theorem HomologicalComplex.asFunctor_obj {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] (C : HomologicalComplex (CategoryTheory.Functor T V) 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' := ⋯ }

def HomologicalComplex.complexOfFunctorsToFunctorToComplex {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] : CategoryTheory.Functor (HomologicalComplex (CategoryTheory.Functor T V) c) (CategoryTheory.Functor T (HomologicalComplex V c))

The functorial version of HomologicalComplex.asFunctor.

Equations

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

@[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.complexOfFunctorsToFunctorToComplex.map f).app t).f i = (f.f i).app t

@[simp]

theorem HomologicalComplex.complexOfFunctorsToFunctorToComplex_obj {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] (C : HomologicalComplex (CategoryTheory.Functor T V) c) : HomologicalComplex.complexOfFunctorsToFunctorToComplex.obj C = C.asFunctor