English
For a 2×2 matrix m over a field K with 2 ≠ 0, m is parabolic iff there exist a ∈ K and n ∈ Mat_2(K) with m = a I + n, n ≠ 0, and n^2 = 0.
Русский
Для любой 2×2 матрицы m над полем K с 2 ≠ 0 матрица параболична тогда и только тогда, когда существует a ∈ K и нильпотентная матрица n с m = a I + n, n ≠ 0, n^2 = 0.
LaTeX
$$$\text{IsParabolic}(m) \iff \exists a,n: m = a I + n \land n \neq 0 \land n^2 = 0.$$$
Lean4
/-- Characterization of parabolic elements: they have the form `a + m` where `a` is scalar and
`m` is nonzero and nilpotent. -/
theorem isParabolic_iff_exists [NeZero (2 : K)] : m.IsParabolic ↔ ∃ a n, m = scalar _ a + n ∧ n ≠ 0 ∧ n ^ 2 = 0 :=
by
constructor
·
exact fun hm ↦
⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩, hm.sub_eigenvalue_sq_eq_zero⟩
· rintro ⟨a, n, hm, hn0, hnsq⟩
constructor
· refine fun ⟨b, hb⟩ ↦ hn0 ?_
rw [← sub_eq_iff_eq_add'] at hm
simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj, sq_eq_zero_iff] using hnsq
· suffices scalar (Fin 2) (m.disc / 4) = 0
by
rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
tauto
rw [← sub_scalar_sq_eq_disc, hm, trace_add, scalar_apply, trace_diagonal]
simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)), (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero,
hnsq]
