Non-hyperbolic toral automorphisms have no return growth: the criterion is the trace

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #179 (out of #19 and #177).

For B ∈ SL₂(ℤ) with |tr B| ≤ 2, toral B has no return growth at any rate (★★★ not_hasReturnGrowth_toral_of_abs_trace_le_two): some power Bᵗ − 1 is singular, and the kernel of a singular toral endomorphism is infinite (★★ infinite_ker_toral_of_det_eq_zero) — a nonzero integer kernel vector k gives the line s ↦ s·k/kᵢ mod ℤ², injective on [0, 1). The five cases are Cayley–Hamilton B² = (tr B)·B − 1: tr = 0 gives B⁴ = 1, tr = 1 gives B⁶ = 1, tr = −1 gives B³ = 1, tr = 2 gives (B − 1)² = 0, tr = −2 gives (B + 1)² = 0 and B² − 1 = −2(B + 1).

With #178 this is the characterisation ★★★ hasReturnGrowth_toral_iff: an element of SL₂(ℤ) has return growth at some rate iff |tr B| > 2 — the return criterion (#177) on integer matrices is decided by one integer.

Honest scope

• det B = 1 throughout, as in #178.
• The rate in the hyperbolic case is log ρ (#178); the characterisation here only asserts existence of a rate, which is what decides the criterion.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8 (classification of elements of SL₂(ℤ) by the trace); Mathlib/Dynamics/ToralReturns.lean (#178), Mathlib/Dynamics/ReturnCriterion.lean (#177); specs/BACKLOG.md #179, #178, #19.

A singular integer matrix has a nonzero integer kernel vector

theorem MeasureTheory.exists_kernel_vector (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det = 0) : ∃ (k : Fin 2 → ℤ), k ≠ 0 ∧ (Matrix.toLin' C) k = 0

A 2 × 2 integer matrix of determinant 0 kills a nonzero integer vector.

A singular toral endomorphism has an infinite kernel

theorem MeasureTheory.realMat_eq_zero_of_toLin'_eq_zero (C : Matrix (Fin 2) (Fin 2) ℤ) {k : Fin 2 → ℤ} (hk : (Matrix.toLin' C) k = 0) : realMat C (↑(k 0), ↑(k 1)) = 0

theorem MeasureTheory.infinite_ker_toral_of_det_eq_zero (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det = 0) : Infinite { p : Torus2 // toral C p = 0 }

★★ The kernel of a singular toral endomorphism is infinite: the line through a nonzero integer kernel vector, parametrised by [0, 1), lies in it injectively.

The five non-hyperbolic cases

theorem MeasureTheory.exists_det_pow_sub_one_eq_zero (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1) (hτ : |B.trace| ≤ 2) : ∃ (t : ℕ), (B ^ (t + 1) - 1).det = 0

In each non-hyperbolic case some Bᵗ − 1 (t ≥ 1) is singular.

The converse, and the characterisation

theorem MeasureTheory.not_hasReturnGrowth_toral_of_abs_trace_le_two (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1) (hτ : |↑B.trace| ≤ 2) (h : ℝ) : ¬HasReturnGrowth (toral B) h

★★★ No non-hyperbolic element of SL₂(ℤ) has return growth: at some stroke every return set is infinite.

theorem MeasureTheory.hasReturnGrowth_toral_iff (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1) : (∃ (h : ℝ), HasReturnGrowth (toral B) h) ↔ 2 < |↑B.trace|

★★★ The return criterion on SL₂(ℤ) is decided by the trace: toral B has return growth at some rate iff |tr B| > 2.