Lean4
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a left homology data for `S₁` induces a left homology data for `S₂` with
the same `K` and `H` fields. The inverse construction is `ofEpiOfIsIsoOfMono'`. -/
@[simps]
noncomputable def ofEpiOfIsIsoOfMono (φ : S₁ ⟶ S₂) (h : LeftHomologyData S₁) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
LeftHomologyData S₂ := by
let i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
have wi : i ≫ S₂.g = 0 := by simp only [i, assoc, φ.comm₂₃, h.wi_assoc, zero_comp]
have hi : IsLimit (KernelFork.ofι i wi) :=
KernelFork.IsLimit.ofι _ _
(fun x hx =>
h.liftK (x ≫ inv φ.τ₂)
(by rw [assoc, ← cancel_mono φ.τ₃, assoc, assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, hx, zero_comp]))
(fun x hx => by simp [i])
(fun x hx b hb => by
dsimp
rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, liftK_i_assoc, assoc, IsIso.inv_hom_id, comp_id, hb])
let f' := hi.lift (KernelFork.ofι S₂.f S₂.zero)
have hf' : φ.τ₁ ≫ f' = h.f' :=
by
have eq := @Fork.IsLimit.lift_ι _ _ _ _ _ _ _ ((KernelFork.ofι S₂.f S₂.zero)) hi
simp only [Fork.ι_ofι] at eq
rw [← cancel_mono h.i, ← cancel_mono φ.τ₂, assoc, assoc, eq, f'_i, φ.comm₁₂]
have wπ : f' ≫ h.π = 0 := by rw [← cancel_epi φ.τ₁, comp_zero, reassoc_of% hf', h.f'_π]
have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) :=
CokernelCofork.IsColimit.ofπ _ _ (fun x hx => h.descH x (by rw [← hf', assoc, hx, comp_zero])) (fun x hx => by simp)
(fun x hx b hb => by rw [← cancel_epi h.π, π_descH, hb])
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, hπ⟩
