The orthogonal Lie algebra of the standard quadratic form

Mathlib's standard quadratic form on n → R is QuadraticMap.weightedSumSquares R (1 : n → R). When 2 is invertible, its polar bilinear form is twice the identity-matrix form. Scaling a bilinear form by an invertible scalar does not change its skew-adjoint endomorphisms, so Mathlib's endomorphism-to-matrix equivalence identifies those endomorphisms with LieAlgebra.Orthogonal.so n R.

This supplies the coordinate bridge used in the standard-form statement that exterior bivectors are the orthogonal Lie algebra. It does not choose a basis for an abstract quadratic module.

Main results

• TauCeti.weightedSumSquares_eq_toQuadraticForm_diagonal: a weighted sum of squares is the quadratic form of the diagonal weight matrix.
• TauCeti.QuadraticForm.polarBilin_weightedSumSquares: the polar form of a weighted sum of squares is twice its diagonal-matrix form.
• TauCeti.QuadraticForm.standardSkewAdjointLieEquiv: the Lie equivalence from the skew-adjoint endomorphisms of its polar form to Mathlib's matrix orthogonal Lie algebra.

References

• Tau Ceti Roadmap, Representation Theory / Spin Representations, Layer 3, "Bivectors as a Lie subalgebra".

theorem TauCeti.weightedSumSquares_eq_toQuadraticForm_diagonal (R : Type u) [CommRing R] (n : Type u_1) [Fintype n] [DecidableEq n] (w : n → R) : QuadraticMap.weightedSumSquares R w = (Matrix.diagonal w).toQuadraticForm'

A weighted sum-of-squares quadratic form is the quadratic form associated to the diagonal matrix of its weights.

theorem TauCeti.QuadraticForm.polarBilin_weightedSumSquares (R : Type u) (n : Type u_1) [CommRing R] [Fintype n] [DecidableEq n] (w : n → R) : (QuadraticMap.weightedSumSquares R w).polarBilin = 2 • (Matrix.toLinearMap₂' R) (Matrix.diagonal w)

The polar bilinear form of a weighted sum of squares is twice its diagonal-matrix form.

@[simp]

theorem TauCeti.QuadraticForm.polarBilin_weightedSumSquares_one (R : Type u) (n : Type u_1) [CommRing R] [Fintype n] [DecidableEq n] : (QuadraticMap.weightedSumSquares R 1).polarBilin = 2 • (Matrix.toLinearMap₂' R) 1

The polar bilinear form of the standard quadratic form is twice the identity-matrix form.

noncomputable def TauCeti.QuadraticForm.standardSkewAdjointLieEquiv (R : Type u) (n : Type u_1) [CommRing R] [Fintype n] [DecidableEq n] [Invertible 2] : ↥(skewAdjointLieSubalgebra (QuadraticMap.weightedSumSquares R 1).polarBilin) ≃ₗ⁅R⁆ ↥(LieAlgebra.Orthogonal.so n R)

The skew-adjoint endomorphisms of the polar form of the standard quadratic form are Mathlib's matrix orthogonal Lie algebra.

@[simp]

theorem TauCeti.QuadraticForm.coe_standardSkewAdjointLieEquiv_apply (R : Type u) (n : Type u_1) [CommRing R] [Fintype n] [DecidableEq n] [Invertible 2] (f : ↥(skewAdjointLieSubalgebra (QuadraticMap.weightedSumSquares R 1).polarBilin)) : ↑((standardSkewAdjointLieEquiv R n) f) = lieEquivMatrix' ↑f

The standard skew-adjoint equivalence sends an endomorphism to its matrix.

@[simp]

theorem TauCeti.QuadraticForm.coe_standardSkewAdjointLieEquiv_symm_apply (R : Type u) (n : Type u_1) [CommRing R] [Fintype n] [DecidableEq n] [Invertible 2] (A : ↥(LieAlgebra.Orthogonal.so n R)) : ↑((standardSkewAdjointLieEquiv R n).symm A) = lieEquivMatrix'.symm ↑A

The inverse standard skew-adjoint equivalence sends a matrix to its endomorphism.