Documentation

Mathlib.Algebra.Homology.Functor

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) :
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' := }
@[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' := }

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 = C.asFunctor
    @[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