Identities for 2 × 2 matrices

This file collects polynomial identities satisfied by 2 × 2 matrices over a commutative ring, all consequences of the Cayley–Hamilton theorem in dimension two.

Main results

• Matrix.mul_self_eq_trace_smul_sub_det_smul_fin_two: Cayley–Hamilton, A * A = trace A • A - det A • 1.
• Matrix.adjugate_fin_two_eq_trace_smul_one_sub: adjugate A = trace A • 1 - A.
• Matrix.adjugate_add_fin_two: the adjugate is additive.
• Matrix.mul_add_mul_eq_trace_smul_add_trace_smul_fin_two: the polarized Cayley–Hamilton identity A * B + B * A = trace A • B + trace B • A + (trace (A * B) - trace A * trace B) • 1.
• Matrix.mul_mul_eq_trace_smul_sub_det_smul_adjugate_fin_two: M * A * M = trace (A * M) • M - det M • adjugate A.
• Matrix.det_add_fin_two: det (A + B) = det A + trace (adjugate A * B) + det B.
• Matrix.det_add_smul_fin_two: the determinant of a pencil A + c • B.
• Matrix.lie_lie_lie_eq_discr_smul_lie_fin_two: ⁅X, ⁅X, ⁅X, T⁆⁆⁆ = discr X • ⁅X, T⁆.
• Matrix.det_lie_lie_eq_neg_discr_mul_det_lie_fin_two: det ⁅X, ⁅X, T⁆⁆ = -discr X * det ⁅X, T⁆.

Related

In Mathlib, Cayley–Hamilton is Matrix.aeval_self_charpoly and the 2 × 2 characteristic polynomial is Matrix.charpoly_fin_two (which assumes Nontrivial R); the entries of the 2 × 2 adjugate are Matrix.adjugate_fin_two and the discriminant is Matrix.discr_fin_two. The statements above are their coordinate-free consequences, with no Nontrivial hypothesis.

theorem Matrix.mul_self_eq_trace_smul_sub_det_smul_fin_two {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) : A * A = A.trace • A - A.det • 1

Cayley–Hamilton for 2 × 2 matrices: A * A = trace A • A - det A • 1.

theorem Matrix.adjugate_fin_two_eq_trace_smul_one_sub {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) : A.adjugate = A.trace • 1 - A

The adjugate of a 2 × 2 matrix is trace A • 1 - A.

theorem Matrix.adjugate_add_fin_two {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : (A + B).adjugate = A.adjugate + B.adjugate

The adjugate of 2 × 2 matrices is additive.

theorem Matrix.mul_add_mul_eq_trace_smul_add_trace_smul_fin_two {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : A * B + B * A = A.trace • B + B.trace • A + ((A * B).trace - A.trace * B.trace) • 1

Polarized Cayley–Hamilton identity for 2 × 2 matrices.

theorem Matrix.mul_mul_eq_trace_smul_sub_det_smul_adjugate_fin_two {R : Type u_1} [CommRing R] (M A : Matrix (Fin 2) (Fin 2) R) : M * A * M = (A * M).trace • M - M.det • A.adjugate

For 2 × 2 matrices, M * A * M = trace (A * M) • M - det M • adjugate A.

theorem Matrix.det_add_fin_two {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) : (A + B).det = A.det + (A.adjugate * B).trace + B.det

The determinant of a sum of 2 × 2 matrices.

theorem Matrix.det_add_smul_fin_two {R : Type u_1} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) (c : R) : (A + c • B).det = A.det + c * (A.trace * B.trace - (A * B).trace) + c ^ 2 * B.det

The determinant of a pencil of 2 × 2 matrices.

theorem Matrix.lie_lie_lie_eq_discr_smul_lie_fin_two {R : Type u_1} [CommRing R] (X T : Matrix (Fin 2) (Fin 2) R) : ⁅X, ⁅X, ⁅X, T⁆⁆⁆ = X.discr • ⁅X, T⁆

For 2 × 2 matrices, ad X ^ 3 = discr X • ad X.

theorem Matrix.det_lie_lie_eq_neg_discr_mul_det_lie_fin_two {R : Type u_1} [CommRing R] (X T : Matrix (Fin 2) (Fin 2) R) : ⁅X, ⁅X, T⁆⁆.det = -X.discr * ⁅X, T⁆.det

For 2 × 2 matrices, det ⁅X, ⁅X, T⁆⁆ = -discr X * det ⁅X, T⁆.