characteristic_iff_le_map — 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 map H ≤ H.map φ.toMonoidHom.

Русский

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

LaTeX

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

Lean4

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

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