map_equiv_normalizer_eq — Mathlib

English

If H ≤ G and f: G ≃* N is an isomorphism, then the image of the normalizer equals the normalizer of the image of H.

Русский

Если H ⊆ G и f: G ≃* N — изоморфизм, тогда образ нормализатора H совпадает с нормализатором образа H в N.

LaTeX

$$$ f(H^{\\\\mathcal N}) = (f(H))^{\\\\mathcal N} $$$

Lean4

/-- The image of the normalizer is equal to the normalizer of the image of an isomorphism. -/
@[to_additive /-- The image of the normalizer is equal to the normalizer of the image of an
          isomorphism. -/
    ]
theorem map_equiv_normalizer_eq (H : Subgroup G) (f : G ≃* N) :
    H.normalizer.map f.toMonoidHom = (H.map f.toMonoidHom).normalizer :=
  by
  ext x
  simp only [mem_normalizer_iff, mem_map_equiv]
  rw [f.toEquiv.forall_congr]
  intro
  simp

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