mathlib3 documentation

algebra.homology.functor

Complexes in functor categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 homological_complex.as_functor_map {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} [category_theory.category T] (C : homological_complex (T V) c) (t₁ t₂ : T) (h : t₁ t₂) :
C.as_functor.map h = {f := λ (i : ι), (C.X i).map h, comm' := _}

A complex of functors gives a functor to complexes.

Equations
@[simp]
theorem homological_complex.as_functor_obj {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} [category_theory.category T] (C : homological_complex (T V) c) (t : T) :
C.as_functor.obj t = {X := λ (i : ι), (C.X i).obj t, d := λ (i j : ι), (C.d i j).app t, shape' := _, d_comp_d' := _}