The real orthogonal Lie algebra as a skew-adjoint part

Mathlib carries two unrelated descriptions of the skew-symmetric real matrices: the orthogonal Lie algebra LieAlgebra.Orthogonal.so n ℝ, cut out by the skew-adjointness condition Aᵀ = -A for the identity bilinear form, and skewAdjoint (Matrix n n ℝ), the skew-adjoint part of the star ring Matrix n n ℝ. This file identifies them: over ℝ the star of a matrix is its conjugate transpose, which is its transpose.

The bridge is purely algebraic, with no exponential or topological content, so it is stated here and consumed by the exponential and Lie-subgroup files that compare so with star-algebra statements about the unitary — that is, orthogonal — group of Matrix n n ℝ.

Main results

• Matrix.mem_so_iff_mem_skewAdjoint identifies the real orthogonal Lie algebra with the skew-adjoint matrices.

theorem Matrix.mem_so_iff_mem_skewAdjoint {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) : A ∈ LieAlgebra.Orthogonal.so n ℝ ↔ A ∈ skewAdjoint (Matrix n n ℝ)

Over ℝ the orthogonal Lie algebra is the skew-adjoint part of the matrix algebra: the star of a real matrix is its conjugate transpose, which is its transpose.