exact_map_mkQ_range — Mathlib

English

Let f: M → N be linear. Then the pair f and the quotient map mkQ(range f) is exact, i.e. Im(f) = Ker(mkQ(range f)).

Русский

Пусть f: M → N — линейное. Тогда пара f и переходная карта mkQ( ran f ) образуют точную пару, то есть Im(f) = Ker(mkQ(ran f)).

LaTeX

$$$$ \\operatorname{Im}(f) = \\ker\\big( \\operatorname{mkQ}( \\operatorname{ran} f ) \\big). $$$$

Lean4

theorem exact_map_mkQ_range (f : M →ₗ[R] N) : Exact f (Submodule.mkQ (range f)) :=
  exact_iff.mpr <| Submodule.ker_mkQ _

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