iff_linearMap_rangeRestrict — Mathlib

English

Exact f g is equivalent to Exact of the restricted map range(f).subtype and g.rangeRestrict.

Русский

Точность f g эквивалентна точности ограниченного отображения range(f).subtype и g.rangeRestrict.

LaTeX

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

Lean4

/-- Two maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P` are exact if and only if the induced maps
`LinearMap.range f → N → LinearMap.range g` are exact. -/
theorem iff_linearMap_rangeRestrict : Exact f g ↔ Exact (LinearMap.range f).subtype g.rangeRestrict :=
  iff_rangeFactorization (zero_mem (LinearMap.range g))

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