feat(category_theory/differential_object): lifting a functor (#6084)

From `lean-liquid`.

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

src/category_theory/differential_object.lean

@@ -104,6 +104,41 @@ lemma zero_f (P Q : differential_object C) : (0 : P ⟶ Q).f = 0 := rfl
 
 end differential_object
 
+namespace functor
+
+universes v' u'
+variables (D : Type u') [category.{v'} D]
+variables [has_zero_morphisms D] [has_shift D]
+
+/--
+A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero morphisms
+can be lifted to a functor `differential_object C ⥤ differential_object D`.
+-/
+@[simps]
+def map_differential_object (F : C ⥤ D) (η : (shift C).functor.comp F ⟶ F.comp (shift D).functor)
+  (hF : ∀ c c', F.map (0 : c ⟶ c') = 0) :
+  differential_object C ⥤ differential_object D :=
+{ obj := λ X, { X := F.obj X.X,
+    d := F.map X.d ≫ η.app X.X,
+    d_squared' := begin
+      dsimp, rw [functor.map_comp, ← functor.comp_map F (shift D).functor],
+      slice_lhs 2 3 { rw [← η.naturality X.d] },
+      rw [functor.comp_map],
+      slice_lhs 1 2 { rw [← F.map_comp, X.d_squared, hF] },
+      rw [zero_comp, zero_comp],
+    end },
+  map := λ X Y f, { f := F.map f.f,
+    comm' := begin
+      dsimp,
+      slice_lhs 2 3 { rw [← functor.comp_map F (shift D).functor, ← η.naturality f.f] },
+      slice_lhs 1 2 { rw [functor.comp_map, ← F.map_comp, f.comm, F.map_comp] },
+      rw [category.assoc]
+    end },
+  map_id' := by { intros, ext, simp },
+  map_comp' := by { intros, ext, simp }, }
+
+end functor
+
 end category_theory
 
 namespace category_theory