Lean4
/-- When a right homology data `h` of a short complex `S` is preserved by a functor `F`,
this is the induced right homology data `h.map F` for the short complex `S.map F`. -/
@[simps]
noncomputable def map : (S.map F).RightHomologyData :=
by
have := IsPreservedBy.hf h F
have := IsPreservedBy.hg' h F
have wp : F.map S.f ≫ F.map h.p = 0 := by rw [← F.map_comp, h.wp, F.map_zero]
have hp := CokernelCofork.mapIsColimit _ h.hp F
let g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g (S.map F).zero)
have hg' : g' = F.map h.g' := by
apply Cofork.IsColimit.hom_ext hp
rw [Cofork.IsColimit.π_desc hp]
simp only [Cofork.π_ofπ, CokernelCofork.map_π, map_g, ← F.map_comp, p_g']
have wι : F.map h.ι ≫ g' = 0 := by rw [hg', ← F.map_comp, ι_g', F.map_zero]
have hι : IsLimit (KernelFork.ofι (F.map h.ι) wι) :=
by
let e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hg') (by simp)
refine IsLimit.postcomposeHomEquiv e _ (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)
exact Fork.ext (Iso.refl _) (by simp [e])
exact
{ Q := F.obj h.Q
H := F.obj h.H
p := F.map h.p
ι := F.map h.ι
wp := wp
hp := hp
wι := wι
hι := hι }
