English
For submodules N1 ≤ N2 of M with N2 finitely generated, equality of their images under the quotient map by m N2 implies N1 = N2.
Русский
Для подсо мнум N1 ⊆ N2 ⊆ M, с N2 конечно порожден, равенство образов под отображением на M/(m N2) влечет N1 = N2.
LaTeX
$$$ N_1.map (Submodule.mkQ (\mathfrak{m} \cdot N_2)) = N_2.map (Submodule.mkQ (\mathfrak{m} \cdot N_2)) \;\iff\; N_1 = N_2. $$$
Lean4
theorem map_mkQ_eq {N₁ N₂ : Submodule R M} (h : N₁ ≤ N₂) (h' : N₂.FG) :
N₁.map (Submodule.mkQ (𝔪 • N₂)) = N₂.map (Submodule.mkQ (𝔪 • N₂)) ↔ N₁ = N₂ :=
by
constructor
· intro hN
have : N₂ ≤ 𝔪 • N₂ ⊔ N₁ := by simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge
rw [sup_comm] at this
exact
h.antisymm
(Submodule.le_of_le_smul_of_le_jacobson_bot h' (by rw [jacobson_eq_maximalIdeal]; exact bot_ne_top) this)
· rintro rfl; simp
