The eight rank conditions for the chain pencil Q_r

Finite certificate of the eight rank conditions of Lemma 5.7(2), for r = 3 and r = 4.

Q_r is the (5r + 1) × (5r + 1) linear pencil C0 + u Cu + v Cv + w Cw of (5.1): five chain blocks (a letter u, v, w on the diagonal, −1 above it), a bottom row carrying the left coefficients α = (w, v, w, u, v) at the first position of each chain and a last column carrying the right coefficients ω at the last position (ω₂ = 1 is the constant). For r = 3 the chains are uuu, uuu, vvv, vvv, www; for r = 4 they are uvwu, uvwu, vwuv, vwuv, wuvw. The matrices below were generated from this description and coincide with scripts/smith_V1/verifica_T159.py (pencil(r) with rho_corregido(r)).

The eight conditions, over ℚ:

• EPIC (vertical): Cu, Cv, Cw have no common nonzero kernel vector, i.e. [Cu; Cv; Cw] has full column rank;
• EPIC (horizontal): Cuᵀ, Cvᵀ, Cwᵀ have no common nonzero kernel vector, i.e. [Cu Cv Cw] has full row rank;
• 𝒦_i^R = ker C0 ∩ ⋂_{j ≠ i} ker C_j = 0 and 𝒦_i^L = 0 (same with transposes), i = u, v, w.

Each condition is certified by a choice of n rows of the stacked 3n × n matrix and an integer matrix Y with Y * S = 1 for the selected n × n block S, checked by decide.

Not formalized. That these conditions imply that Q_r is an atom of ℂ⟨u, v, w⟩ is Cohn's Theorem 5.8.8 (in the form of Helton–Klep–Volčič, Remark 2.6), together with the argument of the proof of Lemma 5.7(2) (weak finiteness of Λ, free loci, HKV Thm 2.11–2.12). It is a hypothesis of the paper, not of this file.

Main results

• ThreeAxes.ChainPencil.noCommonKernel_of_certificate: a selection of rows with an integer left inverse certifies that three integer matrices have no common nonzero kernel vector over ℚ.
• ThreeAxes.ChainPencil.R3.eightConditions, ThreeAxes.ChainPencil.R4.eightConditions: the eight conditions for Q_3 and Q_4.

References

• P. M. Cohn, Free ideal rings and localization in general rings, Cambridge Univ. Press, 2006, Theorem 5.8.8.
• J. W. Helton, I. Klep, J. Volčič, Factorization of noncommutative polynomials and Nullstellensätze for the free algebra, IMRN 2022, Remark 2.6.

def ThreeAxes.ChainPencil.NoCommonKernel {n : ℕ} (M : Fin 3 → Matrix (Fin n) (Fin n) ℤ) : Prop

Three integer matrices have no common nonzero kernel vector over ℚ.

Equations

• ThreeAxes.ChainPencil.NoCommonKernel M = ∀ (v : Fin n → ℚ), (∀ (k : Fin 3), ((M k).map ⇑(Int.castRingHom ℚ)).mulVec v = 0) → v = 0

def ThreeAxes.ChainPencil.stackRows {n : ℕ} (M : Fin 3 → Matrix (Fin n) (Fin n) ℤ) (src : Fin n → Fin 3) (row : Fin n → Fin n) : Matrix (Fin n) (Fin n) ℤ

The n × n matrix whose i-th row is row row i of M (src i).

Equations

• ThreeAxes.ChainPencil.stackRows M src row = Matrix.of fun (i j : Fin n) => M (src i) (row i) j

theorem ThreeAxes.ChainPencil.noCommonKernel_of_certificate {n : ℕ} (M : Fin 3 → Matrix (Fin n) (Fin n) ℤ) (src : Fin n → Fin 3) (row : Fin n → Fin n) (Y : Matrix (Fin n) (Fin n) ℤ) (h : Y * stackRows M src row = 1) : NoCommonKernel M

A selection of rows of the stack [M 0; M 1; M 2] with an integer left inverse certifies NoCommonKernel M.

structure ThreeAxes.ChainPencil.EightConditions {n : ℕ} (C0 Cu Cv Cw : Matrix (Fin n) (Fin n) ℤ) : Prop

The eight rank conditions of Lemma 5.7(2) for a pencil C0 + u Cu + v Cv + w Cw.

• epicV : NoCommonKernel ![Cu, Cv, Cw]

  EPIC, vertical: [Cu; Cv; Cw] has full column rank.

• epicH : NoCommonKernel ![Cu.transpose, Cv.transpose, Cw.transpose]

  EPIC, horizontal: [Cu Cv Cw] has full row rank.

• kerUR : NoCommonKernel ![C0, Cv, Cw]

  𝒦_u^R = 0.

• kerVR : NoCommonKernel ![C0, Cu, Cw]

  𝒦_v^R = 0.

• kerWR : NoCommonKernel ![C0, Cu, Cv]

  𝒦_w^R = 0.

• kerUL : NoCommonKernel ![C0.transpose, Cv.transpose, Cw.transpose]

  𝒦_u^L = 0.

• kerVL : NoCommonKernel ![C0.transpose, Cu.transpose, Cw.transpose]

  𝒦_v^L = 0.

• kerWL : NoCommonKernel ![C0.transpose, Cu.transpose, Cv.transpose]

  𝒦_w^L = 0.

r = 3 (16 × 16)

def ThreeAxes.ChainPencil.R3.C0 : Matrix (Fin 16) (Fin 16) ℤ

The coefficient C0 of Q_3.

Equations

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

def ThreeAxes.ChainPencil.R3.Cu : Matrix (Fin 16) (Fin 16) ℤ

The coefficient Cu of Q_3.

Equations

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

def ThreeAxes.ChainPencil.R3.Cv : Matrix (Fin 16) (Fin 16) ℤ

The coefficient Cv of Q_3.

Equations

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

def ThreeAxes.ChainPencil.R3.Cw : Matrix (Fin 16) (Fin 16) ℤ

The coefficient Cw of Q_3.

Equations

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

def ThreeAxes.ChainPencil.R3.epicVY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for epicV: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.epicV : NoCommonKernel ![Cu, Cv, Cw]

def ThreeAxes.ChainPencil.R3.epicHY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for epicH: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.epicH : NoCommonKernel ![Cu.transpose, Cv.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R3.kerURY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerUR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerUR : NoCommonKernel ![C0, Cv, Cw]

def ThreeAxes.ChainPencil.R3.kerVRY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerVR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerVR : NoCommonKernel ![C0, Cu, Cw]

def ThreeAxes.ChainPencil.R3.kerWRY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerWR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerWR : NoCommonKernel ![C0, Cu, Cv]

def ThreeAxes.ChainPencil.R3.kerULY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerUL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerUL : NoCommonKernel ![C0.transpose, Cv.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R3.kerVLY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerVL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerVL : NoCommonKernel ![C0.transpose, Cu.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R3.kerWLY : Matrix (Fin 16) (Fin 16) ℤ

Certificate for kerWL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R3.kerWL : NoCommonKernel ![C0.transpose, Cu.transpose, Cv.transpose]

theorem ThreeAxes.ChainPencil.R3.eightConditions : EightConditions C0 Cu Cv Cw

The eight rank conditions of Lemma 5.7(2) hold for Q_3.

r = 4 (21 × 21)

def ThreeAxes.ChainPencil.R4.C0 : Matrix (Fin 21) (Fin 21) ℤ

The coefficient C0 of Q_4.

Equations

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

def ThreeAxes.ChainPencil.R4.Cu : Matrix (Fin 21) (Fin 21) ℤ

The coefficient Cu of Q_4.

Equations

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

def ThreeAxes.ChainPencil.R4.Cv : Matrix (Fin 21) (Fin 21) ℤ

The coefficient Cv of Q_4.

Equations

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

def ThreeAxes.ChainPencil.R4.Cw : Matrix (Fin 21) (Fin 21) ℤ

The coefficient Cw of Q_4.

Equations

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

def ThreeAxes.ChainPencil.R4.epicVY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for epicV: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.epicV : NoCommonKernel ![Cu, Cv, Cw]

def ThreeAxes.ChainPencil.R4.epicHY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for epicH: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.epicH : NoCommonKernel ![Cu.transpose, Cv.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R4.kerURY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerUR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerUR : NoCommonKernel ![C0, Cv, Cw]

def ThreeAxes.ChainPencil.R4.kerVRY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerVR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerVR : NoCommonKernel ![C0, Cu, Cw]

def ThreeAxes.ChainPencil.R4.kerWRY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerWR: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerWR : NoCommonKernel ![C0, Cu, Cv]

def ThreeAxes.ChainPencil.R4.kerULY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerUL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerUL : NoCommonKernel ![C0.transpose, Cv.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R4.kerVLY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerVL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerVL : NoCommonKernel ![C0.transpose, Cu.transpose, Cw.transpose]

def ThreeAxes.ChainPencil.R4.kerWLY : Matrix (Fin 21) (Fin 21) ℤ

Certificate for kerWL: a left inverse of the selected rows.

Equations

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

theorem ThreeAxes.ChainPencil.R4.kerWL : NoCommonKernel ![C0.transpose, Cu.transpose, Cv.transpose]

theorem ThreeAxes.ChainPencil.R4.eightConditions : EightConditions C0 Cu Cv Cw

The eight rank conditions of Lemma 5.7(2) hold for Q_4.