def Hex.Perm.Wreath.topPoint {n m : Nat} (r : Perm (n * m)) (j : Fin m) : Fin m

Read the destination of each block using its first point. Empty blocks carry no points, so the top permutation is then the identity.

Equations

• Hex.Perm.Wreath.topPoint r j = if hn : 0 < n then Hex.Perm.Wreath.block (r.get (Hex.Perm.Wreath.index ⟨0, hn⟩ j)) else j

@[simp]

theorem Hex.Perm.Wreath.topPoint_perm {n m : Nat} (hn : 0 < n) (f : Fin m → Perm n) (h : Perm m) (j : Fin m) : topPoint (perm f h) j = h.get j

theorem Hex.Perm.Wreath.topPoint_of_not_pos {n m : Nat} (r : Perm (n * m)) (hn : ¬0 < n) (j : Fin m) : topPoint r j = j

def Hex.Perm.Wreath.top {n m : Nat} (r : Perm (n * m)) (hr : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r = perm f h) : Perm m

Equations

• Hex.Perm.Wreath.top r hr = Hex.Perm.ofFn (Hex.Perm.Wreath.topPoint r) ⋯ ⋯

@[simp]

theorem Hex.Perm.Wreath.top_perm {n m : Nat} (hn : 0 < n) (f : Fin m → Perm n) (h : Perm m) (hr : ∃ (f_1 : Fin m → Perm n), ∃ (h_1 : Perm m), perm f h = perm f_1 h_1) : top (perm f h) hr = h

theorem Hex.Perm.Wreath.top_of_not_pos {n m : Nat} (r : Perm (n * m)) (hr : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r = perm f h) (hn : ¬0 < n) : top r hr = Perm.id m

def Hex.Perm.Wreath.basePoint {n m : Nat} (r : Perm (n * m)) (hr : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r = perm f h) (j : Fin m) (i : Fin n) : Fin n

A base factor is read from the block sent to its destination by the top permutation. This follows the destination-indexed multiplication convention.

Equations

• Hex.Perm.Wreath.basePoint r hr j i = Hex.Perm.Wreath.point (r.get (Hex.Perm.Wreath.index i ((Hex.Perm.Wreath.top r hr).inv.get j)))

@[simp]

theorem Hex.Perm.Wreath.basePoint_perm {n m : Nat} (f : Fin m → Perm n) (h : Perm m) (hr : ∃ (f_1 : Fin m → Perm n), ∃ (h_1 : Perm m), perm f h = perm f_1 h_1) (j : Fin m) (i : Fin n) : basePoint (perm f h) hr j i = (f j).get i

def Hex.Perm.Wreath.base {n m : Nat} (r : Perm (n * m)) (hr : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r = perm f h) (j : Fin m) : Perm n

Equations

• Hex.Perm.Wreath.base r hr j = Hex.Perm.ofFn (Hex.Perm.Wreath.basePoint r hr j) ⋯ ⋯

@[simp]

theorem Hex.Perm.Wreath.base_perm {n m : Nat} (f : Fin m → Perm n) (h : Perm m) (hr : ∃ (f_1 : Fin m → Perm n), ∃ (h_1 : Perm m), perm f h = perm f_1 h_1) (j : Fin m) : base (perm f h) hr j = f j

theorem Hex.Perm.Wreath.reconstruct {n m : Nat} (r : Perm (n * m)) (hr : ∃ (f : Fin m → Perm n), ∃ (h : Perm m), r = perm f h) : perm (base r hr) (top r hr) = r