English
If N' is finitely generated and N' ≤ P ≤ N ⊔ I·N', with I ⊆ jacobson(0), then there exists r ∈ R such that r−1 ∈ I and r·P ≤ N.
Русский
Пусть N' является порождённой конечной тасовностью, N' ≤ P ≤ N ⊔ I·N', и I ⊆ jacobson(0). Тогда существует r ∈ R такой, что r−1 ∈ I и r·P ≤ N.
LaTeX
$$$ N'.FG \\rightarrow N' \\le P \\land P \\le N \\sqcup I \\cdot N' \\Rightarrow \\exists r \\in R, r - 1 \\in I \\land r \\cdot P \\le N $$$
Lean4
@[stacks 00DV "(3) see `Submodule.localized₀_le_localized₀_of_smul_le` for the second conclusion."]
theorem exists_sub_one_mem_and_smul_le_of_fg_of_le_sup {I : Ideal R} {N N' P : Submodule R M} (hN' : N'.FG)
(hN'le : N' ≤ P) (hNN' : P ≤ N ⊔ I • N') : ∃ r : R, r - 1 ∈ I ∧ r • P ≤ N :=
by
have hNN'' : P ≤ N ⊔ N' := le_trans hNN' (by simpa using le_trans smul_le_right le_sup_right)
have h1 : P.map N.mkQ = N'.map N.mkQ :=
by
refine le_antisymm ?_ (map_mono hN'le)
simpa using map_mono (f := N.mkQ) hNN''
have h2 : P.map N.mkQ = (I • N').map N.mkQ := by
apply le_antisymm
· simpa using map_mono (f := N.mkQ) hNN'
· rw [h1]
simp [smul_le_right]
have hle : (P.map N.mkQ) ≤ I • P.map N.mkQ := by
conv_lhs => rw [h2]
simp [← h1]
obtain ⟨r, hmem, hr⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I _ (h1 ▸ hN'.map _) hle
refine ⟨r, hmem, fun x hx ↦ ?_⟩
induction hx using Submodule.smul_inductionOn_pointwise with
| smul₀ p hp =>
rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]
exact hr _ ⟨p, hp, rfl⟩
| smul₁ _ _ _ h => exact N.smul_mem _ h
| add _ _ _ _ hx hy => exact N.add_mem hx hy
| zero => exact N.zero_mem
