1. Physlib
  2. Mathematics
  3. CrossProductMatrix
Imports
/- Copyright (c) 2026 Giuseppe Sorge. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Giuseppe Sorge -/ module public import Mathlib.Data.Matrix.Mul public import Mathlib.Data.Real.Basic public import Mathlib.LinearAlgebra.CrossProduct public import Mathlib.LinearAlgebra.Matrix.Notation

The hat map on three-dimensional vectors

The hat map sends a vector ω : Fin 3 → ℝ to the skew-symmetric matrix [ω]ₓ characterised by [ω]ₓ *ᵥ v = ω ⨯₃ v. It realises the correspondence between ℝ³ and the skew-symmetric 3 × 3 matrices (the Lie algebra 𝖘𝖔(3)), and underlies the angular velocity of a rigid body.

@[expose] public section

The hat map [ω]ₓ: the skew-symmetric 3 × 3 matrix acting as the cross product with ω, i.e. [ω]ₓ *ᵥ v = ω ⨯₃ v.

def crossProductMatrix (ω : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ := !![0, -ω 2, ω 1; ω 2, 0, -ω 0; -ω 1, ω 0, 0]

The hat matrix acts on a vector as the cross product.

@[simp] lemma crossProductMatrix_mulVec (ω v : Fin 3 → ℝ) : crossProductMatrix ω *ᵥ v = ω ⨯₃ v := ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ crossProductMatrix ω *ᵥ v = (crossProduct ω) v ω:Fin 3 → ℝv:Fin 3 → ℝi:Fin 3⊢ (crossProductMatrix ω *ᵥ v) i = (crossProduct ω) v i ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨0, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨1, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨2, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨2, ⋯⟩) ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨0, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨1, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ (crossProductMatrix ω *ᵥ v) ((fun i => i) ⟨2, ⋯⟩) = (crossProduct ω) v ((fun i => i) ⟨2, ⋯⟩) ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ -(ω 1 * v 0) + ω 0 * v 1 = ω 0 * v 1 - ω 1 * v 0 ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ -(ω 2 * v 1) + ω 1 * v 2 = ω 1 * v 2 - ω 2 * v 1ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ ω 2 * v 0 + -(ω 0 * v 2) = ω 2 * v 0 - ω 0 * v 2ω:Fin 3 → ℝv:Fin 3 → ℝ⊢ -(ω 1 * v 0) + ω 0 * v 1 = ω 0 * v 1 - ω 1 * v 0 All goals completed! 🐙

The hat map produces skew-symmetric matrices.

@[simp] lemma crossProductMatrix_transpose (ω : Fin 3 → ℝ) : (crossProductMatrix ω)ᵀ = - crossProductMatrix ω := ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ = -crossProductMatrix ω ω:Fin 3 → ℝi:Fin 3j:Fin 3⊢ (crossProductMatrix ω)ᵀ i j = (-crossProductMatrix ω) i j ω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨0, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨0, ⋯⟩) jω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨1, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨1, ⋯⟩) jω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) j ω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨0, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨0, ⋯⟩) jω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨1, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨1, ⋯⟩) jω:Fin 3 → ℝj:Fin 3⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) j = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) j ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω)ᵀ ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = (-crossProductMatrix ω) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙

The vee map: reads the vector off a 3 × 3 matrix. It is a left inverse of the hat map.

def crossProductVee (A : Matrix (Fin 3) (Fin 3) ℝ) : Fin 3 → ℝ := ![A 2 1, A 0 2, A 1 0]

The vee map is a left inverse of the hat map.

@[simp] lemma crossProductVee_crossProductMatrix (ω : Fin 3 → ℝ) : crossProductVee (crossProductMatrix ω) = ω := ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee = ω ω:Fin 3 → ℝi:Fin 3⊢ (crossProductMatrix ω).crossProductVee i = ω i ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = ω ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = ω ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = ω ((fun i => i) ⟨2, ⋯⟩) ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨0, ⋯⟩) = ω ((fun i => i) ⟨0, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨1, ⋯⟩) = ω ((fun i => i) ⟨1, ⋯⟩)ω:Fin 3 → ℝ⊢ (crossProductMatrix ω).crossProductVee ((fun i => i) ⟨2, ⋯⟩) = ω ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙

On skew-symmetric matrices the hat map is also a right inverse of the vee map: if Aᵀ = -A then [Aᵛ]ₓ = A. Together with crossProductVee_crossProductMatrix this identifies ℝ³ with the skew-symmetric 3 × 3 matrices 𝖘𝖔(3).

A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j i⊢ crossProductMatrix A.crossProductVee = A A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee = A A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0i:Fin 3j:Fin 3⊢ crossProductMatrix A.crossProductVee i j = A i j A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨0, ⋯⟩) j = A ((fun i => i) ⟨0, ⋯⟩) jA:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨1, ⋯⟩) j = A ((fun i => i) ⟨1, ⋯⟩) jA:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) j = A ((fun i => i) ⟨2, ⋯⟩) j A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨0, ⋯⟩) j = A ((fun i => i) ⟨0, ⋯⟩) jA:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨1, ⋯⟩) j = A ((fun i => i) ⟨1, ⋯⟩) jA:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0j:Fin 3⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) j = A ((fun i => i) ⟨2, ⋯⟩) j A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = A ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = A ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ crossProductMatrix A.crossProductVee ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = A ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ 0 = A 2 2 A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ 0 = A 0 0A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ -A 1 0 = A 0 1A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ 0 = A 1 1A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ -A 2 1 = A 1 2A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ -A 0 2 = A 2 0A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ 0 = A 2 2 first | A:Matrix (Fin 3) (Fin 3) ℝhA:Aᵀ = -Ah:∀ (i j : Fin 3), A i j = -A j ihdiag:∀ (i : Fin 3), A i i = 0⊢ 0 = A 2 2 | All goals completed! 🐙