English
Let f be a surjective algebra hom between commutative R-algebras A and A'. Then the lifted transcendence degree of A' is at most that of A.
Русский
Пусть f: A → A' будет сюръективным алгебраическим гомом над R для коммутативных колец A и A'. Тогда поднятая трансцендентная степень (над R) A' не превосходит поднятую трансцендентную степень A.
LaTeX
$$$\forall f : A \to_R A',\ \text{Surjective}(f) \Rightarrow \lift(\trdeg R A') \le \lift(\trdeg R A).$$$
Lean4
theorem lift_trdeg_le_of_surjective (f : A →ₐ[R] A') (hf : Surjective f) :
lift.{v} (trdeg R A') ≤ lift.{v'} (trdeg R A) :=
by
nontriviality R
rw [trdeg, lift_iSup (bddAbove_range _)]
refine ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <| of_comp f ?_)
convert i.2; simp [invFun_eq (hf _)]
