def Hex.PermGroup.Group.wreathProduct {n m : Nat} (G : Group n) (H : Group m) : Group (n * m)

One copy of every original generator in every block, followed by the original top generators. All blocks are included even for intransitive H. With empty blocks (n = 0) there are no points and the result is trivial.

Equations

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

theorem Hex.PermGroup.Group.wreath_generators_size {n m : Nat} (G : Group n) (H : Group m) : (G.wreathProduct H).generators.size = m * G.generators.size + H.generators.size

theorem Hex.PermGroup.Group.wreath_copy_mem {n m : Nat} (G : Group n) (H : Group m) (i : Fin m) (p : Perm n) (hp : Generated G.generators p) : Generated (G.wreathProduct H).generators (Perm.Wreath.copy i p)

theorem Hex.PermGroup.Group.wreath_lift_mem {n m : Nat} (G : Group n) (H : Group m) (h : Perm m) (hh : Generated H.generators h) : Generated (G.wreathProduct H).generators (Perm.Wreath.lift h)

theorem Hex.PermGroup.Group.wreath_base_mem {n m : Nat} (G : Group n) (H : Group m) (f : Fin m → Perm n) (hf : ∀ (j : Fin m), Generated G.generators (f j)) : Generated (G.wreathProduct H).generators (Perm.Wreath.perm f (Perm.id m))

theorem Hex.PermGroup.Group.wreath_perm_mem {n m : Nat} (G : Group n) (H : Group m) (f : Fin m → Perm n) (h : Perm m) (hf : ∀ (j : Fin m), Generated G.generators (f j)) (hh : Generated H.generators h) : Generated (G.wreathProduct H).generators (Perm.Wreath.perm f h)

theorem Hex.PermGroup.Group.mem_wreathProduct {n m : Nat} (G : Group n) (H : Group m) (r : Perm (n * m)) : Generated (G.wreathProduct H).generators r ↔ ∃ (f : Fin m → Perm n), ∃ (h : Perm m), (∀ (j : Fin m), Generated G.generators (f j)) ∧ Generated H.generators h ∧ r = Perm.Wreath.perm f h

Generated elements are exactly the base functions together with a top element. This also proves that the listed copies and lifts generate the result.