feat(algebra/homology): eval and forget functors (#7742)

From LTE.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/homology/additive.lean

@@ -56,6 +56,8 @@ end homological_complex
 
 namespace homological_complex
 
+instance eval_additive (i : ι) : (eval V c i).additive := {}
+
 variables [has_zero_object V]
 
 instance cycles_additive [has_equalizers V] : (cycles_functor V c i).additive := {}

src/algebra/homology/differential_object.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import algebra.homology.homological_complex
 import category_theory.differential_object
-import category_theory.graded_object
 
 /-!
 # Homological complexes are differential graded objects.

src/algebra/homology/homological_complex.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin, Scott Morrison
 -/
 import algebra.homology.complex_shape
 import category_theory.subobject.limits
+import category_theory.graded_object
 
 /-!
 # Homological complexes.
@@ -200,12 +201,25 @@ instance [has_zero_object V] : inhabited (homological_complex V c) := ⟨0⟩
 lemma congr_hom {C D : homological_complex V c} {f g : C ⟶ D} (w : f = g) (i : ι) : f.f i = g.f i :=
 congr_fun (congr_arg hom.f w) i
 
-/--
-Picking out the `i`-th object, as a functor.
--/
-def eval_at (i : ι) : homological_complex V c ⥤ V :=
+section
+variables (V c)
+
+/-- The functor picking out the `i`-th object of a complex. -/
+@[simps] def eval (i : ι) : homological_complex V c ⥤ V :=
 { obj := λ C, C.X i,
-  map := λ C D f, f.f i }
+  map := λ C D f, f.f i, }
+
+/-- The functor forgetting the differential in a complex, obtaining a graded object. -/
+@[simps] def forget : homological_complex V c ⥤ graded_object ι V :=
+{ obj := λ C, C.X,
+  map := λ _ _ f, f.f }
+
+/-- Forgetting the differentials than picking out the `i`-th object is the same as
+just picking out the `i`-th object. -/
+@[simps] def forget_eval (i : ι) : forget V c ⋙ graded_object.eval i ≅ eval V c i :=
+nat_iso.of_components (λ X, iso.refl _) (by tidy)
+
+end
 
 open_locale classical
 noncomputable theory

src/category_theory/graded_object.lean

@@ -55,7 +55,10 @@ variables {C : Type u} [category.{v} C]
 instance category_of_graded_objects (β : Type w) : category.{(max w v)} (graded_object β C) :=
 category_theory.pi (λ _, C)
 
-
+/-- The projection of a graded object to its `i`-th component. -/
+@[simps] def eval {β : Type w} (b : β) : graded_object β C ⥤ C :=
+{ obj := λ X, X b,
+  map := λ X Y f, f b, }
 
 section
 variable (C)