English
Let f be a lattice homomorphism with a bound m on the Krull dimension of preimages under the dual map; then coheight respects the inequality coheight(x) ≤ (m+1)·coheight(f(x)) + m for all x.
Русский
Пусть f — гомоморфизм решёток и существует верхняя граница m для предобразов через двойственную карту; тогда неравенство сохраняется: coheight(x) ≤ (m+1)·coheight(f(x)) + m.
LaTeX
$$$\\forall x,\\; \\operatorname{coheight}(x) \\le (m+1) \\cdot \\operatorname{coheight}(f(x)) + m$ (при условии соответствующего предобразного ограничения).$$
Lean4
theorem coheight_le_of_krullDim_preimage_le (x : α) : Order.coheight x ≤ (m + 1) * Order.coheight (f x) + m :=
by
rw [Order.coheight, Order.coheight]
apply height_le_of_krullDim_preimage_le (f := f.dual)
exact fun x ↦ le_of_eq_of_le (krullDim_orderDual (α := f ⁻¹' { x })) (h x)
