The commutant of a 2 × 2 matrix

A 2 × 2 matrix over a field is regular as soon as it is not scalar: it is then cyclic (nonderogatory), and the matrices commuting with it are exactly the polynomials in it. In size 2 those polynomials are the affine combinations a • 1 + b • M, so the commutant of a non-scalar M : Matrix (Fin 2) (Fin 2) F is the two-dimensional algebra F[M] — in particular it is commutative.

Mathlib's Matrix.mem_range_scalar_iff_commute_transvectionStruct describes the matrices commuting with everything; what is proved here is the commutant of a single matrix, in size two, read off the three independent entry equations of M * N = N * M by splitting on which of the two off-diagonal entries or the diagonal difference is nonzero.

Being scalar is recorded over a semiring; only the commutant computation itself, which divides by a matrix entry, needs a field.

Main results

• TauCeti.mem_range_scalar_fin_two_iff: a 2 × 2 matrix is scalar exactly when its off-diagonal entries vanish and its two diagonal entries agree.
• TauCeti.commute_fin_two_iff: a matrix commutes with a non-scalar 2 × 2 matrix M exactly when it is of the form a • 1 + b • M.
• TauCeti.commute_of_commute_fin_two: two matrices commuting with a common non-scalar 2 × 2 matrix commute with each other.

References

The commutant is used to compute centralizers in GL₂ in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Centralizer, for the character theory roadmap, Layer 9, "The conjugacy classes (a build target)".

theorem TauCeti.mem_range_scalar_fin_two_iff {F : Type u_1} {M : Matrix (Fin 2) (Fin 2) F} [Semiring F] : M ∈ Set.range ⇑(Matrix.scalar (Fin 2)) ↔ M 0 1 = 0 ∧ M 1 0 = 0 ∧ M 0 0 = M 1 1

A 2 × 2 matrix is scalar exactly when its off-diagonal entries vanish and its two diagonal entries agree.

theorem TauCeti.commute_fin_two_iff {F : Type u_1} {M N : Matrix (Fin 2) (Fin 2) F} [Field F] (hM : M ∉ Set.range ⇑(Matrix.scalar (Fin 2))) : Commute M N ↔ ∃ (a : F) (b : F), N = (Matrix.scalar (Fin 2)) a + b • M

The commutant of a non-scalar 2 × 2 matrix. A matrix commutes with a non-scalar M : Matrix (Fin 2) (Fin 2) F exactly when it lies in the two-dimensional subalgebra spanned by 1 and M; equivalently, a non-scalar 2 × 2 matrix is cyclic, so its commutant is F[M].

The hypothesis is necessary: everything commutes with a scalar matrix.

theorem TauCeti.commute_of_commute_fin_two {F : Type u_1} {M N P : Matrix (Fin 2) (Fin 2) F} [Field F] (hM : M ∉ Set.range ⇑(Matrix.scalar (Fin 2))) (hN : Commute M N) (hP : Commute M P) : Commute N P

Two matrices commuting with a common non-scalar 2 × 2 matrix commute with each other: both lie in the commutative algebra F[M].