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)
:
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.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]
:
The functorial version of HomologicalComplex.asFunctor.
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