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₂⟩.

Equations

• «term_≀ᵣ_» = Lean.ParserDescr.trailingNode `«term_≀ᵣ_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≀ᵣ ") (Lean.ParserDescr.cat `term 66))

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

Equations

• RegularWreathProduct.instMul = { mul := fun (a b : D ≀ᵣ Q) => { left := a.left * fun (x : Q) => b.left (a.right⁻¹ * x), right := a.right * b.right } }

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)

Equations

• RegularWreathProduct.instOne = { one := { left := 1, right := 1 } }

@[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)

Equations

• RegularWreathProduct.instInv = { inv := fun (x : D ≀ᵣ Q) => { left := fun (k : Q) => x.left⁻¹ (x.right * k), right := x.right⁻¹ } }

@[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)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• RegularWreathProduct.instInhabited = { default := 1 }

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.

Equations

• RegularWreathProduct.rightHom = { toFun := RegularWreathProduct.right, map_one' := ⋯, map_mul' := ⋯ }

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⟩

Equations

• RegularWreathProduct.inl = { toFun := fun (q : Q) => { left := 1, right := q }, map_one' := ⋯, map_mul' := ⋯ }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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₂.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• RegularWreathProduct.instSMulProd D Q Λ = { smul := fun (w : D ≀ᵣ Q) (p : Λ × Q) => (w.left (w.right * p.2) • p.1, w.right * p.2) }

@[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)

Equations

• RegularWreathProduct.instMulActionProd D Q Λ = { toSMul := RegularWreathProduct.instSMulProd D Q Λ, one_smul := ⋯, mul_smul := ⋯ }

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 Λ.

Equations

• RegularWreathProduct.toPerm D Q Λ = MulAction.toPermHom (D ≀ᵣ Q) (Λ × Q)

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.

Equations

• IteratedWreathProduct G 0 = PUnit.{?u.76 + 1}
• IteratedWreathProduct G n.succ = IteratedWreathProduct G n ≀ᵣ G

@[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)

Equations

• instGroupIteratedWreathProduct G n = Nat.recAux (⋯.mpr inferInstance) (fun (n : ℕ) (ih : Group (IteratedWreathProduct G n)) => ⋯.mpr inferInstance) 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).

Equations

• iteratedWreathToPermHom G 0 = 1
• iteratedWreathToPermHom G n.succ = (Equiv.Perm.permCongrHom (Fin.succFunEquiv G n).symm).toMonoidHom.comp (RegularWreathProduct.toPerm (IteratedWreathProduct G n) G (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.

Equations

• One or more equations did not get rendered due to their size.