English
The image of the normalizer under a homomorphism is contained in the normalizer of the image.
Русский
Образ нормализатора под гомоморфизмом содержится в нормализаторе образа.
LaTeX
$$$H.\operatorname{normalizer}.\operatorname{map}(f) \le (H.\operatorname{map}(f)).\operatorname{normalizer}$$$
Lean4
/-- The image of the normalizer is contained in the normalizer of the image. -/
@[to_additive /-- The image of the normalizer is contained in the normalizer of the image. -/
]
theorem le_normalizer_map (f : G →* N) : H.normalizer.map f ≤ (H.map f).normalizer := fun _ =>
by
simp only [and_imp, mem_map, exists_imp, mem_normalizer_iff]
rintro x hx rfl n
constructor
· rintro ⟨y, hy, rfl⟩
use x * y * x⁻¹, (hx y).1 hy
simp
· rintro ⟨y, hyH, hy⟩
use x⁻¹ * y * x
rw [hx]
simp [hy, hyH, mul_assoc]
