def Hex.Perm.Sum.act {n m : Nat} (p : Perm n) (q : Perm m) : Fin (n + m) → Fin (n + m)

Consecutive disjoint supports retain the full declared factor degrees.

Equations

• Hex.Perm.Sum.act p q i = Fin.addCases (fun (i : Fin n) => Fin.castAdd m (p.get i)) (fun (j : Fin m) => Fin.natAdd n (q.get j)) i

@[simp]

theorem Hex.Perm.Sum.act_left {n m : Nat} (p : Perm n) (q : Perm m) (i : Fin n) : act p q (Fin.castAdd m i) = Fin.castAdd m (p.get i)

@[simp]

theorem Hex.Perm.Sum.act_right {n m : Nat} (p : Perm n) (q : Perm m) (i : Fin m) : act p q (Fin.natAdd n i) = Fin.natAdd n (q.get i)

@[simp]

theorem Hex.Perm.Sum.inv_act {n m : Nat} (p : Perm n) (q : Perm m) (i : Fin (n + m)) : act p.inv q.inv (act p q i) = i

def Hex.Perm.sum {n m : Nat} (p : Perm n) (q : Perm m) : Perm (n + m)

The direct sum action of permutations on consecutive disjoint domains.

Equations

• p.sum q = Hex.Perm.ofFn (Hex.Perm.Sum.act p q) ⋯ ⋯

@[simp]

theorem Hex.Perm.sum_left {n m : Nat} (p : Perm n) (q : Perm m) (i : Fin n) : (p.sum q).get (Fin.castAdd m i) = Fin.castAdd m (p.get i)

@[simp]

theorem Hex.Perm.sum_right {n m : Nat} (p : Perm n) (q : Perm m) (i : Fin m) : (p.sum q).get (Fin.natAdd n i) = Fin.natAdd n (q.get i)

@[simp]

theorem Hex.Perm.sum_id {n m : Nat} : (Perm.id n).sum (Perm.id m) = Perm.id (n + m)

theorem Hex.Perm.sum_comp {n m : Nat} (p r : Perm n) (q s : Perm m) : (p.comp r).sum (q.comp s) = (p.sum q).comp (r.sum s)

theorem Hex.Perm.sum_inv {n m : Nat} (p : Perm n) (q : Perm m) : p.inv.sum q.inv = (p.sum q).inv

theorem Hex.Perm.sum_injective {n m : Nat} {p r : Perm n} {q s : Perm m} (h : p.sum q = r.sum s) : p = r ∧ q = s