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₂) :
def
homological_complex.as_functor
{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 ⥤ homological_complex V c
A complex of functors gives a functor to complexes.
@[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) :
@[simp]
theorem
homological_complex.complex_of_functors_to_functor_to_complex_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) :
@[simp]
theorem
homological_complex.complex_of_functors_to_functor_to_complex_map_app_f
{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 D : homological_complex (T ⥤ V) c)
(f : C ⟶ D)
(t : T)
(i : ι) :
def
homological_complex.complex_of_functors_to_functor_to_complex
{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] :
homological_complex (T ⥤ V) c ⥤ T ⥤ homological_complex V c
The functorial version of homological_complex.as_functor.
Equations
- homological_complex.complex_of_functors_to_functor_to_complex = {obj := λ (C : homological_complex (T ⥤ V) c), C.as_functor, map := λ (C D : homological_complex (T ⥤ V) c) (f : C ⟶ D), {app := λ (t : T), {f := λ (i : ι), (f.f i).app t, comm' := _}, naturality' := _}, map_id' := _, map_comp' := _}