The type-D matrix model of a polarization

An even polarization identifies a quadratic space with the split space on two copies of the isotropic basis. This file compares that basis with Mathlib's matrix model of the type-D Lie algebra and then with the quadratic elements of the Clifford algebra.

The standard diagonal matrix indexed by i acts by 1 on the i-th isotropic basis vector and by -1 on its dual. Under the comparison it is therefore the diagonal Clifford bivector used to compute the spin weights.

References

• Tau Ceti Roadmap, Spin Representations, Layer 5

noncomputable def TauCeti.SpinPolarizationData.typeDBasis {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) (hline : P.line = ⊥) : Module.Basis (ι ⊕ ι) K V

The hyperbolic basis of an even polarization: first b, then its polar-dual basis.

Equations

• P.typeDBasis b hline = (b.prod (P.dualBasis b)).map (TauCeti.SpinPolarizationData.evenDecompositionEquiv✝ P hline)

@[simp]

theorem TauCeti.SpinPolarizationData.typeDBasis_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) (hline : P.line = ⊥) (i : ι) : (P.typeDBasis b hline) (Sum.inl i) = ↑(b i)

@[simp]

theorem TauCeti.SpinPolarizationData.typeDBasis_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) (hline : P.line = ⊥) (i : ι) : (P.typeDBasis b hline) (Sum.inr i) = ↑(P.dualVector b i)

theorem TauCeti.SpinPolarizationData.polarBilin_toMatrix_typeDBasis {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) (hline : P.line = ⊥) : (LinearMap.BilinForm.toMatrix (P.typeDBasis b hline)) (QuadraticMap.polarBilin Q) = LieAlgebra.Orthogonal.JD ι K

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

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

An even polarization identifies the split type-D matrix algebra with the quadratic elements of the Clifford algebra.

Equations

• P.typeDQuadraticEquiv b hline = CliffordAlgebra.skewAdjointMatricesEquivQuadratic Q ⋯ (P.typeDBasis b hline) ⋯

@[simp]

theorem TauCeti.SpinPolarizationData.typeDQuadraticEquiv_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) [Invertible 2] (hline : P.line = ⊥) (A : ↥(LieAlgebra.Orthogonal.typeD ι K)) (x : V) : ⁅↑((P.typeDQuadraticEquiv b hline) A), (CliffordAlgebra.ι Q) x⁆ = (CliffordAlgebra.ι Q) (((Matrix.toLinAlgEquiv (P.typeDBasis b hline)) ↑A) x)

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

theorem TauCeti.SpinPolarizationData.typeDQuadraticEquiv_typeDDiagonalCartanBasis {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) [Invertible 2] (hline : P.line = ⊥) (i : ι) : (P.typeDQuadraticEquiv b hline) ↑(typeDDiagonalCartanBasis i) = ⟨P.diagonalBivector b i, ⋯⟩

The standard diagonal Cartan basis maps to the diagonal Clifford bivectors of the polarization.

@[simp]

theorem TauCeti.SpinPolarizationData.typeDQuadraticEquiv_symm_diagonalBivector {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) [Invertible 2] (hline : P.line = ⊥) (i : ι) : (P.typeDQuadraticEquiv b hline).symm ⟨P.diagonalBivector b i, ⋯⟩ = ↑(typeDDiagonalCartanBasis i)

The inverse comparison sends a diagonal Clifford bivector back to the standard diagonal generator.

theorem TauCeti.SpinPolarizationData.spinAction_typeDQuadraticEquiv_basis {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) (i : ι) (s : Finset ι) : ((spinAction Q P) ↑((P.typeDQuadraticEquiv b hline) ↑(typeDDiagonalCartanBasis i))) (b.ExteriorAlgebra s) = spinWeight K s i • b.ExteriorAlgebra s

Through the type-D comparison, the standard diagonal generator acts on the exterior basis with the corresponding spin weight.