Rational canonical form in size two

A 2 × 2 matrix over a field is scalar or cyclic: as soon as it is not scalar some vector v is not an eigenvector, and v, M *ᵥ v is then a basis in which M becomes the companion matrix !![0, -det M; 1, trace M] of its characteristic polynomial X² - (trace M) X + det M. That is the rational canonical form in size two, proved here at the level of matrices; the conjugacy classification of GL₂(F) it yields is in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.ConjugacyClasses.

Being scalar is spelled M ∈ Set.range (Matrix.scalar (Fin 2)), as in TauCeti.LinearAlgebra.Matrix.Commute, and unfolded by TauCeti.mem_range_scalar_fin_two_iff; that file's commutant computation is the companion result, describing the centralizer of a non-scalar matrix rather than its normal form.

Main definitions

• TauCeti.companionFinTwo: the companion matrix !![0, -d; 1, t] of X² - t X + d.

Main results

• TauCeti.exists_forall_mulVec_ne_smul: a non-scalar 2 × 2 matrix over a semiring has a vector that is not an eigenvector; over a field such a vector is cyclic.
• TauCeti.exists_det_ne_zero_mul_eq_mul_companionFinTwo: rational canonical form in size two, a non-scalar 2 × 2 matrix over a commutative ring is intertwined, by a matrix of nonzero determinant, with the companion matrix of its characteristic polynomial; over a field it is similar to it.

References

• C. Bonnafé, Representations of SL₂(𝔽_q) (2011), Chapter 1.

The companion matrix of a monic quadratic

def TauCeti.companionFinTwo {R : Type u_1} [CommRing R] (t d : R) : Matrix (Fin 2) (Fin 2) R

The companion matrix !![0, -d; 1, t] of the monic quadratic X² - t X + d: the matrix of multiplication by X on R[X] ⧸ (X² - t X + d) in the basis 1, X. Its trace is t and its determinant is d, so it is the normal form that the classification of 2 × 2 matrices runs on.

Equations

• TauCeti.companionFinTwo t d = !![0, -d; 1, t]

theorem TauCeti.companionFinTwo_def {R : Type u_1} [CommRing R] (t d : R) : companionFinTwo t d = !![0, -d; 1, t]

The companion matrix, spelled out entrywise.

@[simp]

theorem TauCeti.det_companionFinTwo {R : Type u_1} [CommRing R] (t d : R) : (companionFinTwo t d).det = d

@[simp]

theorem TauCeti.trace_companionFinTwo {R : Type u_1} [CommRing R] (t d : R) : (companionFinTwo t d).trace = t

theorem TauCeti.companionFinTwo_notMem_range_scalar {R : Type u_1} [CommRing R] (t d : R) [Nontrivial R] : companionFinTwo t d ∉ Set.range ⇑(Matrix.scalar (Fin 2))

A companion matrix is never scalar: its lower-left entry is 1.

Non-eigenvectors of a non-scalar matrix

theorem TauCeti.exists_forall_mulVec_ne_smul {R : Type u_1} [Semiring R] {M : Matrix (Fin 2) (Fin 2) R} (hM : M ∉ Set.range ⇑(Matrix.scalar (Fin 2))) : ∃ (v : Fin 2 → R), ∀ (c : R), M.mulVec v ≠ c • v

A non-scalar 2 × 2 matrix has a vector that is not an eigenvector. Over a field such a vector v is cyclic: v, M *ᵥ v is a basis.

Rational canonical form in size two

theorem TauCeti.exists_det_ne_zero_mul_eq_mul_companionFinTwo {R : Type u_1} [CommRing R] {M : Matrix (Fin 2) (Fin 2) R} (hM : M ∉ Set.range ⇑(Matrix.scalar (Fin 2))) : ∃ (P : Matrix (Fin 2) (Fin 2) R), P.det ≠ 0 ∧ M * P = P * companionFinTwo M.trace M.det

Rational canonical form in size two. A non-scalar 2 × 2 matrix M over a commutative ring is intertwined, by a matrix of nonzero determinant, with the companion matrix of its characteristic polynomial X² - (trace M) X + det M. Over a field the intertwiner is invertible, so M is similar to that companion matrix.

The statement is an intertwining identity of matrices rather than a conjugacy in GL₂: it holds over any commutative ring, where a nonzero determinant need not make the intertwiner invertible, and for an M that is not itself invertible. For an element of GL₂ over a field, the conjugacy form is TauCeti.isConj_companionGL.