The quadratic realization of a skew-adjoint Lie algebra

For a nondegenerate quadratic form on a finite-dimensional vector space, the skew-adjoint endomorphisms of its polar form are exactly the quadratic elements of its Clifford algebra. The equivalence factors through the second exterior power, so its normalization is inherited from the canonical bivector action rather than from a basis-dependent inverse.

Main results

• CliffordAlgebra.soEquivQuadratic: the quadratic realization Lie equivalence.
• CliffordAlgebra.soEquivQuadratic_lie_ι: its defining generator-action equation.
• CliffordAlgebra.skewAdjointMatricesEquivQuadratic: the same realization transported through a basis whose Gram matrix is specified.
• CliffordAlgebra.quadraticLieSubalgebra_ext: quadratic elements are determined by their commutator action on Clifford generators.
• CliffordAlgebra.quadraticLieSubalgebra_eq_bivector_of_lie_ι: the resulting recognition criterion, identifying a quadratic element with the Clifford bivector of two vectors from its commutator action on a basis.

noncomputable def CliffordAlgebra.soEquivQuadratic {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q)) ≃ₗ⁅K⁆ ↥(quadraticLieSubalgebra Q)

The skew-adjoint endomorphisms of a nondegenerate finite-dimensional quadratic module are the quadratic elements of its Clifford algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.soEquivQuadratic_lie_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (f : ↥(skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q))) (x : V) : ⁅↑((soEquivQuadratic Q hQ) f), (ι Q) x⁆ = (ι Q) (↑f x)

The quadratic element realizing a skew-adjoint endomorphism acts by that endomorphism on the Clifford generators.

noncomputable def CliffordAlgebra.skewAdjointMatricesEquivQuadratic {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] {n : Type w} [Fintype n] [DecidableEq n] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (b : Module.Basis n K V) {J : Matrix n n K} (hJ : (LinearMap.BilinForm.toMatrix b) (QuadraticMap.polarBilin Q) = J) : ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅K⁆ ↥(quadraticLieSubalgebra Q)

A basis transports the matrices skew-adjoint for the Gram matrix of a nondegenerate quadratic form to the quadratic elements of its Clifford algebra.

Equations

• CliffordAlgebra.skewAdjointMatricesEquivQuadratic Q hQ b hJ = (TauCeti.skewAdjointLieEquivOfBasis b (QuadraticMap.polarBilin Q) hJ).trans (CliffordAlgebra.soEquivQuadratic Q hQ)

@[simp]

theorem CliffordAlgebra.skewAdjointMatricesEquivQuadratic_lie_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] {n : Type w} [Fintype n] [DecidableEq n] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (b : Module.Basis n K V) {J : Matrix n n K} (hJ : (LinearMap.BilinForm.toMatrix b) (QuadraticMap.polarBilin Q) = J) (A : ↥(skewAdjointMatricesLieSubalgebra J)) (x : V) : ⁅↑((skewAdjointMatricesEquivQuadratic Q hQ b hJ) A), (ι Q) x⁆ = (ι Q) (((Matrix.toLinAlgEquiv b) ↑A) x)

The matrix-to-quadratic equivalence acts on Clifford generators through the matrix endomorphism in the chosen basis.

theorem CliffordAlgebra.quadraticLieSubalgebra_ext {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {a b : ↥(quadraticLieSubalgebra Q)} (h : ∀ (x : V), ⁅↑a, (ι Q) x⁆ = ⁅↑b, (ι Q) x⁆) : a = b

Two quadratic Clifford elements are equal when their commutator actions agree on every generator.

theorem CliffordAlgebra.quadraticLieSubalgebra_ext_iff {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] {Q : QuadraticForm K V} {hQ : QuadraticMap.Nondegenerate} {a b : ↥(quadraticLieSubalgebra Q)} : a = b ↔ ∀ (x : V), ⁅↑a, (ι Q) x⁆ = ⁅↑b, (ι Q) x⁆

theorem CliffordAlgebra.quadraticLieSubalgebra_eq_bivector_of_lie_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (a : ↥(quadraticLieSubalgebra Q)) (f : Module.End K V) (hf : ∀ (v : V), ⁅↑a, (ι Q) v⁆ = (ι Q) (f v)) {n : Type w} (bas : Module.Basis n K V) (x y : V) (h : ∀ (c : n), f (bas c) = QuadraticMap.polar (⇑Q) y (bas c) • x - QuadraticMap.polar (⇑Q) x (bas c) • y) : a = ⟨bivector Q x y, ⋯⟩

Recognizing a quadratic Clifford element as the bivector of two vectors. A quadratic element whose commutator action on the Clifford generators is an endomorphism f is the bivector of x and y as soon as f is the infinitesimal rotation v ↦ polar Q y v • x - polar Q x v • y on some basis.

This is the shared shell of every root-vector and Cartan-generator identification in a matrix model of an orthogonal Lie algebra: f is the matrix endomorphism supplied by CliffordAlgebra.skewAdjointMatricesEquivQuadratic_lie_ι, and only the matrix computation differs between the identifications.