Regular wreath product

This file defines the regular wreath product of groups, and the canonical maps in and out of the product. The regular wreath product of D and Q is the product (Q → D) × Q with the group operation ⟨a₁, a₂⟩ * ⟨b₁, b₂⟩ = ⟨a₁ * (fun x ↦ b₁ (a₂⁻¹ * x)), a₂ * b₂⟩.

Main definitions

• RegularWreathProduct D Q : The regular wreath product of groups D and Q.
• rightHom : The canonical projection D ≀ᵣ Q →* Q.
• inl : The canonical map Q →* D ≀ᵣ Q.
• toPerm : The homomorphism from D ≀ᵣ Q to Equiv.Perm (Λ × Q), where Λ is a D-set.
• IteratedWreathProduct G n : The iterated wreath product of a group G n times.
• Sylow.mulEquivIteratedWreathProduct : The isomorphism between the Sylow p-subgroup of Perm p^n and the iterated wreath product of the cyclic group of order p n times.

Notation

This file introduces the global notation D ≀ᵣ Q for RegularWreathProduct D Q.

Tags

group, regular wreath product, sylow p-subgroup

structure RegularWreathProduct (D : Type u_1) (Q : Type u_2) : Type (max u_1 u_2)

The regular wreath product of groups Q and D. It is the product (Q → D) × Q with the group operation ⟨a₁, a₂⟩ * ⟨b₁, b₂⟩ = ⟨a₁ * (fun x ↦ b₁ (a₂⁻¹ * x)), a₂ * b₂⟩.

• left : Q → D

  The function of Q → D

• right : Q

  The element of Q

theorem RegularWreathProduct.ext_iff {D : Type u_1} {Q : Type u_2} {x y : D ≀ᵣ Q} : x = y ↔ x.left = y.left ∧ x.right = y.right

theorem RegularWreathProduct.ext {D : Type u_1} {Q : Type u_2} {x y : D ≀ᵣ Q} (left : x.left = y.left) (right : x.right = y.right) : x = y

def «term_≀ᵣ_» : Lean.TrailingParserDescr

The regular wreath product of groups Q and D. It is the product (Q → D) × Q with the group operation ⟨a₁, a₂⟩ * ⟨b₁, b₂⟩ = ⟨a₁ * (fun x ↦ b₁ (a₂⁻¹ * x)), a₂ * b₂⟩.

instance RegularWreathProduct.instMul {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : Mul (D ≀ᵣ Q)

theorem RegularWreathProduct.mul_def {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (a b : D ≀ᵣ Q) : a * b = { left := a.left * fun (x : Q) => b.left (a.right⁻¹ * x), right := a.right * b.right }

@[simp]

theorem RegularWreathProduct.mul_left {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (a b : D ≀ᵣ Q) : (a * b).left = a.left * fun (x : Q) => b.left (a.right⁻¹ * x)

@[simp]

theorem RegularWreathProduct.mul_right {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (a b : D ≀ᵣ Q) : (a * b).right = a.right * b.right

instance RegularWreathProduct.instOne {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : One (D ≀ᵣ Q)

@[simp]

theorem RegularWreathProduct.one_left {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : left 1 = 1

@[simp]

theorem RegularWreathProduct.one_right {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : right 1 = 1

instance RegularWreathProduct.instInv {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : Inv (D ≀ᵣ Q)

@[simp]

theorem RegularWreathProduct.inv_left {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (a : D ≀ᵣ Q) : a⁻¹.left = fun (x : Q) => a.left⁻¹ (a.right * x)

@[simp]

theorem RegularWreathProduct.inv_right {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (a : D ≀ᵣ Q) : a⁻¹.right = a.right⁻¹

instance RegularWreathProduct.instGroup {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : Group (D ≀ᵣ Q)

instance RegularWreathProduct.instInhabited {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : Inhabited (D ≀ᵣ Q)

def RegularWreathProduct.rightHom {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : D ≀ᵣ Q →* Q

The canonical projection map D ≀ᵣ Q →* Q, as a group hom.

def RegularWreathProduct.inl {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : Q →* D ≀ᵣ Q

The canonical map Q →* D ≀ᵣ Q sending q to ⟨1, q⟩

@[simp]

theorem RegularWreathProduct.left_inl {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (q : Q) : (inl q).left = 1

@[simp]

theorem RegularWreathProduct.right_inl {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (q : Q) : (inl q).right = q

@[simp]

theorem RegularWreathProduct.rightHom_eq_right {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : ⇑rightHom = right

@[simp]

theorem RegularWreathProduct.rightHom_comp_inl_eq_id {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] : rightHom.comp inl = MonoidHom.id Q

@[simp]

theorem RegularWreathProduct.fun_id {D : Type u_1} {Q : Type u_2} [Group D] [Group Q] (q : Q) : rightHom (inl q) = q

def RegularWreathProduct.equivProd (D : Type u_3) (Q : Type u_4) : D ≀ᵣ Q ≃ (Q → D) × Q

The equivalence map for the representation as a product.

instance RegularWreathProduct.instFinite {D : Type u_1} {Q : Type u_2} [Finite D] [Finite Q] : Finite (D ≀ᵣ Q)

theorem RegularWreathProduct.card {D : Type u_1} {Q : Type u_2} [Finite Q] : Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q

def RegularWreathProduct.congr {D₁ : Type u_3} {Q₁ : Type u_4} {D₂ : Type u_5} {Q₂ : Type u_6} [Group D₁] [Group Q₁] [Group D₂] [Group Q₂] (f : D₁ ≃* D₂) (g : Q₁ ≃* Q₂) : D₁ ≀ᵣ Q₁ ≃* D₂ ≀ᵣ Q₂

Define an isomorphism from D₁ ≀ᵣ Q₁ to D₂ ≀ᵣ Q₂ given isomorphisms D₁ ≀ᵣ Q₁ and Q₁ ≃* Q₂.

instance RegularWreathProduct.instSMulProd (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] : SMul (D ≀ᵣ Q) (Λ × Q)

@[simp]

theorem RegularWreathProduct.smul_def (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] {w : D ≀ᵣ Q} {p : Λ × Q} : w • p = (w.left (w.right * p.2) • p.1, w.right * p.2)

instance RegularWreathProduct.instMulActionProd (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] : MulAction (D ≀ᵣ Q) (Λ × Q)

instance RegularWreathProduct.instFaithfulSMulProdOfNonempty (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] [FaithfulSMul D Λ] [Nonempty Q] [Nonempty Λ] : FaithfulSMul (D ≀ᵣ Q) (Λ × Q)

def RegularWreathProduct.toPerm (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] : D ≀ᵣ Q →* Equiv.Perm (Λ × Q)

The map sending the wreath product D ≀ᵣ Q to its representation as a permutation of Λ × Q given D-set Λ.

theorem RegularWreathProduct.toPermInj (D : Type u_1) (Q : Type u_2) [Group D] [Group Q] (Λ : Type u_3) [MulAction D Λ] [FaithfulSMul D Λ] [Nonempty Λ] : Function.Injective ⇑(toPerm D Q Λ)

def IteratedWreathProduct (G : Type u) (n : ℕ) : Type u

The wreath product of group G iterated n times.

@[simp]

theorem IteratedWreathProduct_zero (G : Type u) : IteratedWreathProduct G 0 = PUnit.{u + 1}

@[simp]

theorem IteratedWreathProduct_succ (G : Type u) (n : ℕ) : IteratedWreathProduct G (n + 1) = IteratedWreathProduct G n ≀ᵣ G

instance instFiniteIteratedWreathProduct (G : Type u) (n : ℕ) [Finite G] : Finite (IteratedWreathProduct G n)

theorem IteratedWreathProduct.card (G : Type u) (n : ℕ) [Finite G] : Nat.card (IteratedWreathProduct G n) = Nat.card G ^ ∑ i ∈ Finset.range n, Nat.card G ^ i

instance instGroupIteratedWreathProduct (G : Type u) (n : ℕ) [Group G] : Group (IteratedWreathProduct G n)

def iteratedWreathToPermHom (G : Type u_3) [Group G] (n : ℕ) : IteratedWreathProduct G n →* Equiv.Perm (Fin n → G)

The homomorphism from IteratedWreathProduct G n to Perm (Fin n → G).

theorem iteratedWreathToPermHomInj (G : Type u_3) [Group G] (n : ℕ) : Function.Injective ⇑(iteratedWreathToPermHom G n)

noncomputable def Sylow.mulEquivIteratedWreathProduct (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (α : Type u_3) [Finite α] (hα : Nat.card α = p ^ n) (G : Type u_4) [Group G] [Finite G] (hG : Nat.card G = p) (P : Sylow p (Equiv.Perm α)) : ↥↑P ≃* IteratedWreathProduct G n

The encoding of the Sylow p-subgroups of Perm α as an iterated wreath product.