The standard split even-dimensional polarization

For a commutative ring K, the hyperbolic quadratic space on a finite free module M is M* × M with quadratic form (f, x) ↦ f x. This file gives the coordinate instance M = Fin n → K its canonical polarization: the two coordinate axes are the isotropic summands, their polar pairing is evaluation, and the orthogonal remainder is zero. It is the instance M = Fin n → K of TauCeti.SpinPolarizationData.hyperbolic.

Unlike the existence construction for a nondegenerate quadratic form over a separably closed field, this polarization uses the fixed coordinate summands. Its named coordinate basis can be fed directly into the spin representation and Kostant-lattice constructions.

Main declarations

• TauCeti.SplitEvenSpace: the standard hyperbolic quadratic space M* × M.
• TauCeti.splitEvenForm: its quadratic form (f, x) ↦ f x.
• TauCeti.splitEvenPolarization: the canonical polarization by the two coordinate axes.
• TauCeti.splitEvenBasis: the coordinate basis of the first isotropic summand.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate IV.

@[reducible, inline]

abbrev TauCeti.SplitEvenSpace (K : Type u) [CommRing K] (n : ℕ) : Type u

The standard split even-dimensional quadratic space on Fin n → K: the product of its dual coordinate module and coordinate module.

Equations

• TauCeti.SplitEvenSpace K n = (Module.Dual K (Fin n → K) × (Fin n → K))

def TauCeti.splitEvenForm (K : Type u) [CommRing K] (n : ℕ) : QuadraticForm K (SplitEvenSpace K n)

The standard split quadratic form on M* × M, given by (f, x) ↦ f x.

Equations

• TauCeti.splitEvenForm K n = QuadraticForm.dualProd K (Fin n → K)

@[simp]

theorem TauCeti.splitEvenForm_apply (K : Type u) [CommRing K] (n : ℕ) (x : SplitEvenSpace K n) : (splitEvenForm K n) x = x.1 x.2

Evaluation formula for the standard split quadratic form.

@[simp]

theorem TauCeti.polar_splitEvenForm (K : Type u) [CommRing K] (n : ℕ) (x y : SplitEvenSpace K n) : QuadraticMap.polar (⇑(splitEvenForm K n)) x y = x.1 y.2 + y.1 x.2

Polarization formula for the standard split quadratic form.

noncomputable def TauCeti.splitEvenPolarization (K : Type u) [CommRing K] (n : ℕ) : SpinPolarizationData (splitEvenForm K n)

The canonical polarization of the standard split quadratic space.

The coordinate axis is the first isotropic summand, the dual-coordinate axis is the second, and the orthogonal remainder is zero.

Equations

• TauCeti.splitEvenPolarization K n = TauCeti.SpinPolarizationData.hyperbolic ⋯

@[simp]

theorem TauCeti.splitEvenPolarization_W (K : Type u) [CommRing K] (n : ℕ) : (splitEvenPolarization K n).W = ⊥.prod ⊤

The first isotropic summand of the standard split polarization is the coordinate axis.

@[simp]

theorem TauCeti.splitEvenPolarization_W' (K : Type u) [CommRing K] (n : ℕ) : (splitEvenPolarization K n).W' = ⊤.prod ⊥

The second isotropic summand of the standard split polarization is the dual-coordinate axis.

@[simp]

theorem TauCeti.splitEvenPolarization_line (K : Type u) [CommRing K] (n : ℕ) : (splitEvenPolarization K n).line = ⊥

The standard split even-dimensional polarization has no orthogonal remainder.

noncomputable def TauCeti.splitEvenBasis (K : Type u) [CommRing K] (n : ℕ) : Module.Basis (Fin n) K ↥(splitEvenPolarization K n).W

The coordinate basis of the first isotropic summand in the standard split polarization.

Equations

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

@[simp]

theorem TauCeti.coe_splitEvenBasis (K : Type u) [CommRing K] (n : ℕ) (i : Fin n) : ↑((splitEvenBasis K n) i) = (0, Pi.single i 1)

A coordinate-basis vector of the first isotropic summand is the corresponding standard coordinate vector on the second axis of the split space.