characteristic_iff_map_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, the image H.map φ ≤ H.

Русский

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

LaTeX

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

Lean4

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

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