iInf_pow_smul_eq_bot_of_le_jacobson

English

For Noetherian R and finite M, x ∈ ⋂_{i≥0} (I^i ⊤) iff ∃ r ∈ I with r·x = x.

Русский

При Noetherian R и конечном M: x принадлежит ∩_{i≥0} I^i ⊤ тогда и только тогда, когда ∃ r ∈ I такое, что r·x = x.

LaTeX

$$$x \\in \\bigcap_{i\\in\\mathbb{N}} (I^i \\cdot \\top) \\iff \\exists r \\in I, (r : R) \\cdot x = x.$$$

Lean4

theorem iInf_pow_smul_eq_bot_of_le_jacobson [IsNoetherianRing R] [Module.Finite R M] (h : I ≤ Ideal.jacobson ⊥) :
    (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M) = ⊥ := by
  rw [eq_bot_iff]
  intro x hx
  obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).mp hx
  have := isUnit_of_sub_one_mem_jacobson_bot (1 - r.1) (by simpa using h r.2)
  apply this.smul_left_cancel.mp
  simp [sub_smul, hr]

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