English
Under NoZeroSmulDivisors, Noetherian, finite module hypotheses, and I ≠ ⊤, the infimum of powers I^i acting on ⊤ is ⊥.
Русский
При NoZeroSmulDivisors и прочих условиях: пересечение степеней I^i действует на ⊤ даёт ⊥.
LaTeX
$$$[\\text{NoZeroSmulDivisors } R] \\rightarrow [\\text{IsNoetherianRing } R] \\rightarrow [\\text{Module.Finite } R M] \\rightarrow (I \\neq \\top) \\Rightarrow \\bigcap_{i\\in\\mathbb{N}} (I^i \\cdot \\top) = \\bot.$$$
Lean4
theorem iInf_pow_smul_eq_bot_of_noZeroSMulDivisors [IsNoetherianRing R] [NoZeroSMulDivisors R M] [Module.Finite R M]
(h : I ≠ ⊤) : (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M) = ⊥ :=
by
rw [eq_bot_iff]
intro x hx
by_contra hx'
have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x
obtain ⟨r, hr⟩ := this.mp hx
have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)
exact I.eq_top_iff_one.not.mp h (this ▸ r.prop)
