ofEpiOfIsIsoOfMono' — Mathlib

Lean4
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a right homology data for `S₂` induces a right homology data for `S₁` with
the same `Q` and `H` fields. This is obtained by dualising `LeftHomologyData.ofEpiOfIsIsoOfMono`.
The inverse construction is `ofEpiOfIsIsoOfMono`. -/
noncomputable def ofEpiOfIsIsoOfMono' : RightHomologyData S₁ :=
  by
  haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
  haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
  haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
  exact (LeftHomologyData.ofEpiOfIsIsoOfMono (opMap φ) h.op).unop
Похожие утверждения