map_comap_eq_self_of_surjective — Mathlib

English

If the algebra homomorphism f is surjective, then (S.comap f).map f = S for all S.

Русский

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

LaTeX

$$$\text{Surjective}(f) \Rightarrow (S.comap f).map f = S$$$

Lean4

theorem map_comap_eq_self_of_surjective {f : L →ₐ[K] L'} (hf : Function.Surjective f) (S : IntermediateField K L') :
    (S.comap f).map f = S :=
  SetLike.coe_injective (Set.image_preimage_eq _ hf)

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