comap_normalizer_eq_of_surjective

English

If H ≤ G and f: N →* G is surjective, then the preimage of the normalizer equals the normalizer of the preimage.

Русский

Пусть H ⊆ G и f: N →* G сюръективно. Тогда предобраз нормализатора H равен нормализатору предобраза H.

LaTeX

$$$ f^{-1}(\\\\mathcal{N}_G(H)) = \\\\mathcal{N}_N(f^{-1}(H)) $$$

Lean4

/-- The preimage of the normalizer is equal to the normalizer of the preimage of a surjective
  function. -/
@[to_additive /-- The preimage of the normalizer is equal to the normalizer of the preimage of
          a surjective function. -/
    ]
theorem comap_normalizer_eq_of_surjective (H : Subgroup G) {f : N →* G} (hf : Function.Surjective f) :
    H.normalizer.comap f = (H.comap f).normalizer :=
  comap_normalizer_eq_of_le_range fun x _ ↦ hf x

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