map_normalClosure — Mathlib

English

The image of the normal closure under a surjective map equals the normal closure of the image.

Русский

Образ нормального замыкания через сюръективное отображение равен нормальному замыканию образа.

LaTeX

$$$ (\\\\mathrm{normalClosure} s).map f = \\\\mathrm{normalClosure} (f '' s) $$$

Lean4

theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
    (normalClosure s).map f = normalClosure (f '' s) :=
  by
  have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
  apply le_antisymm
  · simp [map_le_iff_le_comap, normalClosure_le_normal, coe_comap, ← Set.image_subset_iff, subset_normalClosure]
  · exact normalClosure_le_normal (Set.image_mono subset_normalClosure)

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