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 ≫ inv φ.τ₂
have wi : i ≫ S₁.g = 0 := by
rw [assoc, ← cancel_mono φ.τ₃, zero_comp, assoc, assoc, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h.wi]
have hi : IsLimit (KernelFork.ofι i wi) :=
KernelFork.IsLimit.ofι _ _ (fun x hx => h.liftK (x ≫ φ.τ₂) (by rw [assoc, φ.comm₂₃, reassoc_of% hx, zero_comp]))
(fun x hx => by simp [i])
(fun x hx b hb => by
rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, hb, liftK_i_assoc, assoc, IsIso.hom_inv_id,
comp_id])
let f' := hi.lift (KernelFork.ofι S₁.f S₁.zero)
have hf' : f' ≫ i = S₁.f := Fork.IsLimit.lift_ι _
have hf'' : f' = φ.τ₁ ≫ h.f' := by
rw [← cancel_mono h.i, ← cancel_mono (inv φ.τ₂), assoc, assoc, assoc, hf', f'_i_assoc, φ.comm₁₂_assoc,
IsIso.hom_inv_id, comp_id]
have wπ : f' ≫ h.π = 0 := by simp only [hf'', assoc, f'_π, comp_zero]
have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) :=
CokernelCofork.IsColimit.ofπ _ _
(fun x hx => h.descH x (by rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero])) (fun x hx => π_descH _ _ _)
(fun x hx b hx => by rw [← cancel_epi h.π, π_descH, hx])
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, hπ⟩
