Soundness of the free-locus certificate

One direction of the free-locus test: a flip-poly pencil has corank ≤ m at every point of size m, so corank > m at some point of size m certifies "not flip-poly". Over a field K, corank A = card ι - rank A for a square matrix A : Matrix ι ι K.

Main results

• rank_add_rank_le_fromBlocks: rank A + rank D ≤ rank (fromBlocks A B 0 D); corank_fromBlocks_le: corank (fromBlocks A B 0 D) ≤ corank A + corank D.
• rank_kronecker_one: rank (A ⊗ₖ 1_m) = m * rank A; corank_kronecker_one.
• corank_unit_sub_mul_le: corank (U - P * Q) ≤ m for U invertible and P of width m; corank_one_sub_nil_sub_mul_le: the same with U = 1 - N, N nilpotent.
• TriBounded, Cert: block upper-triangular matrices with one free diagonal block B and k further diagonal blocks of corank ≤ m; cert_corank: corank M - k * m ≤ corank B.

The general rank facts (subadditivity, rank–nullity, block-triangular and Kronecker bounds) are imported from Formalizations.LinearAlgebra.Matrix.Rank and Formalizations.LinearAlgebra.Matrix.Rank.Kronecker; this file restates the two it lists under Main results in terms of corank.

noncomputable def FreeLocusCertificate.corank {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (A : Matrix ι ι K) : ℕ

Corank of a square matrix: card ι - rank.

Equations

• FreeLocusCertificate.corank A = Fintype.card ι - A.rank

theorem FreeLocusCertificate.corank_eq_finrank_ker {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] (A : Matrix n n K) : corank A = Module.finrank K ↥A.mulVecLin.ker

theorem FreeLocusCertificate.corank_of_isUnit {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) (h : IsUnit A) : corank A = 0

theorem FreeLocusCertificate.rank_add_rank_le_fromBlocks {K : Type u_1} [Field K] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] (A : Matrix n n K) (B : Matrix n m K) (D : Matrix m m K) : A.rank + D.rank ≤ (Matrix.fromBlocks A B 0 D).rank

(1) rank A + rank D ≤ rank (fromBlocks A B 0 D); this is Matrix.rank_add_rank_le_rank_fromBlocks_zero₂₁.

theorem FreeLocusCertificate.corank_fromBlocks_le {K : Type u_1} [Field K] {n : Type u_2} {m : Type u_3} [Fintype n] [Fintype m] (A : Matrix n n K) (B : Matrix n m K) (D : Matrix m m K) : corank (Matrix.fromBlocks A B 0 D) ≤ corank A + corank D

(1) corank (fromBlocks A B 0 D) ≤ corank A + corank D.

theorem FreeLocusCertificate.rank_kronecker_one {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] {m : ℕ} (A : Matrix n n K) : (Matrix.kroneckerMap (fun (x1 x2 : K) => x1 * x2) A 1).rank = m * A.rank

(2) rank (A ⊗ₖ I_m) = m * rank A; this is Matrix.rank_kronecker_one with p = Fin m.

theorem FreeLocusCertificate.corank_kronecker_one {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] {m : ℕ} (A : Matrix n n K) : corank (Matrix.kroneckerMap (fun (x1 x2 : K) => x1 * x2) A 1) = m * corank A

(2) corank (A ⊗ₖ I_m) = m * corank A.

theorem FreeLocusCertificate.corank_unit_sub_le {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (U E : Matrix ι ι K) (hU : IsUnit U) (k : ℕ) (hE : E.rank ≤ k) : corank (U - E) ≤ k

(3) Invertible minus a matrix of rank ≤ k has corank ≤ k; this is FreeLocus.corank_unit_sub_le.

theorem FreeLocusCertificate.corank_unit_sub_mul_le {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {m : ℕ} (U : Matrix ι ι K) (hU : IsUnit U) (P : Matrix ι (Fin m) K) (Q : Matrix (Fin m) ι K) : corank (U - P * Q) ≤ m

(3) Flip-poly bound: corank (U - P * Q) ≤ m for U invertible, P with m columns.

theorem FreeLocusCertificate.corank_one_sub_nil_sub_mul_le {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {m : ℕ} (N : Matrix ι ι K) (hN : IsNilpotent N) (P : Matrix ι (Fin m) K) (Q : Matrix (Fin m) ι K) : corank (1 - N - P * Q) ≤ m

(3) Same with U = 1 - N, N nilpotent.

inductive FreeLocusCertificate.TriBounded {K : Type u_1} [Field K] (c : ℕ) (ι : Type) [Fintype ι] [DecidableEq ι] : Matrix ι ι K → ℕ → Prop

Block upper-triangular matrices whose k diagonal blocks (k ≥ 1) all have corank ≤ c.

• single {K : Type u_1} [Field K] {c : ℕ} {ι : Type} [Fintype ι] [DecidableEq ι] (D : Matrix ι ι K) (h : corank D ≤ c) : TriBounded c ι D 1
• cons {K : Type u_1} [Field K] {c : ℕ} {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (D₁ : Matrix ι ι K) (Y : Matrix ι κ K) (D₂ : Matrix κ κ K) (k : ℕ) (h : corank D₁ ≤ c) (hD : TriBounded c κ D₂ k) : TriBounded c (ι ⊕ κ) (Matrix.fromBlocks D₁ Y 0 D₂) (k + 1)

theorem FreeLocusCertificate.TriBounded.corank_le {K : Type u_1} [Field K] {c : ℕ} {ι : Type} [Fintype ι] [DecidableEq ι] {D : Matrix ι ι K} {k : ℕ} (h : TriBounded c ι D k) : corank D ≤ k * c

inductive FreeLocusCertificate.Cert {K : Type u_1} [Field K] (c : ℕ) {β : Type} [Fintype β] [DecidableEq β] (B : Matrix β β K) (ι : Type) [Fintype ι] [DecidableEq ι] : Matrix ι ι K → ℕ → Prop

Block upper-triangular matrices with one free diagonal block B (anywhere on the diagonal) and k further diagonal blocks of corank ≤ c each.

• self {K : Type u_1} [Field K] {c : ℕ} {β : Type} [Fintype β] [DecidableEq β] {B : Matrix β β K} : Cert c B β B 0
• here {K : Type u_1} [Field K] {c : ℕ} {β : Type} [Fintype β] [DecidableEq β] {B : Matrix β β K} {κ : Type} [Fintype κ] [DecidableEq κ] (Y : Matrix β κ K) (D : Matrix κ κ K) (k : ℕ) (hD : TriBounded c κ D k) : Cert c B (β ⊕ κ) (Matrix.fromBlocks B Y 0 D) k
• there {K : Type u_1} [Field K] {c : ℕ} {β : Type} [Fintype β] [DecidableEq β] {B : Matrix β β K} {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (D₁ : Matrix ι ι K) (Y : Matrix ι κ K) (M' : Matrix κ κ K) (k : ℕ) (h : corank D₁ ≤ c) (hM : Cert c B κ M' k) : Cert c B (ι ⊕ κ) (Matrix.fromBlocks D₁ Y 0 M') (k + 1)

theorem FreeLocusCertificate.Cert.corank_le {K : Type u_1} [Field K] {c : ℕ} {β : Type} [Fintype β] [DecidableEq β] {B : Matrix β β K} {ι : Type} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι K} {k : ℕ} (h : Cert c B ι M k) : corank M ≤ corank B + k * c

theorem FreeLocusCertificate.cert_corank {K : Type u_1} [Field K] {c : ℕ} {β : Type} [Fintype β] [DecidableEq β] {B : Matrix β β K} {ι : Type} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι K} {k : ℕ} (h : Cert c B ι M k) : corank M - k * c ≤ corank B

(4) The certificate: corank B ≥ corank M - k * m.