isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing

English

In a Noetherian local ring, an ideal I is idempotent (I^2 = I) if and only if I is either 0 or the whole ring.

Русский

В нищем локальном кольце идеал I идемпотентен (I^2 = I) тогда и только тогда, когда I = 0 или I = ⊤.

LaTeX

$$$\\text{IsIdempotentElem } I \\iff I = \\bot \\lor I = \\top$ (для локального кольца Noetherian).$$

Lean4

/-- Also see `Ideal.isIdempotentElem_iff_eq_bot_or_top` for integral domains. -/
theorem isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing {R} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (I : Ideal R) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ :=
  by
  constructor
  · intro H
    by_cases I = ⊤; · exact Or.inr ‹_›
    refine Or.inl (eq_bot_iff.mpr ?_)
    rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]
    apply le_iInf
    rintro (_ | n) <;> simp [H.pow_succ_eq]
  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]

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