The exact arc as a conjugate, and the parabolic family

The exact arc exactArc i t η of ExactArc is the conjugate of the antidiagonal matrix U₀ = !![0, -t; -η, 0] by the i-th power of the unipotent matrix K t = !![1, 0; t, 1]. Conjugating the square-zero matrix N t = !![0, t; 0, 0] by the same powers gives a family of rank-one square-zero matrices whose cyclic products have an explicit trace.

Main results

• K_pow: (K t)^i = !![1, 0; i t, 1]; K_mul_K_neg: K t * K (-t) = 1.
• exactArc_eq_conj: exactArc i t η = (K t)^i * U₀ * (K (-t))^i.
• conj_mul_conj_eq_of_mul_eq, units_conj_mul_conj_eq: if U * U = c with c central, every conjugate of U squares to c (the second through Mathlib's Units.conj_pow). exactArc_sq_of_conj: the square identity exactArc_sq recovered from U₀ * U₀ = (t η) • 1.
• parabolic_eq_smul_col_mul_row: N_j = t • (c_j * r_j) with c_j = (1, j t)ᵀ, r_j = (-j t, 1); row_mul_col: r_a * c_b = (b - a) t; parabolic_mul_self: N_j * N_j = 0.
• trace_prod_parabolic: for a nonempty list j₁, …, j_q, trace (N_{j₁} ⋯ N_{j_q}) = t^(2q) ∏ₗ (j_{l+1} − j_l) with j_{q+1} = j₁; cycDiff_eq_prod_rotate writes the product as a product over zip l (l.rotate 1).
• det_one_add_allOnes: det (1 + J) = card n + 1 for the all-ones matrix J, from Mathlib's Matrix.det_one_add_replicateCol_mul_replicateRow.

The exact arc as a conjugate

def ThreeAxes.ParabolicFamily.K {R : Type u_1} [CommRing R] (t : R) : Matrix (Fin 2) (Fin 2) R

The unipotent matrix !![1, 0; t, 1].

Equations

• ThreeAxes.ParabolicFamily.K t = !![1, 0; t, 1]

def ThreeAxes.ParabolicFamily.U0 {R : Type u_1} [CommRing R] (t η : R) : Matrix (Fin 2) (Fin 2) R

The antidiagonal matrix !![0, -t; -η, 0] = −(t E₁₂ + η E₂₁).

Equations

• ThreeAxes.ParabolicFamily.U0 t η = !![0, -t; -η, 0]

theorem ThreeAxes.ParabolicFamily.K_mul_K {R : Type u_1} [CommRing R] (s t : R) : K s * K t = K (s + t)

theorem ThreeAxes.ParabolicFamily.K_zero {R : Type u_1} [CommRing R] : K 0 = 1

theorem ThreeAxes.ParabolicFamily.K_mul_K_neg {R : Type u_1} [CommRing R] (t : R) : K t * K (-t) = 1

theorem ThreeAxes.ParabolicFamily.K_neg_mul_K {R : Type u_1} [CommRing R] (t : R) : K (-t) * K t = 1

theorem ThreeAxes.ParabolicFamily.K_pow {R : Type u_1} [CommRing R] (t : R) (i : ℕ) : K t ^ i = !![1, 0; ↑i * t, 1]

theorem ThreeAxes.ParabolicFamily.K_pow_eq {R : Type u_1} [CommRing R] (t : R) (i : ℕ) : K t ^ i = K (↑i * t)

theorem ThreeAxes.ParabolicFamily.U0_mul_self {R : Type u_1} [CommRing R] (t η : R) : U0 t η * U0 t η = (t * η) • 1

theorem ThreeAxes.ParabolicFamily.exactArc_eq_conj_K {R : Type u_1} [CommRing R] (i t η : R) : ExactArc.exactArc i t η = K (i * t) * U0 t η * K (-(i * t))

The exact arc with a parameter i in the ring is the conjugate of U₀ by K (i t).

theorem ThreeAxes.ParabolicFamily.exactArc_eq_conj {R : Type u_1} [CommRing R] (i : ℕ) (t η : R) : ExactArc.exactArc (↑i) t η = K t ^ i * U0 t η * K (-t) ^ i

The exact arc is the conjugate of U₀ by the i-th power of K t.

theorem ThreeAxes.ParabolicFamily.conj_mul_conj_eq_of_mul_eq {A : Type u_2} [Ring A] (U c g h : A) (hU : U * U = c) (hc : ∀ (x : A), Commute c x) (hhg : h * g = 1) (hgh : g * h = 1) : g * U * h * (g * U * h) = c

If U * U = c with c central and h * g = g * h = 1, then (g U h)² = c.

theorem ThreeAxes.ParabolicFamily.units_conj_mul_conj_eq {A : Type u_2} [Ring A] (U c : A) (g : Aˣ) (hU : U * U = c) (hc : ∀ (x : A), Commute c x) : ↑g * U * ↑g⁻¹ * (↑g * U * ↑g⁻¹) = c

Conjugation by a unit preserves a central square (Mathlib's Units.conj_pow with n = 2).

theorem ThreeAxes.ParabolicFamily.exactArc_sq_of_conj {R : Type u_1} [CommRing R] (i t η : R) : ExactArc.exactArc i t η * ExactArc.exactArc i t η = (t * η) • 1

exactArc_sq again, as a corollary of U₀ * U₀ = (t η) • 1 and conjugation.

The parabolic family

def ThreeAxes.ParabolicFamily.N {R : Type u_1} [CommRing R] (t : R) : Matrix (Fin 2) (Fin 2) R

The square-zero matrix !![0, t; 0, 0].

Equations

• ThreeAxes.ParabolicFamily.N t = !![0, t; 0, 0]

def ThreeAxes.ParabolicFamily.parabolic {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : Matrix (Fin 2) (Fin 2) R

N_j = (K t)^j * N t * (K (-t))^j.

Equations

• ThreeAxes.ParabolicFamily.parabolic t j = ThreeAxes.ParabolicFamily.K t ^ j * ThreeAxes.ParabolicFamily.N t * ThreeAxes.ParabolicFamily.K (-t) ^ j

def ThreeAxes.ParabolicFamily.col {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : Matrix (Fin 2) (Fin 1) R

The column (1, j t)ᵀ.

Equations

• ThreeAxes.ParabolicFamily.col t j = !![1; ↑j * t]

def ThreeAxes.ParabolicFamily.row {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : Matrix (Fin 1) (Fin 2) R

The row (-j t, 1).

Equations

• ThreeAxes.ParabolicFamily.row t j = !![-(↑j * t), 1]

def ThreeAxes.ParabolicFamily.outer {R : Type u_1} [CommRing R] (a b : R) : Matrix (Fin 2) (Fin 2) R

The rank-one matrix (1, a)ᵀ (-b, 1).

Equations

• ThreeAxes.ParabolicFamily.outer a b = !![-b, 1; -(a * b), a]

theorem ThreeAxes.ParabolicFamily.outer_mul_outer {R : Type u_1} [CommRing R] (a b a' b' : R) : outer a b * outer a' b' = (a' - b) • outer a b'

theorem ThreeAxes.ParabolicFamily.trace_outer {R : Type u_1} [CommRing R] (a b : R) : (outer a b).trace = a - b

theorem ThreeAxes.ParabolicFamily.parabolic_eq_outer {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : parabolic t j = t • outer (↑j * t) (↑j * t)

theorem ThreeAxes.ParabolicFamily.col_mul_row {R : Type u_1} [CommRing R] (t : R) (a b : ℕ) : col t a * row t b = outer (↑a * t) (↑b * t)

theorem ThreeAxes.ParabolicFamily.parabolic_eq_smul_col_mul_row {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : parabolic t j = t • (col t j * row t j)

theorem ThreeAxes.ParabolicFamily.row_mul_col {R : Type u_1} [CommRing R] (t : R) (a b : ℕ) : row t a * col t b = Matrix.of fun (x x_1 : Fin 1) => (↑b - ↑a) * t

theorem ThreeAxes.ParabolicFamily.parabolic_mul_self {R : Type u_1} [CommRing R] (t : R) (j : ℕ) : parabolic t j * parabolic t j = 0

def ThreeAxes.ParabolicFamily.chainDiff {R : Type u_1} [CommRing R] : ℕ → List ℕ → R

∏ (j_{l+1} − j_l) along the open chain a, j₁, …, j_r.

Equations

• ThreeAxes.ParabolicFamily.chainDiff x✝ [] = 1
• ThreeAxes.ParabolicFamily.chainDiff x✝ (b :: bs) = (↑b - ↑x✝) * ThreeAxes.ParabolicFamily.chainDiff b bs

def ThreeAxes.ParabolicFamily.closedDiff {R : Type u_1} [CommRing R] (f : ℕ) : ℕ → List ℕ → R

∏ (j_{l+1} − j_l) along the chain a, j₁, …, j_r closed by f.

Equations

• ThreeAxes.ParabolicFamily.closedDiff f x✝ [] = ↑f - ↑x✝
• ThreeAxes.ParabolicFamily.closedDiff f x✝ (b :: bs) = (↑b - ↑x✝) * ThreeAxes.ParabolicFamily.closedDiff f b bs

def ThreeAxes.ParabolicFamily.cycDiff {R : Type u_1} [CommRing R] : List ℕ → R

The cyclic product ∏ₗ (j_{l+1} − j_l), j_{q+1} = j₁, of a list j₁, …, j_q.

Equations

• ThreeAxes.ParabolicFamily.cycDiff [] = 1
• ThreeAxes.ParabolicFamily.cycDiff (a :: bs) = ThreeAxes.ParabolicFamily.closedDiff a a bs

theorem ThreeAxes.ParabolicFamily.closedDiff_eq {R : Type u_1} [CommRing R] (f a : ℕ) (bs : List ℕ) : closedDiff f a bs = chainDiff a bs * (↑f - ↑(bs.getLastD a))

theorem ThreeAxes.ParabolicFamily.closedDiff_eq_prod_zip {R : Type u_1} [CommRing R] (f a : ℕ) (bs : List ℕ) : closedDiff f a bs = (List.map (fun (p : ℕ × ℕ) => ↑p.2 - ↑p.1) ((a :: bs).zip (bs ++ [f]))).prod

theorem ThreeAxes.ParabolicFamily.cycDiff_eq_prod_rotate {R : Type u_1} [CommRing R] (l : List ℕ) : cycDiff l = (List.map (fun (p : ℕ × ℕ) => ↑p.2 - ↑p.1) (l.zip (l.rotate 1))).prod

The cyclic product as a product over consecutive pairs of l and its rotation.

theorem ThreeAxes.ParabolicFamily.prod_parabolic {R : Type u_1} [CommRing R] (t : R) (a : ℕ) (bs : List ℕ) : (List.map (parabolic t) (a :: bs)).prod = (t ^ (2 * bs.length + 1) * chainDiff a bs) • outer (↑a * t) (↑(bs.getLastD a) * t)

theorem ThreeAxes.ParabolicFamily.trace_prod_parabolic {R : Type u_1} [CommRing R] (t : R) (l : List ℕ) (hl : l ≠ []) : (List.map (parabolic t) l).prod.trace = t ^ (2 * l.length) * cycDiff l

The trace law: trace (N_{j₁} ⋯ N_{j_q}) = t^(2q) ∏ₗ (j_{l+1} − j_l), j_{q+1} = j₁.

The all-ones matrix

theorem ThreeAxes.ParabolicFamily.det_one_add_allOnes {R : Type u_1} [CommRing R] (n : Type u_2) [Fintype n] [DecidableEq n] : (1 + Matrix.of fun (x x_1 : n) => 1).det = ↑(Fintype.card n) + 1

det (1 + J) = card n + 1 for the all-ones matrix J (Mathlib's Matrix.det_one_add_replicateCol_mul_replicateRow).