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 _