English
The height of a comap under an algebra map equals the height of the target ideal.
Русский
Высота комапа через алгебраическое отображение равна высоте целевого идеала.
LaTeX
$$$\operatorname{height}(\text{comap}) = \operatorname{height}(I).$$$
Lean4
/-- In a nontrivial commutative ring `R`, the supremum of prime heights of all prime ideals is
equal to the Krull dimension of `R`. -/
theorem sup_primeHeight_eq_ringKrullDim [Nontrivial R] :
↑(⨆ (I : Ideal R) (_ : I.IsPrime), I.primeHeight) = ringKrullDim R :=
by
rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]
apply le_antisymm
· exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, by rw [← height_eq_primeHeight]⟩
· refine iSup_mono' fun I => ?_
by_cases I_top : I = ⊤
· exact ⟨⊥, by simp [I_top]⟩
· obtain ⟨P, hP⟩ : I.minimalPrimes.Nonempty := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)
refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
exact iInf_le_of_le P (iInf_le_of_le hP le_rfl)
