English
Let α be a preorder. Then the Krull dimension of α equals the supremum over all elements a of α of the coheight of a.
Русский
Пусть α — частично упорядоченное множество. Тогда размерность Крull α равна верхней грані над ко-высотами элементов α:
LaTeX
$$$\operatorname{krullDim}(\alpha) = \sup_{a \in \alpha} \operatorname{coheight}(a)$$$
Lean4
/-- The Krull dimension is the supremum of the elements' coheights.
If `α` is `Nonempty`, then `krullDim_eq_iSup_coheight_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
-/
theorem krullDim_eq_iSup_coheight : krullDim α = ⨆ (a : α), ↑(coheight a) := by
cases isEmpty_or_nonempty α with
| inl h => rw [krullDim_eq_bot, ciSup_of_empty]
| inr h => rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]
