supportDim_self_eq_ringKrullDim — Mathlib

English

With NoZeroDivisors, the equivalence for Krull dimension 1 holds for ideals that are nonzero.

Русский

С условием нет нулевых делителей, эквивалентность KrullDim 1 сохраняется для ненулевых идеалов.

LaTeX

$$$[\text{NoZeroDivisors }R] \Rightarrow Ring.KrullDimLE 1 R \iff \forall I:\mathrm{Ideal}(R), I \neq \perp \rightarrow I.IsPrime \rightarrow I.IsMaximal$$$

Lean4

theorem supportDim_self_eq_ringKrullDim : supportDim R R = ringKrullDim R :=
  by
  have : annihilator R R = ⊥ :=
    annihilator_eq_bot.mpr ((faithfulSMul_iff_algebraMap_injective R R).mpr fun {a₁ a₂} a ↦ a)
  rw [supportDim_eq_ringKrullDim_quotient_annihilator, this]
  exact (RingEquiv.ringKrullDim (RingEquiv.quotientBot R))

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