English
If S is exact and φ boundary maps are mono, then φ.τ₂ is mono.
Русский
Если S точен и границы φ моно, то φ.τ₂ моно.
LaTeX
$$Mono(φ.τ₂)$$
Lean4
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.g = 0`
(e.g when `S₁` is of the form `S₁.X₁ ⟶ S₁.X₂ ⟶ 0`) and both `S₂.f` and `S₂.g` are zero
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ 0`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₂ ⟶ S₁.X₂ ⟶ S₂.X₂` is exact and `φ.τ₂` is an epi). -/
theorem quasiIso_iff_of_zeros' {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
(hg₂ : S₂.g = 0) : QuasiIso φ ↔ (ShortComplex.mk S₁.f φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero])).Exact ∧ Epi φ.τ₂ :=
by
rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
rotate_left
· dsimp
rw [hg₂, op_zero]
· dsimp
rw [hf₂, op_zero]
· dsimp
rw [hg₁, op_zero]
rw [← exact_unop_iff]
have : Mono φ.τ₂.op ↔ Epi φ.τ₂ := ⟨fun _ => unop_epi_of_mono φ.τ₂.op, fun _ => op_mono_of_epi _⟩
tauto
