relrank_comap_comap_eq_relrank_of_surjective

English

If f is surjective, then relrank is preserved when taking preimages: relrank(A^{\\downarrow f}, B^{\\downarrow f}) = relrank(A,B).

Русский

Пусть f сюръективно отображает поля. Тогда relrank подполей A и B после взятия прообраза по f равен relrank(A,B).

LaTeX

$$$\\operatorname{relrank}(f^{-1}(A), f^{-1}(B)) = \\operatorname{relrank}(A,B)\\quad(\\text{при сюръективности } f).$$$

Lean4

theorem relrank_comap_comap_eq_relrank_of_surjective {L : Type v} [Field L] (f : L →+* E) (h : Function.Surjective f) :
    relrank (A.comap f) (B.comap f) = relrank A B := by
  simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

Похожие утверждения