map_comap_eq_self_of_surjective — Mathlib

English

If f is surjective, pulling back then pushing forward along f returns S for any S.

Русский

Если f сюръективен, то возврат к подпалгебре и повторное отображение возвращают S.

LaTeX

$$$ (S.comap f).map f = S $$$

Lean4

theorem map_comap_eq_self_of_surjective {f : A →ₐ[R] B} (hf : Function.Surjective f) (S : Subalgebra R B) :
    (S.comap f).map f = S :=
  map_comap_eq_self <| by simp [(AlgHom.range_eq_top f).2 hf]

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