English
Under a ring isomorphism, the height of the mapped ideal equals the height of the original ideal.
Русский
При кольцевом изоморфизме высота образа идеала равна высоте исходного идеала.
LaTeX
$$$\operatorname{height}(I) = \operatorname{height}(I^{\prime})$ under a RingEquiv mapping.$$
Lean4
/-- In a nontrivial commutative ring `R`, the supremum of prime heights of all maximal ideals is
equal to the Krull dimension of `R`. -/
theorem sup_primeHeight_of_maximal_eq_ringKrullDim [Nontrivial R] :
↑(⨆ (I : Ideal R) (_ : I.IsMaximal), I.primeHeight) = ringKrullDim R :=
by
rw [← Ideal.sup_primeHeight_eq_ringKrullDim, WithBot.coe_inj]
apply le_antisymm
· exact iSup_mono fun I => iSup_mono' fun hI => ⟨IsMaximal.isPrime hI, le_rfl⟩
· refine iSup_mono' fun I => ?_
obtain rfl | I_top := eq_or_ne I ⊤
· exact ⟨⊥, by grind [iSup_le_iff, Ideal.IsPrime.ne_top]⟩
· obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, primeHeight_mono hIM⟩)⟩
