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_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)
:
@[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.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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
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
.
Equations
- One or more equations did not get rendered due to their size.