def Hex.Perm.support {n : Nat} (p : Perm n) : Array (Fin n)

The sorted points moved by a permutation.

Equations

• p.support = (List.filter (fun (i : Fin n) => decide (p.get i ≠ i)) (List.finRange n)).toArray

@[simp]

theorem Hex.Perm.mem_support {n : Nat} (p : Perm n) (i : Fin n) : i ∈ p.support ↔ p.get i ≠ i

def Hex.Perm.visit {n : Nat} (p : Perm n) : Nat → Fin n → Vector Bool n → Array (Fin n) → Vector Bool n × Array (Fin n)

Follow one cycle, marking each point on its first visit. The degree bounds its length, including when the cycle contains every point.

Equations

• p.visit 0 x✝² x✝¹ x✝ = (x✝¹, x✝)
• p.visit fuel.succ x✝² x✝¹ x✝ = if x✝¹[↑x✝²] = true then (x✝¹, x✝) else p.visit fuel (p.get x✝²) (x✝¹.set (↑x✝²) true ⋯) (x✝.push x✝²)

def Hex.Perm.scanCycles {n : Nat} (p : Perm n) : List (Fin n) → Vector Bool n → Array (Array (Fin n)) → Vector Bool n × Array (Array (Fin n))

Scan the starting points, retaining the marks between visits.

Equations

• p.scanCycles [] x✝¹ x✝ = (x✝¹, x✝)
• p.scanCycles (x_3 :: xs) x✝¹ x✝ = if x✝¹[↑x_3] = true then p.scanCycles xs x✝¹ x✝ else match p.visit n x_3 x✝¹ #[] with | (next, cycle) => p.scanCycles xs next (x✝.push cycle)

def Hex.Perm.allCycles {n : Nat} (p : Perm n) : Array (Array (Fin n))

Disjoint cycles, including singleton fixed points. Scanning starting points in order makes each cycle begin at its least point and orders the cycles.

Equations

• p.allCycles = (p.scanCycles (List.finRange n) (Vector.replicate n false) #[]).snd

def Hex.Perm.cycles {n : Nat} (p : Perm n) : Array (Array (Fin n))

Canonical disjoint cycles, omitting fixed points.

Equations

• p.cycles = Array.filter (fun (cycle : Array (Fin n)) => decide (cycle.size > 1)) p.allCycles

def Hex.Perm.cycleType {n : Nat} (p : Perm n) : Array Nat

Sorted cycle lengths, with a one for every fixed point. Counting lengths in the range 1,...,n keeps the computation linear in the declared degree.

Equations

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

def Hex.Perm.sign {n : Nat} (p : Perm n) : Int

Permutation sign from the number of cycles, including fixed points.

Equations

• p.sign = if (n - p.allCycles.size) % 2 = 0 then 1 else -1

def Hex.Perm.order {n : Nat} (p : Perm n) : Nat

The least common multiple of the cycle lengths; the empty lcm is one.

Equations

• p.order = Array.foldl (fun (k : Nat) (cycle : Array (Fin n)) => k.lcm cycle.size) 1 p.cycles

def Hex.Perm.pow {n : Nat} (p : Perm n) : Nat → Perm n

Natural powers, with function-composition multiplication.

Equations

• p.pow 0 = Hex.Perm.id n
• p.pow k.succ = p.comp (p.pow k)

@[simp]

theorem Hex.Perm.pow_zero {n : Nat} (p : Perm n) : p.pow 0 = Perm.id n

@[simp]

theorem Hex.Perm.pow_succ {n : Nat} (p : Perm n) (k : Nat) : p.pow (k + 1) = p.comp (p.pow k)

theorem Hex.Perm.pow_add {n : Nat} (p : Perm n) (k l : Nat) : p.pow (k + l) = (p.pow k).comp (p.pow l)

@[instance_reducible]

instance Hex.Perm.instMul {n : Nat} : Mul (Perm n)

Equations

• Hex.Perm.instMul = { mul := Hex.Perm.comp }

@[instance_reducible]

instance Hex.Perm.instInv {n : Nat} : Inv (Perm n)

Equations

• Hex.Perm.instInv = { inv := Hex.Perm.inv }

@[instance_reducible]

instance Hex.Perm.instOfNatOfNatNat {n : Nat} : OfNat (Perm n) 1

Equations

• Hex.Perm.instOfNatOfNatNat = { ofNat := Hex.Perm.id n }

@[instance_reducible]

instance Hex.Perm.instPowNat {n : Nat} : Pow (Perm n) Nat

Equations

• Hex.Perm.instPowNat = { pow := Hex.Perm.pow }

@[simp]

theorem Hex.Perm.mul_def {n : Nat} (p q : Perm n) : p * q = p.comp q

@[simp]

theorem Hex.Perm.inv_def {n : Nat} (p : Perm n) : p⁻¹ = p.inv

@[simp]

theorem Hex.Perm.one_def {n : Nat} : 1 = Perm.id n

@[simp]

theorem Hex.Perm.pow_def {n : Nat} (p : Perm n) (k : Nat) : p ^ k = p.pow k

theorem Hex.Perm.sign_eq {n : Nat} (p : Perm n) : p.sign = 1 ∨ p.sign = -1