English
Let G be a finite group, P a Sylow p-subgroup and suppose N_G(P) ≤ C_G(P). Then for every g ∈ P, the transferSylow map evaluated at g has the form a pair whose first coordinate is g raised to the index [G : P], and whose second coordinate is given by a canonical auxiliary power-map. In particular, the transfer restricted to P coincides with the power map g ↦ g^{[G:P]} on P.
Русский
Пусть G — конечная группа, P — Sylow-подгруппа при p и предположим, что нормализатор N_G(P) содержится в центральизаторе C_G(P). Тогда для каждого элемента g ∈ P перенос Sylow имеет вид пары, первая координата которой равна g^{[G:P]}, а вторая координата задаётся соответствующей вспомогательной отображением степени. В частности, ограничение переноса к P совпадает с отображением g ↦ g^{[G:P]}.
LaTeX
$$$\forall g\in P,\quad \operatorname{transferSylow}(P,h_P)(g) = \langle g^{\,[G:P]},\operatorname{transferSylowEqPowAux}\bigl(g,\operatorname{transferSylowEqPowAux_P}(P,h_P,g,g\in P)\bigr)\rangle,$$$
Lean4
theorem transferSylow_eq_pow (g : G) (hg : g ∈ P) :
transferSylow P hP g = ⟨g ^ (P : Subgroup G).index, transfer_eq_pow_aux g (transferSylow_eq_pow_aux P hP g hg)⟩ :=
haveI : IsMulCommutative P := ⟨⟨fun a b => Subtype.ext (hP (le_normalizer b.2) a a.2)⟩⟩
transfer_eq_pow _ _ <| transferSylow_eq_pow_aux P hP g hg
