map_mkQ_eq_top — Mathlib

English

For a finitely generated submodule N of a finite module M, the image of N under the quotient map by m ⊗ N is the whole quotient iff N = M.

Русский

Для подмодуля N ⊆ M, который конечно порожден, образ N в M/(m M) равен всему модулю тогда и только тогда, когда N = M.

LaTeX

$$$ N.map (Submodule.mkQ (\mathfrak{m} \cdot \top)) = \top \iff N = \top. $$$

Lean4

theorem map_mkQ_eq_top {N : Submodule R M} [Module.Finite R M] : N.map (Submodule.mkQ (𝔪 • ⊤)) = ⊤ ↔ N = ⊤ := by
  rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]

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