map_comap_eq_self_of_surjective — Mathlib

English

If f is surjective, then for every subring t of S, (t.comap f).map f = t.

Русский

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

LaTeX

$$$\text{surjective}(f) \Rightarrow (t.comap f).map f = t$$$

Lean4

theorem map_comap_eq_self_of_surjective {f : R →+* S} (hf : Function.Surjective f) (t : Subring S) :
    (t.comap f).map f = t :=
  map_comap_eq_self <| by simp [hf]

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