The rotation matrix of the plane

The real 2 × 2 matrix Matrix.rotation θ = !![cos θ, -sin θ; sin θ, cos θ] of the counterclockwise rotation of ℝ² by the angle θ.

Mathlib has the conformal matrix Matrix.planeConformalMatrix a b = !![a, -b; b, a] in GL₂, which Complex.toMatrix_rotation identifies with multiplication by a unit complex number, but no rotation matrix parametrised by the angle (the GeneralLinearGroup file lists one as a TODO); Matrix.rotation θ is its case a = cos θ, b = sin θ. The angle parametrisation is needed whenever a physical model mixes two real fields by an angle: the neutral electroweak gauge fields (W³, B) are rotated into (Z, A) by the weak mixing angle, and the mass matrix is diagonalised by conjugating with this rotation. The results here are the facts such a diagonalisation uses: the action on vectors, the transpose as the inverse, the group law, and membership in the special orthogonal group.

Main results

• Matrix.rotation_eq_planeConformalMatrix: the rotation is Mathlib's planeConformalMatrix (cos θ) (sin θ).
• Matrix.rotation_mulVec: the rotation applied to a vector w, componentwise.
• Matrix.rotation_zero, Matrix.rotation_mul_rotation: the rotation by 0 is the identity, and composing rotations adds their angles.
• Matrix.rotation_transpose: the transpose of the rotation by θ is the rotation by -θ.
• Matrix.det_rotation: the rotation has determinant 1.
• Matrix.rotation_mem_specialOrthogonalGroup: the rotation is orthogonal with determinant 1.

noncomputable def EpsilonEridani.Matrix.rotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The rotation of the plane by the angle θ, !![cos θ, -sin θ; sin θ, cos θ].

Equations

• EpsilonEridani.Matrix.rotation θ = !![Real.cos θ, -Real.sin θ; Real.sin θ, Real.cos θ]

theorem EpsilonEridani.Matrix.rotation_def (θ : ℝ) : rotation θ = !![Real.cos θ, -Real.sin θ; Real.sin θ, Real.cos θ]

The rotation matrix, entry by entry.

theorem EpsilonEridani.Matrix.rotation_eq_planeConformalMatrix (θ : ℝ) : rotation θ = ↑(Matrix.planeConformalMatrix (Real.cos θ) (Real.sin θ) ⋯)

The rotation by θ is the underlying matrix of Mathlib's conformal matrix planeConformalMatrix (cos θ) (sin θ), an element of GL₂(ℝ).

@[simp]

theorem EpsilonEridani.Matrix.rotation_mulVec (θ : ℝ) (w : Fin 2 → ℝ) : (rotation θ).mulVec w = ![Real.cos θ * w 0 - Real.sin θ * w 1, Real.sin θ * w 0 + Real.cos θ * w 1]

The rotation by θ applied to a vector w = (w₀, w₁).

@[simp]

theorem EpsilonEridani.Matrix.rotation_zero : rotation 0 = 1

The rotation by 0 is the identity.

@[simp]

theorem EpsilonEridani.Matrix.rotation_mul_rotation (θ φ : ℝ) : rotation θ * rotation φ = rotation (θ + φ)

Composing the rotations by θ and φ gives the rotation by θ + φ.

@[simp]

theorem EpsilonEridani.Matrix.rotation_transpose (θ : ℝ) : (rotation θ).transpose = rotation (-θ)

The transpose of the rotation by θ is the rotation by -θ, its inverse.

@[simp]

theorem EpsilonEridani.Matrix.det_rotation (θ : ℝ) : (rotation θ).det = 1

The rotation matrix has determinant 1.

theorem EpsilonEridani.Matrix.rotation_mem_specialOrthogonalGroup (θ : ℝ) : rotation θ ∈ Matrix.specialOrthogonalGroup (Fin 2) ℝ

The rotation matrix is orthogonal and has determinant 1.