characteristic_iff_comap_le — 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, H.comap φ = H.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem characteristic_iff_comap_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.comap ϕ.toMonoidHom ≤ H :=
  characteristic_iff_comap_eq.trans
    ⟨fun h ϕ => le_of_eq (h ϕ), fun h ϕ =>
      le_antisymm (h ϕ) fun g hg => h ϕ.symm ((congr_arg (· ∈ H) (ϕ.symm_apply_apply g)).mpr hg)⟩

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