English
Let A and B be subfields of E and let f: L → E be a surjective field homomorphism. Then the relrank of the preimages A^{-1}(f) and B^{-1}(f) lift to the same value as the relrank of A and B; i.e., lifting preserves relrank under a surjective pullback.
Русский
Пусть A и B — подрасширения E, а f: L → E — сюръективное гомоморфное отображение полей. Тогда relrank предобразов A и B по f равен relrank(A,B) после подъема по универсу. То есть сохранение relrank при сюръективном прообразовании.
LaTeX
$$$\\operatorname{lift}\\bigl(\\operatorname{relrank}(A^{\\downarrow f}, B^{\\downarrow f})\\bigr) = \\operatorname{lift}\\bigl(\\operatorname{relrank}(A,B)\\bigr) \\quad\\text{where } A^{\\downarrow f}=f^{-1}(A),\\; B^{\\downarrow f}=f^{-1}(B).$$$
Lean4
theorem lift_relrank_comap_comap_eq_lift_relrank_of_surjective (f : L →+* E) (h : Function.Surjective f) :
lift.{v} (relrank (A.comap f) (B.comap f)) = lift.{w} (relrank A B) :=
lift_relrank_comap_comap_eq_lift_relrank_of_le A B f fun x _ ↦ h x
