map_comap_map — Mathlib

English

For a subsemigroup S of M, applying comap then map yields S again when S is stable under the adjunction; more precisely (S.map f).comap f = S when f is invertible on S.

Русский

Для подполугруппы S ⊆ M применение комапа затем мапа возвращает S, если отображение инвертируемо на S.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem map_comap_map {f : M →ₙ* N} : ((S.map f).comap f).map f = S.map f :=
  (gc_map_comap f).l_u_l_eq_l _

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