map_comap_eq_of_surjective — Mathlib

English

Let f: M → N be a surjective monoid hom. For any submonoid S of N, the image of its comap equals S; that is, (S.comap f).map f = S.

Русский

Пусть f: M → N — сюръективный моноид-гомоморфизм. Для любого подмоноида S ⊆ N выполняется (S.comap f).map f = S.

LaTeX

$$$ \forall S \in \mathrm{Submonoid}(N), \operatorname{map} f\big(\operatorname{comap} f\, S\big) = S. $$$

Lean4

@[to_additive]
theorem map_comap_eq_of_surjective (S : Submonoid N) : (S.comap f).map f = S :=
  (giMapComap hf).l_u_eq _

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