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}
[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)
:
(HomologicalComplex.asFunctor C).obj t = HomologicalComplex.mk (fun i => (HomologicalComplex.X C i).obj t) fun i j => (HomologicalComplex.d C i j).app t
@[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),
(HomologicalComplex.asFunctor C).map h = HomologicalComplex.Hom.mk fun i => (HomologicalComplex.X C i).map h
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)
:
A complex of functors gives a functor to complexes.
Instances For
@[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 = HomologicalComplex.asFunctor C
@[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
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]
:
The functorial version of HomologicalComplex.asFunctor.