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 = { 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}
[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 = { f := fun (i : ι) => (C.X i).map h, comm' := ⋯ }
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_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.complexOfFunctorsToFunctorToComplex.map f).app t).f i = (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.
Equations
- One or more equations did not get rendered due to their size.