English
Let f be a lattice homomorphism from α to β with the property that for every x ∈ β, krullDim(f⁻¹({x})) ≤ m. Then krullDim(α) ≤ (m+1)·krullDim(β) + m.
Русский
Пусть f — гомоморфизм решёток α → β и для всех x ∈ β справедливо krullDim(f⁻¹({x})) ≤ m. Тогда krullDim(α) ≤ (m+1)·krullDim(β) + m.
LaTeX
$$$\\forall x:\\beta,\\; \\operatorname{krullDim}(f^{-1}\\{x\\}) \\le m \\Rightarrow \\operatorname{krullDim}(\\alpha) \\le (m+1)\\cdot \\operatorname{krullDim}(\\beta) + m$.$$
Lean4
theorem krullDim_le_of_krullDim_preimage_le : Order.krullDim α ≤ (m + 1) * Order.krullDim β + m :=
by
rw [Order.krullDim_eq_iSup_height, Order.krullDim_eq_iSup_height]
apply iSup_le fun x ↦ (le_trans (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)) ?_)
push_cast
apply add_le_add_right <| mul_le_mul_of_nonneg_left ?_ (right_eq_inf.mp rfl)
exact le_iSup_iff.mpr fun b a ↦ a (f x)
