iff_addMonoidHom_rangeRestrict — Mathlib

English

Exactness of f,g is equivalent to exactness of the restricted range maps on ranges after factoring.

Русский

Точность f,g эквивалентна точности ограниченных отображений образов после факторизации.

LaTeX

$$$\\mathrm{Exact}(f,g) \\iff \\mathrm{Exact}(f.range.subtype, g.rangeRestrict)$$$

Lean4

/-- Two maps `f : M →+ N` and `g : N →+ P` are exact if and only if the induced maps
`AddMonoidHom.range f → N → AddMonoidHom.range g` are exact. -/
theorem iff_addMonoidHom_rangeRestrict : Exact f g ↔ Exact f.range.subtype g.rangeRestrict :=
  iff_rangeFactorization (zero_mem g.range)

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