map_centralizer_le_centralizer_image

English

For a set s ⊆ G and a monoid hom f: G →* G', the image under f of the centralizer is contained in the centralizer of the image: map(centralizer s) ≤ centralizer(f''s).

Русский

Для множества s ⊆ G и гомоморфа f: G →* G', образ центральлизатора лежит в центральлизаторе образа: map(centralizer s) ≤ centralizer(f''s).

LaTeX

$$map(centralizer(s)) \le centralizer(f '' s)$$

Lean4

@[to_additive]
theorem map_centralizer_le_centralizer_image (s : Set G) (f : G →* G') :
    (Subgroup.centralizer s).map f ≤ Subgroup.centralizer (f '' s) :=
  by
  rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩
  rw [← map_mul, ← map_mul, hg h hh]

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