Permutation-group structure on permutation vectors.

This module develops the operations on permutation vectors that the elementary row and column operation laws are built from: finTranspose and transposePermutationValues/swapPermutationValues (position and value swaps), inversePermutationVector, and composePermutationValues. It shows these preserve membership in permutationVectors and tracks their effect on inversion parity, culminating in detSign_swapPermutationValues and the multiplicativity law detSign_composePermutationValues. The elementary-operation determinant laws themselves live in HexDeterminant.RowOps.

def Hex.Matrix.finTranspose {n : Nat} (i j r : Fin n) : Fin n

The transposition of Fin n swapping i and j, sending r to j if r = i, to i if r = j, and to itself otherwise.

Equations

• Hex.Matrix.finTranspose i j r = if r = i then j else if r = j then i else r

def Hex.Matrix.swapPermutationValues {n : Nat} (perm : Vector (Fin n) n) (i j : Fin n) : Vector (Fin n) n

Swap the values i and j inside a permutation vector, leaving positions fixed. This models the column permutation induced by exchanging two columns.

Equations

• Hex.Matrix.swapPermutationValues perm i j = Vector.map (Hex.Matrix.finTranspose i j) perm

theorem Hex.Matrix.swapPermutationValues_get_if {n : Nat} (perm : Vector (Fin n) n) (i j r : Fin n) : (swapPermutationValues perm i j)[r] = if perm[r] = i then j else if perm[r] = j then i else perm[r]

Entrywise characterization of swapPermutationValues: occurrences of i become j, occurrences of j become i, and all other values stay put.

def Hex.Matrix.inversePermutationValues {n : Nat} (perm : Vector (Fin n) n) (hnodup : perm.toList.Nodup) : Vector (Fin n) n

The inverse permutation vector: at value c, return the position where c occurs in perm.

Equations

• Hex.Matrix.inversePermutationValues perm hnodup = Vector.ofFn fun (c : Fin n) => ⟨List.idxOf c perm.toList, ⋯⟩

def Hex.Matrix.inversePermutationVector {n : Nat} (perm : Vector (Fin n) n) : Vector (Fin n) n

Equations

• Hex.Matrix.inversePermutationVector perm = if hnodup : perm.toList.Nodup then Hex.Matrix.inversePermutationValues perm hnodup else perm

def Hex.Matrix.composePermutationValues {n : Nat} (sigma tau : Vector (Fin n) n) : Vector (Fin n) n

Equations

• Hex.Matrix.composePermutationValues sigma tau = Vector.ofFn fun (i : Fin n) => sigma[tau[i]]

theorem Hex.Matrix.detSign_swapPermutationValues {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (perm : Vector (Fin n) n) (i j : Fin n) (hnodup : perm.toList.Nodup) (h : i ≠ j) : detSign perm = -detSign (swapPermutationValues perm i j)

Swapping two distinct values in a duplicate-free permutation vector flips the determinant sign. This is the sign bookkeeping for column swaps.

theorem Hex.Matrix.detSign_composePermutationValues {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (sigma tau : Vector (Fin n) n) (hsigma : sigma ∈ permutationVectors n) (htau : tau ∈ permutationVectors n) : detSign (composePermutationValues sigma tau) = detSign sigma * detSign tau

Multiplicativity of detSign under composition of permutation vectors. The sign of a composed permutation equals the product of the component signs.

theorem Hex.Matrix.detSign_eq_mul_detSign_composePermutationValues {R : Type u} [Lean.Grind.CommRing R] {n : Nat} (sigma tau : Vector (Fin n) n) (hsigma : sigma ∈ permutationVectors n) (htau : tau ∈ permutationVectors n) : detSign tau = detSign sigma * detSign (composePermutationValues sigma tau)

Inverse-orientation form of detSign_composePermutationValues: the sign of tau is the sign of sigma times the sign of composePermutationValues sigma tau.