Lean4
/-- A functor `F : C ⥤ D` which commutes with shift functors on `C` and `D` and preserves zero
morphisms can be lifted to a functor `DifferentialObject S C ⥤ DifferentialObject S D`. -/
@[simps]
def mapDifferentialObject (F : C ⥤ D) (η : (shiftFunctor C (1 : S)).comp F ⟶ F.comp (shiftFunctor D (1 : S)))
(hF : ∀ c c', F.map (0 : c ⟶ c') = 0) : DifferentialObject S C ⥤ DifferentialObject S D
where
obj
X :=
{ obj := F.obj X.obj
d := F.map X.d ≫ η.app X.obj
d_squared := by
rw [Functor.map_comp, ← Functor.comp_map F (shiftFunctor D (1 : S))]
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] }
map
f :=
{ f := F.map f.f
comm := by
dsimp
slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
rw [Category.assoc] }
map_id := by intros; ext; simp
map_comp := by intros; ext; simp
