Exterior bivectors and the standard orthogonal Lie algebra

For the standard sum-of-squares quadratic form on Fin n → R, the second exterior power is canonically the matrix orthogonal Lie algebra. The forward map sends u ∧ v to the skew matrix with entries 2 * (u i * v j - v i * u j); the factor of two matches the polar form of the sum-of-squares quadratic form.

The inverse reads ⅟ 2 times the upper-triangular entries of a skew matrix in the standard exterior basis. Lie compatibility is proved through the faithful Clifford generators and the established commutator action of Clifford bivectors, rather than by expanding a matrix commutator.

Main results

• CliffordAlgebra.bivectorEquivSo: the standard exterior-bivector Lie equivalence.
• CliffordAlgebra.bivectorEquivSo_apply_ιMulti: its value on a decomposable bivector.
• CliffordAlgebra.bivectorEquivSo_symm_repr_apply: the coefficients of its inverse.
• CliffordAlgebra.bivectorEquivSo_apply_ιMulti_mulVec: its normalized action on a vector.

References

This implements the Layer 3 "Bivectors are 𝔰𝔬(V)" target in TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md.

noncomputable def CliffordAlgebra.bivectorEquivSo (n : ℕ) (R : Type u) [CommRing R] [Invertible 2] : have Q := QuadraticMap.weightedSumSquares R 1; ↥(⋀[R]^2 (Fin n → R)) ≃ₗ⁅R⁆ ↥(LieAlgebra.Orthogonal.so (Fin n) R)

The second exterior power of the standard quadratic module is the matrix orthogonal Lie algebra. The Lie structure on the exterior power is the one transported from quadratic Clifford elements for the standard sum-of-squares form.

Equations

• CliffordAlgebra.bivectorEquivSo n R = (CliffordAlgebra.bivectorLieEquiv (QuadraticMap.weightedSumSquares R 1)).trans (CliffordAlgebra.standardQuadraticToSoLieEquiv✝ n R)

@[simp]

theorem CliffordAlgebra.bivectorEquivSo_apply_ιMulti (n : ℕ) (R : Type u) [CommRing R] [Invertible 2] (u v : Fin n → R) : have Q := QuadraticMap.weightedSumSquares R 1; ↑((bivectorEquivSo n R) ((exteriorPower.ιMulti R 2) ![u, v])) = fun (i j : Fin n) => 2 * (u i * v j - v i * u j)

On a decomposable bivector, bivectorEquivSo is the normalized skew matrix 2 * (u vᵀ - v uᵀ).

@[simp]

theorem CliffordAlgebra.bivectorEquivSo_symm_repr_apply (n : ℕ) (R : Type u) [CommRing R] [Invertible 2] (A : ↥(LieAlgebra.Orthogonal.so (Fin n) R)) (s : ↑(Set.powersetCard (Fin n) 2)) : have Q := QuadraticMap.weightedSumSquares R 1; ((Module.Basis.exteriorPower 2 (Pi.basisFun R (Fin n))).repr ((LieEquiv.symm (bivectorEquivSo n R)) A)) s = have e := Set.powersetCard.ofFinEmbEquiv.symm s; ⅟2 * ↑A (e 0) (e 1)

The inverse of bivectorEquivSo reads ⅟ 2 times an upper-triangular matrix entry as the corresponding coefficient in the standard exterior basis.

theorem CliffordAlgebra.bivectorEquivSo_apply_ιMulti_mulVec (n : ℕ) (R : Type u) [CommRing R] [Invertible 2] (u v x : Fin n → R) : have Q := QuadraticMap.weightedSumSquares R 1; (↑((bivectorEquivSo n R) ((exteriorPower.ιMulti R 2) ![u, v]))).mulVec x = (2 * ∑ i : Fin n, v i * x i) • u - (2 * ∑ i : Fin n, u i * x i) • v

The standard exterior bivector u ∧ v acts on a vector by the polar-form-normalized infinitesimal rotation.