English
The action of a group α on Sylow p-subgroups of G by conjugation (or pointwise action) corresponds to the acting of α on the Subgroup level: the underlying subgroup of g • P equals g acting on P.
Русский
Дествие группы α на подпогруппы Силова p G по конъюгации соответствует действию α на подгруппах: основанная подгруппа g • P равна g • (P).
LaTeX
$$$ \\uparrow (g \\cdot P) = g \\cdot (P : Subgroup G) $$$
Lean4
/-- `Subgroup.pointwiseMulAction` preserves Sylow subgroups. -/
instance pointwiseMulAction {α : Type*} [Group α] [MulDistribMulAction α G] : MulAction α (Sylow p G)
where
smul g
P :=
⟨g • P.toSubgroup, P.2.map _, fun {Q} hQ hS =>
inv_smul_eq_iff.mp
(P.3 (hQ.map _) fun s hs =>
(congr_arg (· ∈ g⁻¹ • Q) (inv_smul_smul g s)).mp
(smul_mem_pointwise_smul (g • s) g⁻¹ Q (hS (smul_mem_pointwise_smul s g P hs))))⟩
one_smul P := ext (one_smul α P.toSubgroup)
mul_smul g h P := ext (mul_smul g h P.toSubgroup)
