characteristic_iff_map_eq — Mathlib

English

Let G be a group and H a subgroup of G. Then H is characteristic in G iff for every automorphism φ of G, the image of H under φ equals H.

Русский

Пусть G — группа и H — подгруппа G. Тогда H характеристическая в G тогда и только тогда, если образ H при любом автоморфизме φ равен H.

LaTeX

$$$H \text{ characteristic in } G \iff \forall \varphi \in \mathrm{Aut}(G),\; \varphi(H) = H.$$$

Lean4

@[to_additive]
theorem characteristic_iff_map_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom = H :=
  by
  simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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