exact_subtype_mkQ — Mathlib

English

For any submodule Q of N, the inclusion map Q ↪ N followed by the quotient map N → N/Q forms an exact sequence, i.e. Im(subtype) = Ker(mkQ).

Русский

Для произвольного подсообщества Q подмодуля N вложение Q ↪ N вместе с фактор-мэпом N → N/Q образуют точную последовательность: Im(subtype) = Ker(mkQ).

LaTeX

$$$$ \\operatorname{Im}(\\operatorname{Submodule.subtype} Q) = \\ker(\\operatorname{Submodule.mkQ} Q). $$$$

Lean4

theorem exact_subtype_mkQ (Q : Submodule R N) : Exact (Submodule.subtype Q) (Submodule.mkQ Q) := by
  rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]

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