Lean4
/-- When a left homology data `h` of a short complex `S` is preserved by a functor `F`,
this is the induced left homology data `h.map F` for the short complex `S.map F`. -/
@[simps]
noncomputable def map : (S.map F).LeftHomologyData :=
by
have := IsPreservedBy.hg h F
have := IsPreservedBy.hf' h F
have wi : F.map h.i ≫ F.map S.g = 0 := by rw [← F.map_comp, h.wi, F.map_zero]
have hi := KernelFork.mapIsLimit _ h.hi F
let f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f (S.map F).zero)
have hf' : f' = F.map h.f' :=
Fork.IsLimit.hom_ext hi
(by
rw [Fork.IsLimit.lift_ι hi]
simp only [KernelFork.map_ι, Fork.ι_ofι, map_f, ← F.map_comp, f'_i])
have wπ : f' ≫ F.map h.π = 0 := by rw [hf', ← F.map_comp, f'_π, F.map_zero]
have hπ : IsColimit (CokernelCofork.ofπ (F.map h.π) wπ) :=
by
let e : parallelPair f' 0 ≅ parallelPair (F.map h.f') 0 :=
parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hf') (by simp)
refine IsColimit.precomposeInvEquiv e _ (IsColimit.ofIsoColimit (CokernelCofork.mapIsColimit _ h.hπ' F) ?_)
exact Cofork.ext (Iso.refl _) (by simp [e])
exact
{ K := F.obj h.K
H := F.obj h.H
i := F.map h.i
π := F.map h.π
wi := wi
hi := hi
wπ := wπ
hπ := hπ }
