Common definitions for the three-axes files

Definitions shared by Extractors, TraceResidue and DegenerateResidue.

Main definitions and results

• M2 R: 2 × 2 matrices over R.
• d3, det4: an explicit 4 × 4 determinant (Laplace along row 0, 3 × 3 minors written out as d3, the polynomial of Mathlib's Matrix.det_fin_three). Mathlib has det_fin_two and det_fin_three but no 4 × 4 analogue.
• blk A B C: the 4 × 4 matrix [[A + B, A], [A, A + C]] built from 2 × 2 blocks.
• Nsq a b: the square-zero rank-one matrix with kernel and image spanned by (a, b); Nsq_sq.
• Wx, Wy, Wz (and the inverses Wxi, Wyi, Wzi, Xxi, Xyi): the integer witness matrices used in TraceResidue.witness and DegenerateResidue.F2_witness.

@[reducible, inline]

abbrev ThreeAxes.M2 (R : Type u_2) [CommRing R] : Type u_2

2 × 2 matrices over R.

Equations

• ThreeAxes.M2 R = Matrix (Fin 2) (Fin 2) R

def ThreeAxes.d3 {R : Type u_1} [CommRing R] (a b c d e f g h i : R) : R

3 × 3 determinant polynomial (same shape as Matrix.det_fin_three).

Equations

• ThreeAxes.d3 a b c d e f g h i = a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g

theorem ThreeAxes.det4 {R : Type u_1} [CommRing R] (A : Matrix (Fin 4) (Fin 4) R) : A.det = A 0 0 * d3 (A 1 1) (A 1 2) (A 1 3) (A 2 1) (A 2 2) (A 2 3) (A 3 1) (A 3 2) (A 3 3) - A 0 1 * d3 (A 1 0) (A 1 2) (A 1 3) (A 2 0) (A 2 2) (A 2 3) (A 3 0) (A 3 2) (A 3 3) + A 0 2 * d3 (A 1 0) (A 1 1) (A 1 3) (A 2 0) (A 2 1) (A 2 3) (A 3 0) (A 3 1) (A 3 3) - A 0 3 * d3 (A 1 0) (A 1 1) (A 1 2) (A 2 0) (A 2 1) (A 2 2) (A 3 0) (A 3 1) (A 3 2)

Explicit 4 × 4 determinant: Laplace along row 0, minors by d3.

def ThreeAxes.blk {R : Type u_1} [CommRing R] (A B C : M2 R) : Matrix (Fin 4) (Fin 4) R

The 4 × 4 matrix [[A + B, A], [A, A + C]] built from 2 × 2 blocks.

Equations

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

def ThreeAxes.Nsq {R : Type u_1} [CommRing R] (a b : R) : M2 R

The square-zero rank-one matrix with kernel and image spanned by (a, b).

Equations

• ThreeAxes.Nsq a b = !![a * b, -a ^ 2; b ^ 2, -(a * b)]

theorem ThreeAxes.Nsq_sq {R : Type u_1} [CommRing R] (a b : R) : Nsq a b * Nsq a b = 0

def ThreeAxes.Wx : Matrix (Fin 2) (Fin 2) ℚ

Integer witness matrices W_j ∈ SL₂(ℤ) (over ℚ), with inverses W_j⁻¹ and the inverses of W_j − 1 for j = x, y.

Equations

• ThreeAxes.Wx = !![7, -1; 1, 0]

def ThreeAxes.Wy : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Wy = !![1, -1; 2, -1]

def ThreeAxes.Wz : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Wz = !![2, -1; 7, -3]

def ThreeAxes.Wxi : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Wxi = !![0, 1; -1, 7]

def ThreeAxes.Wyi : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Wyi = !![-1, 1; -2, 1]

def ThreeAxes.Wzi : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Wzi = !![-3, 1; -7, 2]

def ThreeAxes.Xxi : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Xxi = !![1 / 5, -1 / 5; 1 / 5, -6 / 5]

def ThreeAxes.Xyi : Matrix (Fin 2) (Fin 2) ℚ

Equations

• ThreeAxes.Xyi = !![-1, 1 / 2; -1, 0]