Weighted trinomials for the three-axes problem

Finite identities behind the weighted-trinomial construction: a hidden commutator in GL₂, a curve of nilpotent 2×2 matrices realising the weighted trinomials, and the Schur complement of the rank-two block matrix.

Main results

• sq_eq_trace_smul_sub_det_smul: Cayley–Hamilton for 2×2 matrices, X * X = tr X • X − det X • 1.
• hidden_commutator: if tr X = tr Y = −1, T = 1 + X + Y satisfies T * T = 0 and X, Y are invertible with a = det X, b = det Y, then (X Y) (Y X) (X Y)⁻¹ (Y X)⁻¹ = 1 + (a⁻¹ − b⁻¹) • T; the commutator is unipotent.
• weighted_trinomial: for any three matrices n 0, n 1, n 2, with T i = (n i − z n (i+1) + z² n (i+2)) / (1 + z³) and X i = −1/(1+z) • 1 + T i, one has 1 + X i + z X (i+1) = n i. weighted_curve: the instance N i = !![i t², −t; i² t³, −i t²]; N_sq: N i * N i = 0.
• schur_r2: over any ring, with Q = A + 2B and S = A + B − C Q⁻¹ C units, the block matrix !![A + B, C; C, A + 2B] has right inverse !![S⁻¹, −S⁻¹ C Q⁻¹; −Q⁻¹ C S⁻¹, Q⁻¹ + Q⁻¹ C S⁻¹ C Q⁻¹]; in particular its (1,1) entry is S⁻¹.

Related

Mathlib's block inverse through a Schur complement (Matrix.fromBlocks₁₁Invertible, Matrix.invOf_fromBlocks₂₂_eq) is stated over a CommRing; schur_r2 is the noncommutative 2 × 2 case with entries in a ring (compare ThreeAxes.InverseIdentities.schur_two, pivot in the other corner).

The hidden commutator

theorem ThreeAxes.WeightedTrinomials.sq_eq_trace_smul_sub_det_smul {R : Type u_1} [CommRing R] (X : Matrix (Fin 2) (Fin 2) R) : X * X = X.trace • X - X.det • 1

Cayley–Hamilton for 2×2 matrices; this is Matrix.mul_self_eq_trace_smul_sub_det_smul_fin_two (in Formalizations.LinearAlgebra.Matrix.FinTwo).

theorem ThreeAxes.WeightedTrinomials.hidden_commutator {K : Type u_1} [Field K] (X Y : Matrix (Fin 2) (Fin 2) K) (hX : X.trace = -1) (hY : Y.trace = -1) (hT : (1 + X + Y) * (1 + X + Y) = 0) (ha : X.det ≠ 0) (hb : Y.det ≠ 0) : X * Y * (Y * X) * (X * Y)⁻¹ * (Y * X)⁻¹ = 1 + (X.det⁻¹ - Y.det⁻¹) • (1 + X + Y)

The weighted curve

noncomputable def ThreeAxes.WeightedTrinomials.trinomial {K : Type u_1} [Field K] (z : K) (n : Fin 3 → Matrix (Fin 2) (Fin 2) K) (i : Fin 3) : Matrix (Fin 2) (Fin 2) K

The weighted trinomial built from three matrices n 0, n 1, n 2.

Equations

• ThreeAxes.WeightedTrinomials.trinomial z n i = (1 + z ^ 3)⁻¹ • (n i - z • n (i + 1) + z ^ 2 • n (i + 2))

noncomputable def ThreeAxes.WeightedTrinomials.curvePoint {K : Type u_1} [Field K] (z : K) (n : Fin 3 → Matrix (Fin 2) (Fin 2) K) (i : Fin 3) : Matrix (Fin 2) (Fin 2) K

X i = λ • 1 + T i with λ = −1/(1+z).

Equations

• ThreeAxes.WeightedTrinomials.curvePoint z n i = -(1 + z)⁻¹ • 1 + ThreeAxes.WeightedTrinomials.trinomial z n i

theorem ThreeAxes.WeightedTrinomials.weighted_trinomial {K : Type u_1} [Field K] (z : K) (hz : 1 + z ≠ 0) (hz3 : 1 + z ^ 3 ≠ 0) (n : Fin 3 → Matrix (Fin 2) (Fin 2) K) (i : Fin 3) : 1 + curvePoint z n i + z • curvePoint z n (i + 1) = n i

def ThreeAxes.WeightedTrinomials.N {K : Type u_1} [Field K] (t : K) (i : Fin 3) : Matrix (Fin 2) (Fin 2) K

The nilpotent curve N i = !![i t², −t; i² t³, −i t²].

Equations

• ThreeAxes.WeightedTrinomials.N t i = !![↑↑i * t ^ 2, -t; ↑↑i ^ 2 * t ^ 3, -(↑↑i * t ^ 2)]

theorem ThreeAxes.WeightedTrinomials.N_sq {K : Type u_1} [Field K] (t : K) (i : Fin 3) : N t i * N t i = 0

theorem ThreeAxes.WeightedTrinomials.weighted_curve {K : Type u_1} [Field K] (t z : K) (hz : 1 + z ≠ 0) (hz3 : 1 + z ^ 3 ≠ 0) (i : Fin 3) : 1 + curvePoint z (N t) i + z • curvePoint z (N t) (i + 1) = N t i

The Schur complement for r = 2

theorem ThreeAxes.WeightedTrinomials.schur_r2 {R : Type u_1} [Ring R] (A B C : R) (Q S : Rˣ) (hQ : ↑Q = A + 2 * B) (hS : ↑S = A + B - C * ↑Q⁻¹ * C) : !![A + B, C; C, A + 2 * B] * !![↑S⁻¹, -(↑S⁻¹ * C * ↑Q⁻¹); -(↑Q⁻¹ * C * ↑S⁻¹), ↑Q⁻¹ + ↑Q⁻¹ * C * ↑S⁻¹ * C * ↑Q⁻¹] = 1

theorem ThreeAxes.WeightedTrinomials.schur_r2_col {R : Type u_1} [Ring R] (A B C : R) (Q S : Rˣ) (hQ : ↑Q = A + 2 * B) (hS : ↑S = A + B - C * ↑Q⁻¹ * C) : (A + B) * ↑S⁻¹ + C * -(↑Q⁻¹ * C * ↑S⁻¹) = 1 ∧ C * ↑S⁻¹ + (A + 2 * B) * -(↑Q⁻¹ * C * ↑S⁻¹) = 0

The (1,1) entry of the inverse of the block matrix is the inverse Schur complement.