exists_mem_and_smul_eq_self_of_fg_of_le_smul

English

Under the same Nakayama setup as above, there exists r ∈ I such that r kills every element of N and r acts as the identity on N modulo I, i.e., r·n = n for all n ∈ N.

Русский

При той же предпосылке Накоямы существует r ∈ I такое, что r убивает все элементы N и действует как единица на N по модулю I, то есть r·n = n для всех n ∈ N.

LaTeX

$$$\\exists r ∈ I, \\forall n ∈ N, r \\cdot n = n.$$$

Lean4

theorem exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
    (I : Ideal R) (N : Submodule R M) (hn : N.FG) (hin : N ≤ I • N) : ∃ r ∈ I, ∀ n ∈ N, r • n = n :=
  by
  obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin
  exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩

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