map_comap_eq_self_of_surjective — Mathlib

English

If f is surjective, then (s.comap f).map f = s for any subfield s of L.

Русский

Если f сюръективен, то (s.comap f).map f = s для любого подполя s над L.

LaTeX

$$$$ \\text{If } f \\text{ is surjective, then } (s.\\mathrm{comap} f).\\mathrm{map} f = s.$$$$

Lean4

theorem map_comap_eq_self_of_surjective {f : K →+* L} (hf : Function.Surjective f) (s : Subfield L) :
    (s.comap f).map f = s :=
  SetLike.coe_injective (Set.image_preimage_eq _ hf)

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