Lean formalization: over $\mathbb{Q}$, the matrix $J-P_\sigma$ has rank $n$ for $n\neq 1$

This short note extends the Lean formalization in [ixekny] from the diagonal matching $J-I$ to a general permutation matrix $P_\sigma$.

Statement

Let $n\in\mathbb{N}$, $n\neq 1$, and let $\sigma\in S_n$ be a permutation. Let $J$ be the $n\times n$ all-ones matrix and $P_\sigma$ the permutation matrix of $\sigma$.

Then over $\mathbb{Q}$, $$\operatorname{rank}(J-P_\sigma)=n.$$

Equivalently, the linear map $(J-P_\sigma)\colon \mathbb{Q}^n\to\mathbb{Q}^n$ is injective.

This matches the kernel argument used informally in [ixekny] to prove the general lower bound $T(n)\ge n$.

Lean file

Attachment: TilesRankPerm.lean.

import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.LinearAlgebra.Matrix.Permutation

open scoped BigOperators

namespace TilesRankPerm

open Matrix Module Equiv

/-- The all-ones matrix. -/
noncomputable def allOnes (n : ℕ) : Matrix (Fin n) (Fin n) ℚ := fun _ _ => 1

lemma allOnes_mulVec {n : ℕ} (v : Fin n → ℚ) :
    allOnes n *ᵥ v = fun _ : Fin n => ∑ j : Fin n, v j := by
  classical
  ext i
  simpa [allOnes, Matrix.mulVec] using (one_dotProduct (v := v) : (1 : Fin n → ℚ) ⬝ᵥ v = _)

/-- For $n \neq 1$, the matrix $J-P$ (with $P$ a permutation matrix) has rank $n$. -/
theorem rank_allOnes_sub_permMatrix {n : ℕ} (hn : n ≠ 1) (σ : Perm (Fin n)) :
    (allOnes n - σ.permMatrix ℚ).rank = n := by
  classical
  -- show injective of mulVecLin
  have hinj : Function.Injective (allOnes n - σ.permMatrix ℚ).mulVecLin := by
    -- kernel trivial
    refine (LinearMap.ker_eq_bot).1 ?_
    refine (LinearMap.ker_eq_bot'.mpr ?_)
    intro v hv

    have hv0 : allOnes n *ᵥ v - (σ.permMatrix ℚ) *ᵥ v = 0 := by
      -- `hv : (J-P)*v = 0`, unfold and rewrite the `sub`-action.
      simpa [Matrix.mulVecLin_apply, Matrix.sub_mulVec] using hv

    have hv1 : allOnes n *ᵥ v = (σ.permMatrix ℚ) *ᵥ v := by
      exact sub_eq_zero.mp hv0

    -- left side is constant sum
    have hconst : (σ.permMatrix ℚ) *ᵥ v = fun _ : Fin n => ∑ j : Fin n, v j := by
      simpa [allOnes_mulVec] using hv1.symm

    -- permMatrix mulVec formula
    have hperm : (σ.permMatrix ℚ) *ᵥ v = v ∘ σ := by
      simpa using (Matrix.permMatrix_mulVec (σ := σ) (R := ℚ) (v := v))

    -- conclude v is constant with value `s = ∑ v`
    have hvconst : ∀ i : Fin n, v i = ∑ j : Fin n, v j := by
      intro i
      let j : Fin n := σ⁻¹ i
      have : (v ∘ σ) j = ∑ k : Fin n, v k := by
        have := congrFun (by simpa [hperm] using hconst) j
        simpa using this
      simpa [j] using this

    let s : ℚ := ∑ j : Fin n, v j
    have hvconst' : ∀ i, v i = s := by
      intro i
      simpa [s] using hvconst i

    -- sum both sides to get s = n*s
    have hs : s = (n : ℚ) * s := by
      have hsum : (∑ j : Fin n, v j) = ∑ _j : Fin n, s := by
        show (Finset.univ.sum fun j : Fin n => v j) = Finset.univ.sum (fun _j : Fin n => s)
        refine Finset.sum_congr rfl ?_
        intro j hj
        simpa using hvconst' j
      have hconst2 : (∑ _j : Fin n, s) = (n : ℚ) * s := by
        calc
          (∑ _j : Fin n, s) = (Fintype.card (Fin n) : ℕ) • s := by
            simpa using
              (Finset.sum_const (a := s) (s := (Finset.univ : Finset (Fin n))))
          _ = (n : ℚ) * s := by
            simp [Fintype.card_fin, nsmul_eq_mul]
      simpa [s] using hsum.trans hconst2

    have hs0 : s = 0 := by
      have hs' : (n : ℚ) * s - s = 0 := by
        simpa using congrArg (fun t => (n : ℚ) * s - t) hs
      have hs'' : ((n : ℚ) - 1) * s = 0 := by
        simpa [sub_mul, one_mul] using hs'
      have hn' : ((n : ℚ) - 1) ≠ 0 := by
        have : (n : ℚ) ≠ (1 : ℚ) := by
          exact_mod_cast hn
        exact sub_ne_zero.mpr this
      exact (mul_eq_zero.mp hs'').resolve_left hn'

    -- conclude v = 0
    ext i
    simp [hvconst' i, hs0]

  -- compute rank
  simpa [Matrix.rank, LinearMap.finrank_range_of_inj hinj, finrank_pi, Fintype.card_fin]

end TilesRankPerm

Compilation

$ lake env lean TilesRankPerm.lean
TilesRankPerm.lean:69:12: warning: try 'simp' instead of 'simpa'
TilesRankPerm.lean:91:2: warning: try 'simp' instead of 'simpa'