Homomorphisms from wreath products to abelian groups

#(D ≀ᵣ Q →* A) = #(D →* A) · #(Q →* A) for A abelian, and consequently the maximal elementary abelian 2-quotient of the n-fold iterated wreath power of C₂ has order 2 ^ n.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem elem_ab_card_hom (H : Type u_1) [Group H] [Finite H] (hcomm : ∀ (a b : H), a * b = b * a) (hexp : ∀ (h : H), h ^ 2 = 1) : Nat.card H = Nat.card (H →* Multiplicative (ZMod 2))

For a finite commutative group H of exponent 2, #H = #(H →* C₂) where C₂ = Multiplicative (ZMod 2).

theorem RegularWreathProduct.card_hom (D Q A : Type) [Group D] [Group Q] [CommGroup A] [Finite Q] : Nat.card (D ≀ᵣ Q →* A) = Nat.card (D →* A) * Nat.card (Q →* A)

#((D ≀ᵣ Q) →* A) = #(D →* A) · #(Q →* A) for finite groups D, Q and finite abelian A.

theorem wreath_max_elem_ab (n : ℕ) : Nat.card (IteratedWreathProduct (Multiplicative (ZMod 2)) n →* Multiplicative (ZMod 2)) = 2 ^ n

#([C_2]^n →* C_2) = 2^n: the maximal elementary-abelian 2-quotient of WreathPower n has 𝔽₂-dimension n.