krullDimLE_one_iff_of_isPrime_bot

English

In rings with KrullDimLE 0, a prime ideal yields a maximal ideal (as an instance).

Русский

В кольцах с KrullDimLE 0 простой идеал порождает максимальный идеал (как экземпляр).

LaTeX

$$$\mathrm{I.IsPrime} \Rightarrow \mathrm{I.IsMaximal}$ under $\mathrm{Ring.KrullDimLE }0 R$ as an instance.$$

Lean4

theorem krullDimLE_one_iff_of_isPrime_bot [(⊥ : Ideal R).IsPrime] :
    Ring.KrullDimLE 1 R ↔ ∀ I : Ideal R, I ≠ ⊥ → I.IsPrime → I.IsMaximal :=
  by
  letI : OrderBot (PrimeSpectrum R) := { bot := ⟨⊥, ‹_›⟩, bot_le I := bot_le (a := I.1) }
  simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one, Order.krullDim_le_one_iff_forall_isMax,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff, forall_comm (α := _ ≠ ⊥),
    ne_eq, PrimeSpectrum.ext_iff]
  rfl

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