conjAction — Mathlib

English

If H is a normal subgroup of G, then G acts on H by conjugation via h ↦ g h g^{-1}, turning H into a G-set and giving a natural action.

Русский

Пусть H нормальная подгруппа G. Тогда G действует на H посредством сопряжения: g·h = g h g^{-1}; это образует действие группы на H.

LaTeX

$$$ (\forall g \in G)(h \in H) : g \cdot h = g h g^{-1}, \quad H \trianglelefteq G \Rightarrow H \text{ carries a } G\text{-action}. $$$

Lean4

/-- As normal subgroups are closed under conjugation, they inherit the conjugation action
  of the underlying group. -/
instance conjAction {H : Subgroup G} [hH : H.Normal] : SMul (ConjAct G) H :=
  ⟨fun g h => ⟨g • (h : G), hH.conj_mem h.1 h.2 (ofConjAct g)⟩⟩

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