English
The Krull dimension can be expressed as the supremum of height(a) + coheight(a) over a ∈ α when α nonempty.
Русский
Размерность Крулла выражается через максимум высоты и ко-высоты элементов α.
LaTeX
$$\operatorname{krullDim}(\alpha) = \bigvee_{a \in \alpha} (\operatorname{height}(a) + \operatorname{coheight}(a))$$
Lean4
/-- The Krull dimension is the supremum of the elements' height plus coheight.
-/
theorem krullDim_eq_iSup_height_add_coheight_of_nonempty [Nonempty α] :
krullDim α = ↑(⨆ (a : α), height a + coheight a) :=
by
apply le_antisymm
· rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_le_coe]
apply ciSup_mono (by bddDefault) (by simp)
· wlog hnottop : krullDim α < ⊤
· simp_all
rw [krullDim_eq_iSup_length, WithBot.coe_le_coe]
apply iSup_le
intro a
have : height a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (height_le_krullDim a) hnottop)
have : coheight a < ⊤ := WithBot.coe_lt_coe.mp (lt_of_le_of_lt (coheight_le_krullDim a) hnottop)
cases hh : height a with
| top => simp_all
| coe n =>
cases hch : coheight a with
| top => simp_all
| coe m =>
obtain ⟨p₁, hlast, hlen₁⟩ := exists_series_of_height_eq_coe a hh
obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch
apply le_iSup_of_le ((p₁.smash p₂) (by simp [*])) (by simp [*])
