def Hex.Perm.Wreath.single {m n : Nat} (i : Fin m) (p : Perm n) : Fin m → Perm n

Equations

• Hex.Perm.Wreath.single i p j = if j = i then p else Hex.Perm.id n

def Hex.Perm.Wreath.copy {m n : Nat} (i : Fin m) (p : Perm n) : Perm (n * m)

Equations

• Hex.Perm.Wreath.copy i p = Hex.Perm.Wreath.perm (Hex.Perm.Wreath.single i p) (Hex.Perm.id m)

def Hex.Perm.Wreath.lift {m n : Nat} (h : Perm m) : Perm (n * m)

Equations

• Hex.Perm.Wreath.lift h = Hex.Perm.Wreath.perm (fun (x : Fin m) => Hex.Perm.id n) h

@[simp]

theorem Hex.Perm.Wreath.copy_id {m n : Nat} (i : Fin m) : copy i (Perm.id n) = Perm.id (n * m)

@[simp]

theorem Hex.Perm.Wreath.lift_id {m n : Nat} : lift (Perm.id m) = Perm.id (n * m)

theorem Hex.Perm.Wreath.copy_comp {m n : Nat} (i : Fin m) (p q : Perm n) : copy i (p.comp q) = (copy i p).comp (copy i q)

theorem Hex.Perm.Wreath.copy_inv {m n : Nat} (i : Fin m) (p : Perm n) : copy i p.inv = (copy i p).inv

theorem Hex.Perm.Wreath.lift_comp {m n : Nat} (h k : Perm m) : lift (h.comp k) = (lift h).comp (lift k)

theorem Hex.Perm.Wreath.lift_inv {m n : Nat} (h : Perm m) : lift h.inv = (lift h).inv

theorem Hex.Perm.Wreath.factor {m n : Nat} (f : Fin m → Perm n) (h : Perm m) : perm f h = (perm f (Perm.id m)).comp (lift h)

The base permutation followed by the top permutation gives the stated destination-indexed action.

def Hex.Perm.Wreath.initial {m n : Nat} (f : Fin m → Perm n) (k : Nat) : Fin m → Perm n

Multiply the base factors in increasing block order. This auxiliary function is used in the erased generation proof, not to enumerate elements.

Equations

• Hex.Perm.Wreath.initial f k j = if ↑j < k then f j else Hex.Perm.id n

@[simp]

theorem Hex.Perm.Wreath.initial_zero {m n : Nat} (f : Fin m → Perm n) : initial f 0 = fun (x : Fin m) => Perm.id n

@[simp]

theorem Hex.Perm.Wreath.initial_full {m n : Nat} (f : Fin m → Perm n) : initial f m = f

theorem Hex.Perm.Wreath.initial_succ {m n : Nat} (f : Fin m → Perm n) (k : Nat) (hk : k < m) : perm (initial f (k + 1)) (Perm.id m) = (perm (initial f k) (Perm.id m)).comp (copy ⟨k, hk⟩ (f ⟨k, hk⟩))