Ordered column-tuple expansion underlying Cauchy-Binet for hex-matrix.

This module expands the determinant of a column-sum matrix as a finite sum over all ordered column tuples drawn from Fin m. It defines the column-selected minor columnTupleMatrix, its product coefficient columnTupleCoeff, the tuple enumerator columnTupleVectors, and proves the summands of repeated columns vanish. The headline results are det_columnSumMatrix_eq_sum_columnTuples (the Mathlib-free multilinearity form) and det_gramMatrix_eq_sum_columnTuples, which specializes it to a row Gram matrix. The bulk of the file is a suffix-based partial-assignment recursion (columnSumMatrixWithSuffix) aligning the iteration with columnTupleVectors.

def Hex.Matrix.columnTupleMatrix {R : Type u} {n m : Nat} (A : Matrix R n m) (cols : Fin n → Fin m) : Matrix R n n

Square submatrix obtained by selecting an ordered tuple of columns.

Equations

• A.columnTupleMatrix cols = Hex.Matrix.ofFn fun (r c : Fin n) => A[(r, cols c)]

theorem Hex.Matrix.getElem_columnTupleMatrix {R : Type u} {n m : Nat} (A : Matrix R n m) (cols : Fin n → Fin m) (r c : Fin n) : (A.columnTupleMatrix cols)[r][c] = A[r][cols c]

Entry (r, c) of the column-selected minor is the source entry A[r][cols c].

def Hex.Matrix.columnTupleVectorFn {n m : Nat} (cols : Vector (Fin m) n) : Fin n → Fin m

Interpret an ordered column tuple vector as its column-selection function.

Equations

• Hex.Matrix.columnTupleVectorFn cols i = cols[i]

@[simp]

theorem Hex.Matrix.columnTupleVectorFn_apply {n m : Nat} (cols : Vector (Fin m) n) (i : Fin n) : columnTupleVectorFn cols i = cols[i]

Applying the column-selection function at i reads the i-th entry cols[i] of the tuple vector.

theorem Hex.Matrix.getElem_columnTupleMatrix_compose_perm {R : Type u} {n m : Nat} (A : Matrix R n m) (s : Vector (Fin m) n) (sigma : Vector (Fin n) n) (r c : Fin n) : (A.columnTupleMatrix fun (i : Fin n) => s[sigma[i]])[r][c] = (A.columnTupleMatrix (columnTupleVectorFn s))[r][sigma[c]]

Reindexing the selected columns by a permutation is entrywise the generic column permutation of the selected minor.

Unattributed: the LHS [r][c] is not in simp-normal form (Fin.getElem_fin rewrites the Fin indices to ↑r/↑c), and grind = rejects the pattern because the columns s sigma appear only under the fun i => s[sigma[i]] binder, so the LHS cannot instantiate them. Invoked explicitly via rw.

theorem Hex.Matrix.columnTupleMatrix_compose_perm_eq_colPermute {R : Type u} {n m : Nat} (A : Matrix R n m) (s : Vector (Fin m) n) (sigma : Vector (Fin n) n) : (A.columnTupleMatrix fun (i : Fin n) => s[sigma[i]]) = ofFn fun (r c : Fin n) => (A.columnTupleMatrix (columnTupleVectorFn s))[r][sigma[c]]

Reindexing the selected columns by a permutation is the generic column permutation of the selected minor.

theorem Hex.Matrix.det_columnTupleMatrix_compose_perm {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) (s : Vector (Fin m) n) (sigma : Vector (Fin n) n) (hsigma : sigma ∈ permutationVectors n) : (A.columnTupleMatrix fun (i : Fin n) => s[sigma[i]]).det = detSign sigma * (A.columnTupleMatrix (columnTupleVectorFn s)).det

Specialization of the generic column-permutation determinant sign theorem to selected-minor matrices.

def Hex.Matrix.columnTupleVectors (n m : Nat) : List (Vector (Fin m) n)

Enumerate all ordered n-tuples of columns from Fin m.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.columnTupleVectors 0 x✝ = [#v[]]

theorem Hex.Matrix.columnTupleVectors_mem_ofFn {n m : Nat} (cols : Fin n → Fin m) : Vector.ofFn cols ∈ columnTupleVectors n m

Every ordered column-selection function occurs in columnTupleVectors.

def Hex.Matrix.columnTupleCoeff {R : Type u} [Mul R] [OfNat R 1] {n m : Nat} (A : Matrix R n m) (cols : Vector (Fin m) n) : R

Product coefficient attached to an ordered column tuple in the Gram expansion.

Equations

• A.columnTupleCoeff cols = Fin.foldl n (fun (acc : R) (i : Fin n) => acc * A[(i, cols[i])]) 1

def Hex.Matrix.columnTupleExpansionTerm {R : Type u} [Lean.Grind.Ring R] {n m : Nat} (A : Matrix R n m) (cols : Vector (Fin m) n) : R

The determinant summand associated to an ordered column tuple.

Equations

• A.columnTupleExpansionTerm cols = A.columnTupleCoeff cols * (A.columnTupleMatrix (Hex.Matrix.columnTupleVectorFn cols)).det

theorem Hex.Matrix.det_columnTupleMatrix_eq_zero_of_col_eq {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) (cols : Fin n → Fin m) {src dst : Fin n} (h : src ≠ dst) (hcols : cols src = cols dst) : (A.columnTupleMatrix cols).det = 0

An ordered column-tuple minor with a repeated selected column has determinant zero.

theorem Hex.Matrix.det_columnTupleMatrix_eq_zero_of_not_injective {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) (cols : Fin n → Fin m) (hcols : ¬Function.Injective cols) : (A.columnTupleMatrix cols).det = 0

An ordered column-tuple minor with a non-injective selected-column map has determinant zero.

Suffix-based partial assignment

We use a SUFFIX-based parametrization (chosen represents right-fixed columns) to align with the natural recursion of columnTupleVectors, which factors out the LAST element of the suffix. After Fubini sum-swap, the inductive step reduces to identity matching of the per-term values.

theorem Hex.Matrix.det_columnSumMatrix_eq_sum_columnTuples {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (source coeff : Matrix R n m) : (source.columnSumMatrix coeff).det = List.foldl (fun (acc : R) (cols : Vector (Fin m) n) => acc + coeff.columnTupleCoeff cols * (source.columnTupleMatrix (columnTupleVectorFn cols)).det) 0 (columnTupleVectors n m)

Expand the determinant of a matrix whose columns are linear combinations of source columns as a finite sum over all ordered column tuples. This is the Mathlib-free multilinearity form behind Cauchy-Binet.

theorem Hex.Matrix.det_gramMatrix_eq_sum_columnTuples {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (A : Matrix R n m) : A.gramMatrix.det = List.foldl (fun (acc : R) (cols : Vector (Fin m) n) => acc + A.columnTupleCoeff cols * (A.columnTupleMatrix (columnTupleVectorFn cols)).det) 0 (columnTupleVectors n m)

The determinant of a row Gram matrix expands as the ordered-column tuple sum induced by the generic column-sum determinant expansion.