mathlibdocumentation

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 homological_complex.as_functor_map {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} (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' := _}
def homological_complex.as_functor {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} (C : homological_complex (T V) c) :
T

A complex of functors gives a functor to complexes.

Equations
@[simp]
theorem homological_complex.as_functor_obj {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} (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' := _}
@[simp]
theorem homological_complex.complex_of_functors_to_functor_to_complex_obj {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} (C : homological_complex (T V) c) :
@[simp]
theorem homological_complex.complex_of_functors_to_functor_to_complex_map_app_f {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2} (C D : homological_complex (T V) c) (f : C D) (t : T) (i : ι) :
= (f.f i).app t
def homological_complex.complex_of_functors_to_functor_to_complex {V : Type u} {ι : Type u_1} {c : complex_shape ι} {T : Type u_2}  :

The functorial version of homological_complex.as_functor.

Equations