def Hex.PermGroup.WreathProduct.pair {n m : Nat} {G : Group n} {H : Group m} (f : Fin m → Element G) (h : Element H) : Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.pair f h = ⟨Hex.Perm.Wreath.perm (fun (j : Fin m) => (f j).val) h.val, ⋯⟩

theorem Hex.PermGroup.WreathProduct.factors {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r.val = Perm.Wreath.perm f h

def Hex.PermGroup.WreathProduct.top {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) : Element H

Equations

• Hex.PermGroup.WreathProduct.top r = ⟨Hex.Perm.Wreath.top r.val ⋯, ⋯⟩

def Hex.PermGroup.WreathProduct.base {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) (j : Fin m) : Element G

Equations

• Hex.PermGroup.WreathProduct.base r j = ⟨Hex.Perm.Wreath.base r.val ⋯ j, ⋯⟩

theorem Hex.PermGroup.WreathProduct.top_of_not_pos {n m : Nat} {G : Group n} {H : Group m} (hn : ¬0 < n) (r : Element (G.wreathProduct H)) : top r = Element.id H

Empty blocks have no points, so the top projection is trivial.

@[simp]

theorem Hex.PermGroup.WreathProduct.top_pair {n m : Nat} {G : Group n} {H : Group m} (hn : 0 < n) (f : Fin m → Element G) (h : Element H) : top (pair f h) = h

@[simp]

theorem Hex.PermGroup.WreathProduct.base_pair {n m : Nat} {G : Group n} {H : Group m} (f : Fin m → Element G) (h : Element H) (j : Fin m) : base (pair f h) j = f j

@[simp]

theorem Hex.PermGroup.WreathProduct.pair_factors {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) : pair (base r) (top r) = r

theorem Hex.PermGroup.WreathProduct.pair_injective {n m : Nat} {G : Group n} {H : Group m} (hn : 0 < n) {f g : Fin m → Element G} {h k : Element H} (he : pair f h = pair g k) : f = g ∧ h = k

@[simp]

theorem Hex.PermGroup.WreathProduct.pair_id {n m : Nat} {G : Group n} {H : Group m} : pair (fun (x : Fin m) => Element.id G) (Element.id H) = Element.id (G.wreathProduct H)

theorem Hex.PermGroup.WreathProduct.pair_comp {n m : Nat} {G : Group n} {H : Group m} (f g : Fin m → Element G) (h k : Element H) : (pair f h).comp (pair g k) = pair (fun (j : Fin m) => (f j).comp (g (h.val.inv.get j))) (h.comp k)

theorem Hex.PermGroup.WreathProduct.top_comp {n m : Nat} {G : Group n} {H : Group m} (r s : Element (G.wreathProduct H)) : top (r.comp s) = (top r).comp (top s)

theorem Hex.PermGroup.WreathProduct.base_comp {n m : Nat} {G : Group n} {H : Group m} (r s : Element (G.wreathProduct H)) (j : Fin m) : base (r.comp s) j = (base r j).comp (base s ((top r).val.inv.get j))

def Hex.PermGroup.WreathProduct.inl {n m : Nat} {G : Group n} (H : Group m) (f : Fin m → Element G) : Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.inl H f = Hex.PermGroup.WreathProduct.pair f (Hex.PermGroup.Element.id H)

def Hex.PermGroup.WreathProduct.inr {n m : Nat} {H : Group m} (G : Group n) (h : Element H) : Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.inr G h = Hex.PermGroup.WreathProduct.pair (fun (x : Fin m) => Hex.PermGroup.Element.id G) h

def Hex.PermGroup.WreathProduct.copy {n m : Nat} {G : Group n} (H : Group m) (i : Fin m) (p : Element G) : Element (G.wreathProduct H)

Equations

• Hex.PermGroup.WreathProduct.copy H i p = Hex.PermGroup.WreathProduct.inl H fun (j : Fin m) => if j = i then p else Hex.PermGroup.Element.id G

theorem Hex.PermGroup.WreathProduct.inl_injective {n m : Nat} {G : Group n} {H : Group m} {f g : Fin m → Element G} (he : inl H f = inl H g) : f = g

theorem Hex.PermGroup.WreathProduct.inr_injective {n m : Nat} {G : Group n} {H : Group m} (hn : 0 < n) {h k : Element H} (he : inr G h = inr G k) : h = k

theorem Hex.PermGroup.WreathProduct.copy_injective {n m : Nat} {G : Group n} {H : Group m} (i : Fin m) {p q : Element G} (he : copy H i p = copy H i q) : p = q

@[simp]

theorem Hex.PermGroup.WreathProduct.top_inl {n m : Nat} {G : Group n} {H : Group m} (f : Fin m → Element G) : top (inl H f) = Element.id H

@[simp]

theorem Hex.PermGroup.WreathProduct.top_inr {n m : Nat} {G : Group n} {H : Group m} (hn : 0 < n) (h : Element H) : top (inr G h) = h

theorem Hex.PermGroup.WreathProduct.top_eq_id {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) : top r = Element.id H ↔ ∃ (f : Fin m → Element G), inl H f = r

The kernel of the top projection is exactly the embedded base group.

theorem Hex.PermGroup.WreathProduct.inl_comp {n m : Nat} {G : Group n} {H : Group m} (f g : Fin m → Element G) : (inl H f).comp (inl H g) = inl H fun (j : Fin m) => (f j).comp (g j)

theorem Hex.PermGroup.WreathProduct.inr_comp {n m : Nat} {G : Group n} {H : Group m} (h k : Element H) : (inr G h).comp (inr G k) = inr G (h.comp k)

theorem Hex.PermGroup.WreathProduct.inr_inv {n m : Nat} {G : Group n} {H : Group m} (h : Element H) : (inr G h).inv = inr G h.inv

theorem Hex.PermGroup.WreathProduct.copy_comp {n m : Nat} {G : Group n} {H : Group m} (i : Fin m) (p q : Element G) : (copy H i p).comp (copy H i q) = copy H i (p.comp q)

theorem Hex.PermGroup.WreathProduct.conjugate_base {n m : Nat} {G : Group n} {H : Group m} (h : Element H) (f : Fin m → Element G) : (inr G h).comp ((inl H f).comp (inr G h).inv) = inl H fun (j : Fin m) => f (h.val.inv.get j)

Conjugation by a top element permutes the base factors by its action on blocks. This is the semidirect-product action.

theorem Hex.PermGroup.WreathProduct.conjugate_copy {n m : Nat} {G : Group n} {H : Group m} (h : Element H) (i : Fin m) (p : Element G) : (inr G h).comp ((copy H i p).comp (inr G h).inv) = copy H (h.val.get i) p

theorem Hex.PermGroup.WreathProduct.decomposition {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.wreathProduct H)) : (inl H (base r)).comp (inr G (top r)) = r