Lean, informalized

Nielsen & Chuang · Chapter 8, Quantum noise and quantum operations · p. 375

Exercise 8.12 - A real three by three matrix written as orthogonal times symmetric, with the orthogonal factor made a rotation

Trading an orthogonal factor for a rotation.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A real 3×33 \times 3 matrix MM is written as a product M=OSM = OS of an orthogonal matrix OO and a symmetric matrix SS. Nothing in that forces OO to be a rotation. The exercise asks to show that MM also has a factorization of the same kind whose orthogonal factor is a rotation.

Orthogonal and Symmetric Matrices

An orthogonal matrix OO is a real 3×33 \times 3 matrix whose transpose is its inverse, O𝖳O=OO𝖳=I.O^{\mathsf T} O = O O^{\mathsf T} = I .(1) The orthogonal matrices form the group O(3)O(3).

A rotation is an orthogonal matrix of determinant +1+1, and the rotations form the special orthogonal group SO(3)SO(3). A symmetric matrix SS is a real 3×33 \times 3 matrix equal to its transpose, S𝖳=SS^{\mathsf T} = S.

The Claim

Theorem 1. Let MM, OO and SS be real 3×33 \times 3 matrices, with OO orthogonal, SS symmetric and M=OSM = OS. Then there are real 3×33 \times 3 matrices O′O' and S′S' with M=O′S′,O′∈SO(3),S′𝖳=S′.M = O' S', \qquad O' \in SO(3), \qquad S'^{\mathsf T} = S' .(2)✦

What Is Checked

The claim is stated over real 3×33 \times 3 matrices, with the orthogonal group O(3)O(3) of (1), its subgroup SO(3)SO(3) of rotations, and symmetry as equality with the transpose.