Existence of polarization data

This file constructs TauCeti.SpinPolarizationData for finite-dimensional nondegenerate quadratic spaces over separably closed fields of characteristic different from two.

Over such a field a nondegenerate quadratic form is determined up to isometry by its dimension (QuadraticForm.equivalent_of_finrank_eq_of_isSepClosed), so it is isometric to the standard split form of the same dimension, TauCeti.splitEvenForm or TauCeti.splitOddForm. The polarization is the pullback of the canonical polarization of that split form along such an isometry.

Main definition

• TauCeti.SpinPolarizationData.ofNondegenerate constructs the data for a finite-dimensional nondegenerate quadratic space over a separably closed field of characteristic different from two.

noncomputable def TauCeti.SpinPolarizationData.ofNondegenerate {F : Type u} [Field F] [NeZero 2] [IsSepClosed F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] (Q : QuadraticForm F V) (hQ : QuadraticMap.Nondegenerate) : SpinPolarizationData Q

Every finite-dimensional nondegenerate quadratic space over a separably closed field of characteristic different from two admits polarization data.

Equations

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