characteristic_iff_comap_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 comap of H along φ equals H.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem characteristic_iff_comap_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom = H :=
  ⟨Characteristic.fixed, Characteristic.mk⟩

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