iInf_pow_smul_eq_bot_of_isLocalRing

English

If I ≤ Jacobson(⊥) in a Noetherian, finite module setting, then ∩_{i≥0} I^i ⊤ = ⊥.

Русский

Если I ≤ Jacobson(⊥) в условиях Noetherian и конечного модуля, то пересечение всех степеней ⊤ по I^i равно нулю.

LaTeX

$$$I \\leq \\mathrm{jacobson}(\\bot) \\Rightarrow \\bigcap_{i\\in\\mathbb{N}} (I^i \\cdot \\top) = \\bot.$$$

Lean4

theorem iInf_pow_smul_eq_bot_of_isLocalRing [IsNoetherianRing R] [IsLocalRing R] [Module.Finite R M] (h : I ≠ ⊤) :
    (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M) = ⊥ :=
  Ideal.iInf_pow_smul_eq_bot_of_le_jacobson _ ((le_maximalIdeal h).trans (maximalIdeal_le_jacobson _))

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