English
The Sylow p-subgroups of Perm α can be encoded as an iterated wreath product: under suitable cardinality assumptions card α = p^n and card G = p, there exists a MulEquiv between a Sylow p-subgroup of Perm α and IteratedWreathProduct G n.
Русский
Сиоловы подгруппы p-ой степени Perm α кодируются как итерированное вентовое произведение: при подходящих условиях |α| = p^n и |G| = p существует MulEquiv между Sylow_p (Perm α) и IteratedWreathProduct G n.
LaTeX
$$$ P \simeq^* IteratedWreathProduct(G,n) $ with card α = p^n and card G = p$$
Lean4
/-- The encoding of the Sylow `p`-subgroups of `Perm α` as an iterated wreath product. -/
noncomputable def mulEquivIteratedWreathProduct (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (α : Type*) [Finite α]
(hα : Nat.card α = p ^ n) (G : Type*) [Group G] [Finite G] (hG : Nat.card G = p) (P : Sylow p (Equiv.Perm α)) :
P ≃* IteratedWreathProduct G n :=
by
let e1 : α ≃ (Fin n → G) :=
(Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq (by rw [Nat.card_fun, Nat.card_fin, hG])).symm
let f := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
have hf : Function.Injective f := (e1.symm.permCongrHom.comp_injective _).mpr (iteratedWreathToPermHomInj G n)
let g := (MonoidHom.ofInjective hf).symm
let P' : Sylow p (Equiv.Perm α) :=
Sylow.ofCard (MonoidHom.range f)
(by
rw [Nat.card_congr g.toEquiv, IteratedWreathProduct.card, hG, Nat.card_perm, hα, ←
Nat.multiplicity_eq_factorization hp.out (p ^ n).factorial_ne_zero,
Nat.Prime.multiplicity_factorial_pow hp.out])
exact (P.equiv P').trans g
