The standard split odd-dimensional polarization

For a commutative ring K, the split odd quadratic space of rank 2n + 1 is (M* × M) × K, where M = Fin n → K, with quadratic form

  ((f, x), z) ↦ f x + z².

This file gives that space its canonical polarization. The two coordinate axes in the hyperbolic summand are the isotropic subspaces, and the final scalar coordinate is the orthogonal remainder. The vector with final coordinate one has quadratic norm one, so the polarization can be used directly by the type-B spin representation.

Main declarations

• TauCeti.SplitOddSpace: the standard split quadratic space (M* × M) × K.
• TauCeti.splitOddForm: its quadratic form ((f, x), z) ↦ f x + z².
• TauCeti.splitOddPolarization: its canonical polarization.
• TauCeti.splitOddBasis: the coordinate basis of the first isotropic summand.
• TauCeti.splitOddRemainderOne: the distinguished norm-one remainder vector.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate II.
• TauCeti.RepresentationTheory.Spin.Polarization.Split.Even, for the corresponding even-dimensional polarization. The odd-dimensional construction adds the scalar coordinate and its norm-one remainder.

@[reducible, inline]

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

The standard split odd-dimensional quadratic space on Fin n → K.

Equations

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

def TauCeti.splitOddForm (K : Type u) [CommRing K] (n : ℕ) : QuadraticForm K (SplitOddSpace K n)

The standard split odd quadratic form, given by ((f, x), z) ↦ f x + z².

Equations

• TauCeti.splitOddForm K n = QuadraticMap.prod (QuadraticForm.dualProd K (Fin n → K)) QuadraticMap.sq

@[simp]

theorem TauCeti.splitOddForm_apply (K : Type u) [CommRing K] (n : ℕ) (x : SplitOddSpace K n) : (splitOddForm K n) x = x.1.1 x.1.2 + x.2 * x.2

Evaluation formula for the standard split odd quadratic form.

@[simp]

theorem TauCeti.polar_splitOddForm (K : Type u) [CommRing K] (n : ℕ) (x y : SplitOddSpace K n) : QuadraticMap.polar (⇑(splitOddForm K n)) x y = x.1.1 y.1.2 + y.1.1 x.1.2 + 2 * x.2 * y.2

Polarization formula for the standard split odd quadratic form.

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

The canonical polarization of the standard split odd quadratic space.

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem TauCeti.splitOddPolarization_line (K : Type u) [CommRing K] (n : ℕ) : (splitOddPolarization K n).line = ⊥.prod ⊤

The orthogonal remainder of the split odd polarization is the final scalar axis.

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

The coordinate basis of the first isotropic summand.

Equations

• TauCeti.splitOddBasis K n = (Pi.basisFun K (Fin n)).map ((TauCeti.splitOddWEquiv✝ K n).symm.trans (LinearEquiv.ofEq (TauCeti.splitOddW✝ K n) (TauCeti.splitOddPolarization K n).W ⋯))

@[simp]

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

A coordinate-basis vector is the corresponding standard vector on the second axis.

noncomputable def TauCeti.splitOddRemainderOne (K : Type u) [CommRing K] (n : ℕ) : ↥(splitOddPolarization K n).line

The distinguished vector of quadratic norm one in the orthogonal remainder.

Equations

• TauCeti.splitOddRemainderOne K n = ⟨((0, 0), 1), ⋯⟩

@[simp]

theorem TauCeti.coe_splitOddRemainderOne (K : Type u) [CommRing K] (n : ℕ) : ↑(splitOddRemainderOne K n) = ((0, 0), 1)

The distinguished remainder vector has the expected ambient coordinates.

@[simp]

theorem TauCeti.splitOddPolarization_lineCoordinate_remainderOne (K : Type u) [CommRing K] (n : ℕ) : (splitOddPolarization K n).lineCoordinate (splitOddRemainderOne K n) = 1

The distinguished remainder vector has scalar coordinate one.

theorem TauCeti.splitOddForm_remainderOne (K : Type u) [CommRing K] (n : ℕ) : (splitOddForm K n) ↑(splitOddRemainderOne K n) = 1

The distinguished remainder vector has quadratic norm one.