The split polarization of a hyperbolic quadratic space

TauCeti.SpinPolarizationData.ofNondegenerate produces polarization data for any finite-dimensional nondegenerate quadratic space over a separably closed field, but it does so by normalizing an arbitrary form, so its two isotropic summands are not given by a formula. A construction that has to exhibit the carrier of the spin representation explicitly needs the split case written down instead.

This file writes it down. For a module M over a commutative ring K, Mathlib's QuadraticForm.dualProd K M is the hyperbolic form Q (f, m) = f m on Module.Dual K M × M, and its two coordinate summands Submodule.snd and Submodule.fst are isotropic and dually paired by construction:

polar Q (f, m) (g, x) = f x + g m.

TauCeti.SpinPolarizationData.hyperbolic packages them as a TauCeti.SpinPolarizationData, with the copy of M as the exterior summand W, the copy of its dual as the contraction summand W', and no orthogonal remainder, so the spinor module attached to it is the full exterior algebra of M. The only hypothesis is that the evaluation map Module.Dual.eval K M into the double dual is injective, that is, that the functionals on M separate its points. This ensures that the polar pairing has trivial left radical; by Module.eval_apply_injective it holds for every projective module, in particular over a field. The identification of W' with the dual of W needs no such hypothesis.

Nothing here constructs a Clifford action, a Lie algebra or a group: this file supplies the decomposition data those constructions take as input, and it asserts nothing about the quadratic space beyond the fields of the structure and the nondegeneracy they imply.

Main definitions

• TauCeti.SpinPolarizationData.hyperbolic: the polarization data of QuadraticForm.dualProd.
• TauCeti.SpinPolarizationData.hyperbolicBasis: the basis of the exterior summand transported from a basis of M.

Main results

• TauCeti.SpinPolarizationData.hyperbolic_W, hyperbolic_W' and hyperbolic_line: the summands of the constructed data.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II, for the exterior model attached to a split decomposition.
• N. Bourbaki, Algèbre, Chapter 9, §4, for hyperbolic quadratic spaces.

The polarization data

noncomputable def TauCeti.SpinPolarizationData.hyperbolic {K : Type u} [CommRing K] {M : Type v} [AddCommGroup M] [Module K M] (hM : Function.Injective ⇑(Module.Dual.eval K M)) : SpinPolarizationData (QuadraticForm.dualProd K M)

The split polarization of a hyperbolic quadratic space. For a module M over a commutative ring K whose functionals separate points, the hyperbolic form Q (f, m) = f m on Module.Dual K M × M is polarized by its two coordinate summands, with no orthogonal remainder.

The exterior summand W is the copy of M and the contraction summand W' is the copy of its dual, so the spinor module attached to this datum is the full exterior algebra of M.

Equations

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

@[simp]

theorem TauCeti.SpinPolarizationData.hyperbolic_W {K : Type u} [CommRing K] {M : Type v} [AddCommGroup M] [Module K M] (hM : Function.Injective ⇑(Module.Dual.eval K M)) : (hyperbolic hM).W = Submodule.snd K (Module.Dual K M) M

@[simp]

theorem TauCeti.SpinPolarizationData.hyperbolic_W' {K : Type u} [CommRing K] {M : Type v} [AddCommGroup M] [Module K M] (hM : Function.Injective ⇑(Module.Dual.eval K M)) : (hyperbolic hM).W' = Submodule.fst K (Module.Dual K M) M

@[simp]

theorem TauCeti.SpinPolarizationData.hyperbolic_line {K : Type u} [CommRing K] {M : Type v} [AddCommGroup M] [Module K M] (hM : Function.Injective ⇑(Module.Dual.eval K M)) : (hyperbolic hM).line = ⊥

The basis of the exterior summand

noncomputable def TauCeti.SpinPolarizationData.hyperbolicBasis {R : Type u} [CommSemiring R] {N : Type v} [AddCommMonoid N] [Module R N] {ι : Type w} (b : Module.Basis ι R N) : Module.Basis ι R ↥(Submodule.snd R (Module.Dual R N) N)

A basis of N transported to its coordinate copy in Module.Dual R N × N. Over a commutative ring this is a basis of the exterior summand of the hyperbolic polarization, by TauCeti.SpinPolarizationData.hyperbolic_W. The transport itself only needs a commutative semiring.

Equations

• TauCeti.SpinPolarizationData.hyperbolicBasis b = b.map (Submodule.sndEquiv R (Module.Dual R N) N).symm

@[simp]

theorem TauCeti.SpinPolarizationData.coe_hyperbolicBasis_apply {R : Type u} [CommSemiring R] {N : Type v} [AddCommMonoid N] [Module R N] {ι : Type w} (b : Module.Basis ι R N) (i : ι) : ↑((hyperbolicBasis b) i) = (0, b i)