The type-B matrix model of an odd polarization

An odd polarization whose orthogonal remainder contains a vector of quadratic norm one identifies the quadratic space with the standard split odd space. This file compares the resulting basis with Mathlib's matrix model of the type-B Lie algebra and then with the quadratic elements of the Clifford algebra.

The normalization is fixed by LieAlgebra.Orthogonal.JB: the distinguished remainder vector has quadratic norm 1 and polar self-pairing 2, while the two isotropic families pair by the identity matrix. The coordinate equivalence absorbs its arbitrary square-one internal coordinate.

Main definitions

• TauCeti.SpinPolarizationData.typeBBasis: the odd hyperbolic basis, with the remainder first.
• TauCeti.SpinPolarizationData.typeBQuadraticEquiv: the standard type-B matrix algebra identified with the quadratic Clifford Lie algebra.

Main results

• TauCeti.SpinPolarizationData.polarBilin_toMatrix_typeBBasis: the polar form has Gram matrix LieAlgebra.Orthogonal.JB in the odd hyperbolic basis.
• TauCeti.SpinPolarizationData.polar_basis_typeBBasis, TauCeti.SpinPolarizationData.polar_dualVector_typeBBasis and TauCeti.SpinPolarizationData.polar_line_typeBBasis: the rows of that Gram matrix, read as the polar coordinates of a single vector against the whole basis.
• TauCeti.SpinPolarizationData.typeBQuadraticEquiv_lie_ι: the comparison acts on Clifford generators through the matrix endomorphism in that basis.

Roadmap

This supplies the matrix-to-Clifford bridge needed by the full-weight type-B Chevalley carrier in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. The comparison is evaluated on the numbered root vectors in TauCeti/RepresentationTheory/Spin/Polarization/TypeB/RootGenerators.lean.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.

noncomputable def TauCeti.SpinPolarizationData.typeBBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) : Module.Basis (Unit ⊕ ι ⊕ ι) K V

The standard odd hyperbolic basis of a polarization: the quadratic-unit remainder vector, then a basis of the first isotropic summand, then its polar-dual basis.

Equations

• P.typeBBasis b z hz = ((Module.Basis.singleton Unit K).prod (b.prod (P.dualBasis b))).map (TauCeti.SpinPolarizationData.oddDecompositionEquiv✝ P z hz)

@[simp]

theorem TauCeti.SpinPolarizationData.typeBBasis_inl {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : Unit) : (P.typeBBasis b z hz) (Sum.inl i) = ↑z

@[simp]

theorem TauCeti.SpinPolarizationData.typeBBasis_inr_inl {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : ι) : (P.typeBBasis b z hz) (Sum.inr (Sum.inl i)) = ↑(b i)

@[simp]

theorem TauCeti.SpinPolarizationData.typeBBasis_inr_inr {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : ι) : (P.typeBBasis b z hz) (Sum.inr (Sum.inr i)) = ↑(P.dualVector b i)

theorem TauCeti.SpinPolarizationData.polarBilin_toMatrix_typeBBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) : (LinearMap.BilinForm.toMatrix (P.typeBBasis b z hz)) (QuadraticMap.polarBilin Q) = LieAlgebra.Orthogonal.JB ι K

In the odd hyperbolic basis, the polar form has the standard split type-B Gram matrix.

The polar coordinates of the three kinds of vector

These are the rows of polarBilin_toMatrix_typeBBasis in the form a Clifford computation wants them: the polar form of a fixed vector against the whole odd hyperbolic basis at once.

@[simp]

theorem TauCeti.SpinPolarizationData.polar_basis_typeBBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : ι) (c : Unit ⊕ ι ⊕ ι) : QuadraticMap.polar (⇑Q) (↑(b i)) ((P.typeBBasis b z hz) c) = if c = Sum.inr (Sum.inr i) then 1 else 0

A basis vector of the first isotropic summand pairs with the odd hyperbolic basis only against its own polar dual.

@[simp]

theorem TauCeti.SpinPolarizationData.polar_dualVector_typeBBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : ι) (c : Unit ⊕ ι ⊕ ι) : QuadraticMap.polar (⇑Q) (↑(P.dualVector b i)) ((P.typeBBasis b z hz) c) = if c = Sum.inr (Sum.inl i) then 1 else 0

A polar-dual vector pairs with the odd hyperbolic basis only against its own basis vector.

@[simp]

theorem TauCeti.SpinPolarizationData.polar_line_typeBBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (c : Unit ⊕ ι ⊕ ι) : QuadraticMap.polar (⇑Q) (↑z) ((P.typeBBasis b z hz) c) = if c = Sum.inl () then 2 else 0

The remainder vector pairs with the odd hyperbolic basis only against itself, and there by 2. That coefficient is the middle entry of LieAlgebra.Orthogonal.JB, and it is what the integral short-root matrix carries.

noncomputable def TauCeti.SpinPolarizationData.typeBQuadraticEquiv {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] : ↥(LieAlgebra.Orthogonal.typeB ι K) ≃ₗ⁅K⁆ ↥(CliffordAlgebra.quadraticLieSubalgebra Q)

An odd polarization with a quadratic-unit remainder identifies the split type-B matrix algebra with the quadratic elements of the Clifford algebra.

Equations

• P.typeBQuadraticEquiv b z hz = CliffordAlgebra.skewAdjointMatricesEquivQuadratic Q ⋯ (P.typeBBasis b z hz) ⋯

@[simp]

theorem TauCeti.SpinPolarizationData.typeBQuadraticEquiv_lie_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] (A : ↥(LieAlgebra.Orthogonal.typeB ι K)) (x : V) : ⁅↑((P.typeBQuadraticEquiv b z hz) A), (CliffordAlgebra.ι Q) x⁆ = (CliffordAlgebra.ι Q) (((Matrix.toLinAlgEquiv (P.typeBBasis b z hz)) ↑A) x)

The type-B comparison acts on Clifford generators through the corresponding matrix endomorphism in the odd hyperbolic basis.