Lean4
/-- Turning an object into a complex supported at `j` then applying a functor is
the same as applying the functor then forming the complex.
-/
noncomputable def singleMapHomologicalComplex (j : ι) : single W₁ c j ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single W₂ c j :=
NatIso.ofComponents
(fun X =>
{ hom := { f := fun i => if h : i = j then eqToHom (by simp [h]) else 0 }
inv := { f := fun i => if h : i = j then eqToHom (by simp [h]) else 0 }
hom_inv_id := by
ext i
dsimp
split_ifs with h
· simp
· rw [zero_comp, ← F.map_id, (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
inv_hom_id := by
ext i
dsimp
split_ifs with h
· simp
· apply (isZero_single_obj_X c j _ _ h).eq_of_src })
fun f => by
ext i
dsimp
split_ifs with h
· subst h
simp [single_map_f_self, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
· apply (isZero_single_obj_X c j _ _ h).eq_of_tgt
