def Hex.PermGroup.WreathProduct.shift {n m : ℕ} (G : Group n) (H : Group m) : Element H →* MulAut (Fin m → Element G)

The top group acts on the base functions by inverse reindexing.

Equations

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

def Hex.PermGroup.WreathProduct.equiv {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) : Element (G.wreathProduct H) ≃* (Fin m → Element G) ⋊[shift G H] Element H

The imprimitive permutation group is the semidirect product G^m ⋊ H, with the executable base and top projections as the equivalence.

Equations

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

@[simp]

theorem Hex.PermGroup.WreathProduct.equiv_pair {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) (f : Fin m → Element G) (h : Element H) : (equiv G H hn) (pair f h) = ⟨f, h⟩

def Hex.PermGroup.WreathProduct.inlHom {n m : ℕ} (G : Group n) (H : Group m) : (Fin m → Element G) →* Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.inlHom G H = { toFun := Hex.PermGroup.WreathProduct.inl H, map_one' := ⋯, map_mul' := ⋯ }

def Hex.PermGroup.WreathProduct.inrHom {n m : ℕ} (G : Group n) (H : Group m) : Element H →* Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.inrHom G H = { toFun := Hex.PermGroup.WreathProduct.inr G, map_one' := ⋯, map_mul' := ⋯ }

def Hex.PermGroup.WreathProduct.topHom {n m : ℕ} (G : Group n) (H : Group m) : Element (G.wreathProduct H) →* Element H

The executable top projection. With empty blocks it is the trivial map.

Equations

• Hex.PermGroup.WreathProduct.topHom G H = { toFun := Hex.PermGroup.WreathProduct.top, map_one' := ⋯, map_mul' := ⋯ }

theorem Hex.PermGroup.WreathProduct.range_inl {n m : ℕ} (G : Group n) (H : Group m) : (inlHom G H).range = (topHom G H).ker

theorem Hex.PermGroup.WreathProduct.equiv_inl {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) (f : Fin m → Element G) : (equiv G H hn) (inl H f) = SemidirectProduct.inl f

theorem Hex.PermGroup.WreathProduct.equiv_inr {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) (h : Element H) : (equiv G H hn) (inr G h) = SemidirectProduct.inr h

def Hex.PermGroup.WreathProduct.subgroupShift {n m : ℕ} (G : Group n) (H : Group m) : ↥(closure H.generators) →* MulAut (Fin m → ↥(closure G.generators))

Inverse reindexing stated entirely in the generated Mathlib subgroups.

Equations

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

def Hex.PermGroup.WreathProduct.groupEquiv {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) : ↥(closure (G.wreathProduct H).generators) ≃* (Fin m → ↥(closure G.generators)) ⋊[subgroupShift G H] ↥(closure H.generators)

The checked permutation subgroup is multiplicatively equivalent to the Mathlib semidirect product of its mathematical factors.

Equations

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

theorem Hex.PermGroup.WreathProduct.groupEquiv_pair {n m : ℕ} (G : Group n) (H : Group m) (hn : 0 < n) (f : Fin m → Element G) (h : Element H) : (groupEquiv G H hn) ((Element.equiv (G.wreathProduct H)) (pair f h)) = ⟨fun (j : Fin m) => (Element.equiv G) (f j), (Element.equiv H) h⟩