English
In a local ring with finite Krull dimension, a prime height equals the Krull dimension exactly when the prime is the maximal ideal.
Русский
В локальном кольце с конечной размерностью Крull высота primeHeight равна размерности Крull тогда и только тогда, когда данный простой идеал является максимальным.
LaTeX
$$$\text{In a local ring with finite Krull dim: }\operatorname{primeHeight}(I) = \operatorname{ringKrullDim}(R) \iff I = \text{IsLocalRing.maximalIdeal } R.$$$
Lean4
/-- For a local ring with finite Krull dimension, a prime ideal has height equal to the Krull
dimension if and only if it is the maximal ideal. -/
theorem primeHeight_eq_ringKrullDim_iff [FiniteRingKrullDim R] [IsLocalRing R] {I : Ideal R} [I.IsPrime] :
Ideal.primeHeight I = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R :=
by
constructor
· intro h
exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_primeHeight_eq_ringKrullDim h)
· rintro rfl
exact IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim
