The linear algebra behind the atoms of the size chain

Linear-algebra core of the atom criterion for the 4d × 4d pencil 𝐋 of the size chain (Lemma 6.2(c)). The pencil is an atom when the coefficient matrices 𝖢, 𝖣 generate the full matrix algebra and 𝖣 and 𝖤 = 𝖣 − 1 − 𝖢² are invertible. This file proves these three facts for the two families used in the paper:

• 𝖣_d = diag(3, 4, …, d + 2) and the cyclic permutation matrix 𝖢_d ((𝖢_d)_{i, i+1} = 1, indices mod d), for every d ≥ 1, over any field of characteristic 0;
• 𝖣 = diag(λ, λ + 1) and the swap 𝖢 = 𝖢_2 (the matrices of F^{(λ)}), over any field.

That a diagonal matrix with distinct eigenvalues and the cyclic permutation matrix generate the full matrix algebra is a classical fact (Lagrange interpolation gives the diagonal matrix units, and the cycle moves them around); it is proved here only because we did not find it in Mathlib. The invertibility of 𝖤_d uses Mathlib's Gershgorin theorem (det_ne_zero_of_sum_row_lt_diag): 𝖤_d is strictly diagonally dominant over ℚ, and the statement is transferred to any field of characteristic 0 through Rat.castHom.

The step "these conditions imply that the pencil is an atom" is Cohn's Theorem 5.8.8 (in the form of Helton–Klep–Volčič, Remark 2.6); it is not formalized here.

Main results

• ThreeAxes.SizeChain.adjoin_cyc_diagonal_eq_top: if v is injective, then Algebra.adjoin K {cyc K d, diagonal v} = ⊤.
• adjoin_cyc_diagD_eq_top: 𝖢_d and 𝖣_d generate M_d(K) (characteristic 0).
• det_diagD_ne_zero, det_matE_ne_zero: 𝖣_d and 𝖤_d = 𝖣_d − 1 − 𝖢_d² are invertible (characteristic 0).
• adjoin_swap_diagLam_eq_top: 𝖢_2 and diag(λ, λ + 1) generate M_2(K).
• det_diagLam_ne_zero_and_iff: diag(λ, λ+1) and diag(λ, λ+1) − 1 − 𝖢_2² are both invertible iff λ ∉ {−1, 0, 1, 2}.

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.SizeChain.cyc (K : Type u_1) [Zero K] [One K] (d : ℕ) [NeZero d] : Matrix (Fin d) (Fin d) K

The cyclic permutation matrix 𝖢_d: (𝖢_d)_{i, i+1} = 1, indices mod d.

Equations

• ThreeAxes.SizeChain.cyc K d = Matrix.of fun (i j : Fin d) => if j = i + 1 then 1 else 0

def ThreeAxes.SizeChain.diagD (K : Type u_1) [CommRing K] (d : ℕ) : Matrix (Fin d) (Fin d) K

𝖣_d = diag(3, 4, …, d + 2).

Equations

• ThreeAxes.SizeChain.diagD K d = Matrix.diagonal fun (i : Fin d) => ↑↑i + 3

def ThreeAxes.SizeChain.matE (K : Type u_1) [CommRing K] (d : ℕ) [NeZero d] : Matrix (Fin d) (Fin d) K

𝖤_d = 𝖣_d − 1 − 𝖢_d².

Equations

• ThreeAxes.SizeChain.matE K d = ThreeAxes.SizeChain.diagD K d - 1 - ThreeAxes.SizeChain.cyc K d * ThreeAxes.SizeChain.cyc K d

theorem ThreeAxes.SizeChain.single_mem_adjoin_diagonal {K : Type u_1} [Field K] {n : Type u_2} [Fintype n] [DecidableEq n] {v : n → K} (hv : Function.Injective v) (i : n) : Matrix.single i i 1 ∈ K[Matrix.diagonal v]

A diagonal matrix with distinct eigenvalues generates every diagonal matrix unit (Lagrange interpolation).

theorem ThreeAxes.SizeChain.adjoin_cyc_diagonal_eq_top {K : Type u_1} [Field K] {d : ℕ} [NeZero d] {v : Fin d → K} (hv : Function.Injective v) : K[cyc K d, Matrix.diagonal v] = ⊤

A diagonal matrix with distinct eigenvalues and the cyclic permutation matrix generate the full matrix algebra. Classical; see the module docstring.

The family 𝖣_d = diag(3, …, d + 2), 𝖢_d

theorem ThreeAxes.SizeChain.diagD_injective (K : Type u_1) [Field K] [CharZero K] (d : ℕ) : Function.Injective fun (i : Fin d) => ↑↑i + 3

theorem ThreeAxes.SizeChain.adjoin_cyc_diagD_eq_top (K : Type u_1) [Field K] [CharZero K] (d : ℕ) [NeZero d] : K[cyc K d, diagD K d] = ⊤

𝖢_d and 𝖣_d generate M_d(K).

theorem ThreeAxes.SizeChain.det_diagD_ne_zero (K : Type u_1) [Field K] [CharZero K] (d : ℕ) : (diagD K d).det ≠ 0

𝖣_d is invertible.

theorem ThreeAxes.SizeChain.cyc_mul_cyc_apply (d : ℕ) [NeZero d] {R : Type u_2} [CommRing R] (i j : Fin d) : (cyc R d * cyc R d) i j = if j = i + 1 + 1 then 1 else 0

theorem ThreeAxes.SizeChain.det_matE_real_ne_zero (d : ℕ) [NeZero d] : (matE ℝ d).det ≠ 0

Strict diagonal dominance of 𝖤_d over ℝ: Mathlib's Gershgorin theorem det_ne_zero_of_sum_row_lt_diag.

theorem ThreeAxes.SizeChain.mapMatrix_matE (K : Type u_1) [Field K] [CharZero K] (d : ℕ) [NeZero d] : (Rat.castHom K).mapMatrix (matE ℚ d) = matE K d

theorem ThreeAxes.SizeChain.det_matE_rat_ne_zero (d : ℕ) [NeZero d] : (matE ℚ d).det ≠ 0

theorem ThreeAxes.SizeChain.det_matE_ne_zero (K : Type u_1) [Field K] [CharZero K] (d : ℕ) [NeZero d] : (matE K d).det ≠ 0

𝖤_d = 𝖣_d − 1 − 𝖢_d² is invertible over every field of characteristic 0.

The matrices of F^{(λ)}

theorem ThreeAxes.SizeChain.cyc_two {K : Type u_1} [Field K] : cyc K 2 = !![0, 1; 1, 0]

For d = 2, 𝖢_2 is the swap.

theorem ThreeAxes.SizeChain.cyc_two_mul_self {K : Type u_1} [Field K] : cyc K 2 * cyc K 2 = 1

theorem ThreeAxes.SizeChain.adjoin_swap_diagLam_eq_top {K : Type u_1} [Field K] (l : K) : K[cyc K 2, Matrix.diagonal ![l, l + 1]] = ⊤

𝖢_2 (the swap) and diag(λ, λ + 1) generate M_2(K), for every λ.

theorem ThreeAxes.SizeChain.det_diagLam_ne_zero_and_iff {K : Type u_1} [Field K] (l : K) : (Matrix.diagonal ![l, l + 1]).det ≠ 0 ∧ (Matrix.diagonal ![l, l + 1] - 1 - cyc K 2 * cyc K 2).det ≠ 0 ↔ l ≠ -1 ∧ l ≠ 0 ∧ l ≠ 1 ∧ l ≠ 2

diag(λ, λ + 1) and 𝖤 = diag(λ, λ + 1) − 1 − 𝖢_2² = diag(λ, λ + 1) − 2 are both invertible iff λ ∉ {−1, 0, 1, 2}.