English
The Krull dimension equals the supremum of coheights over α, when α is nonempty.
Русский
Размерность Крулла равна супремуму коheight элементов α, если α непусто.
LaTeX
$$\operatorname{krullDim}(\alpha) = \bigvee_{a \in \alpha} \operatorname{coheight}(a)$$
Lean4
/-- The Krull dimension is the supremum of the elements' coheights.
This version of the lemma assumes that `α` is nonempty. In this case, the coercion from `ℕ∞` to
`WithBot ℕ∞` is on the outside of the right-hand side, which is usually more convenient.
If `α` were empty, then `krullDim α = ⊥`. See `krullDim_eq_iSup_coheight` for the more general
version, with the coercion under the supremum.
-/
theorem krullDim_eq_iSup_coheight_of_nonempty [Nonempty α] : krullDim α = ↑(⨆ (a : α), coheight a) := by
simpa using krullDim_eq_iSup_height_of_nonempty (α := αᵒᵈ)
