exact_iff_mono_g' — Mathlib

English

For RightHomologyData h, monomorphism of g' follows from exactness.

Русский

Из точности следует монообразность g'.

LaTeX

$$$ Mono\\; h.g' $$$

Lean4

theorem exact_iff_mono_g' [S.HasHomology] (h : RightHomologyData S) : S.Exact ↔ Mono h.g' :=
  by
  constructor
  · intro hS
    exact hS.mono_g' h
  · intro
    simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_mono h.ι, ← cancel_mono h.g', id_comp, h.ι_g', zero_comp]

Похожие утверждения