Polarization data for quadratic spaces

This file packages the decomposition used to construct spinor modules: two isotropic subspaces in a left- and right-nondegenerate polar pairing and an orthogonal remainder embedded in the scalar line. It also records two elementary consequences: the polar form vanishes identically on each isotropic summand, and a basis of the first summand has a Kronecker-dual family of vectors in the second.

The decomposition also counts dimensions. Over any commutative ring the remainder embeds in the scalar line, so is at most a line; over a field the two isotropic summands are moreover dual to each other, so equidimensional. Hence dim V = 2 · dim W + dim line with dim line ≤ 1, and the parity of dim V decides which, giving dim W = l both in dimension 2l (type Dₗ) and in dimension 2l + 1 (type Bₗ).

Main definitions

• TauCeti.SpinPolarizationData records the decomposition and its consumer-facing coordinates.
• TauCeti.SpinPolarizationData.dualVector: given a basis of the first isotropic summand, the vector of the second summand matching a coordinate functional of that basis.
• TauCeti.SpinPolarizationData.dualBasis: the resulting basis of the second isotropic summand.

Main results

• TauCeti.SpinPolarizationData.polar_W_eq_zero and TauCeti.SpinPolarizationData.polar_W'_eq_zero: the polar form vanishes on each isotropic summand.
• TauCeti.SpinPolarizationData.isOrtho_W_line and TauCeti.SpinPolarizationData.isOrtho_line_W': the orthogonal remainder is orthogonal to each isotropic summand.
• TauCeti.SpinPolarizationData.polar_dualVector: the dual vectors pair with the chosen basis by the Kronecker delta.
• TauCeti.SpinPolarizationData.isOrtho_basis_dualVector: off the diagonal a basis vector is orthogonal to a dual vector.
• TauCeti.SpinPolarizationData.dualBasis_apply: the dual basis has dualVector as its underlying family.
• TauCeti.SpinPolarizationData.finrank_line_le_one: over any commutative ring the remainder is at most a line.
• TauCeti.SpinPolarizationData.finrank_W'_eq_finrank_W and TauCeti.SpinPolarizationData.finrank_eq_two_mul_finrank_W_add_finrank_line: over a field the isotropic summands are equidimensional, and a finite-dimensional polarized space has dimension 2 · dim W + dim line.
• TauCeti.SpinPolarizationData.line_eq_bot_of_even_finrank, TauCeti.SpinPolarizationData.even_finrank_of_line_eq_bot and TauCeti.SpinPolarizationData.finrank_W_eq_of_finrank_eq_two_mul: in even dimension the remainder vanishes, and conversely, and the isotropic summand has half the dimension.
• TauCeti.SpinPolarizationData.finrank_W_eq_of_finrank_eq_two_mul_add_one and TauCeti.SpinPolarizationData.finrank_line_eq_one_of_finrank_eq_two_mul_add_one: in dimension 2l + 1 the isotropic summand again has dimension l, and the remainder is exactly a line.
• TauCeti.SpinPolarizationData.lineCoordinate_surjective_of_ne_bot: over a field the coordinate of a nonzero remainder takes every scalar value.
• TauCeti.SpinPolarizationData.nondegenerate and TauCeti.SpinPolarizationData.nondegenerate_of_line_eq_bot: a polarized quadratic form is nondegenerate, as soon as 2 is a regular scalar of a reduced ring in general and unconditionally when there is no remainder.

structure TauCeti.SpinPolarizationData {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) : Type (max u v)

A polarization of a quadratic space (V, Q): a decomposition V = W ⊕ W' ⊕ line into two isotropic submodules, paired by the polar form so that W' is identified with the dual of W and no nonzero vector of W pairs to zero with all of W', and an orthogonal remainder embedded in the scalar line by a coordinate whose square is Q. It is the data from which the exterior model ⋀·W of a spin representation is built.

• W : Submodule K V

  The isotropic subspace used for exterior multiplication.

• W' : Submodule K V

  The complementary isotropic subspace used for contraction.

• line : Submodule K V

  The orthogonal remainder, embedded in the scalar line by lineCoordinate.

• decompositionEquiv : ((↥self.W × ↥self.W') × ↥self.line) ≃ₗ[K] V

  The direct-sum coordinates of the quadratic space.

• decompositionEquiv_apply (x : (↥self.W × ↥self.W') × ↥self.line) : self.decompositionEquiv x = ↑x.1.1 + ↑x.1.2 + ↑x.2

  The decomposition equivalence adds the three components in the ambient module.

• isotropic_W (x : ↥self.W) : Q ↑x = 0

  The first summand is isotropic.

• isotropic_W' (y : ↥self.W') : Q ↑y = 0

  The second summand is isotropic.

• pairingEquiv : ↥self.W' ≃ₗ[K] Module.Dual K ↥self.W

  The polar form identifies the second summand with the dual of the first.

• pairingEquiv_apply (y : ↥self.W') (x : ↥self.W) : (self.pairingEquiv y) x = QuadraticMap.polar ⇑Q ↑x ↑y

  The pairing equivalence is evaluation by the polar form.

• pairing_separatingLeft (x : ↥self.W) : (∀ (y : ↥self.W'), QuadraticMap.polar ⇑Q ↑x ↑y = 0) → x = 0

  The polar pairing has trivial left radical.

• lineCoordinate : ↥self.line →ₗ[K] K

  The coordinate on the at-most-one-dimensional remainder.

• lineCoordinate_injective : Function.Injective ⇑self.lineCoordinate

  The remainder embeds in the scalar line through its coordinate.

• lineCoordinate_sq (z : ↥self.line) : self.lineCoordinate z * self.lineCoordinate z = Q ↑z

  The quadratic form on the remainder is the square of its coordinate.

• line_orthogonal_W (z : ↥self.line) (x : ↥self.W) : QuadraticMap.polar ⇑Q ↑z ↑x = 0

  The remainder is orthogonal to the first isotropic summand.

• line_orthogonal_W' (z : ↥self.line) (y : ↥self.W') : QuadraticMap.polar ⇑Q ↑z ↑y = 0

  The remainder is orthogonal to the second isotropic summand.

theorem TauCeti.SpinPolarizationData.ext_iff {K : Type u} {inst✝ : CommRing K} {V : Type v} {inst✝¹ : AddCommGroup V} {inst✝² : Module K V} {Q : QuadraticForm K V} {x y : SpinPolarizationData Q} : x = y ↔ x.W = y.W ∧ x.W' = y.W' ∧ x.line = y.line ∧ x.decompositionEquiv ≍ y.decompositionEquiv ∧ x.pairingEquiv ≍ y.pairingEquiv ∧ x.lineCoordinate ≍ y.lineCoordinate

theorem TauCeti.SpinPolarizationData.ext {K : Type u} {inst✝ : CommRing K} {V : Type v} {inst✝¹ : AddCommGroup V} {inst✝² : Module K V} {Q : QuadraticForm K V} {x y : SpinPolarizationData Q} (W : x.W = y.W) (W' : x.W' = y.W') (line : x.line = y.line) (decompositionEquiv : x.decompositionEquiv ≍ y.decompositionEquiv) (pairingEquiv : x.pairingEquiv ≍ y.pairingEquiv) (lineCoordinate : x.lineCoordinate ≍ y.lineCoordinate) : x = y

@[simp]

theorem TauCeti.SpinPolarizationData.decompositionEquiv_symm_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (y : ↥P.W') (z : ↥P.line) : P.decompositionEquiv.symm (↑x + ↑y + ↑z) = ((x, y), z)

Recover the three components of a vector assembled from polarization coordinates.

@[simp]

theorem TauCeti.SpinPolarizationData.decompositionEquiv_symm_coe_W {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) : P.decompositionEquiv.symm ↑x = ((x, 0), 0)

A vector of the first isotropic summand has only that coordinate.

@[simp]

theorem TauCeti.SpinPolarizationData.decompositionEquiv_symm_coe_W' {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (y : ↥P.W') : P.decompositionEquiv.symm ↑y = ((0, y), 0)

A vector of the second isotropic summand has only that coordinate.

@[simp]

theorem TauCeti.SpinPolarizationData.decompositionEquiv_symm_coe_line {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) : P.decompositionEquiv.symm ↑z = ((0, 0), z)

A vector of the orthogonal remainder has only that coordinate.

theorem TauCeti.SpinPolarizationData.pairing_separatingRight {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (y : ↥P.W') (hy : ∀ (x : ↥P.W), QuadraticMap.polar ⇑Q ↑x ↑y = 0) : y = 0

The polar pairing has trivial right radical.

The polar form vanishes on each isotropic summand

theorem TauCeti.SpinPolarizationData.polar_W_eq_zero {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x y : ↥P.W) : QuadraticMap.polar ⇑Q ↑x ↑y = 0

The polar form vanishes on the first isotropic summand of a polarization.

theorem TauCeti.SpinPolarizationData.polar_W'_eq_zero {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x y : ↥P.W') : QuadraticMap.polar ⇑Q ↑x ↑y = 0

The polar form vanishes on the second isotropic summand of a polarization.

The remainder is orthogonal to both isotropic summands

theorem TauCeti.SpinPolarizationData.isOrtho_W_line {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (z : ↥P.line) : QuadraticMap.IsOrtho Q ↑x ↑z

A vector of the first isotropic summand is orthogonal to the remainder.

theorem TauCeti.SpinPolarizationData.isOrtho_line_W' {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) (y : ↥P.W') : QuadraticMap.IsOrtho Q ↑z ↑y

The remainder is orthogonal to the second isotropic summand.

The dual isotropic vectors of a basis

noncomputable def TauCeti.SpinPolarizationData.dualVector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} (b : Module.Basis ι K ↥P.W) (i : ι) : ↥P.W'

The vector of the second isotropic summand W' dual to the i-th basis vector of W: the polarization pairing identifies W' with the dual of W, and this is the vector matching the i-th coordinate functional.

Equations

• P.dualVector b i = P.pairingEquiv.symm (b.coord i)

@[simp]

theorem TauCeti.SpinPolarizationData.pairingEquiv_dualVector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} (b : Module.Basis ι K ↥P.W) (i : ι) : P.pairingEquiv (P.dualVector b i) = b.coord i

The dual vector of the i-th basis vector pairs with W as the i-th coordinate functional.

noncomputable def TauCeti.SpinPolarizationData.dualBasis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Finite ι] : Module.Basis ι K ↥P.W'

The basis of the second isotropic summand dual to b under the polarization pairing.

Equations

• P.dualBasis b = b.dualBasis.map P.pairingEquiv.symm

@[simp]

theorem TauCeti.SpinPolarizationData.dualBasis_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Finite ι] (i : ι) : (P.dualBasis b) i = P.dualVector b i

The dual basis consists of the dual vectors.

@[simp]

theorem TauCeti.SpinPolarizationData.polar_dualVector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (i j : ι) : QuadraticMap.polar ⇑Q ↑(b j) ↑(P.dualVector b i) = if j = i then 1 else 0

The dual vectors pair with the basis of W by the Kronecker delta.

theorem TauCeti.SpinPolarizationData.polar_dualVector_self {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} (b : Module.Basis ι K ↥P.W) (i : ι) : QuadraticMap.polar ⇑Q ↑(b i) ↑(P.dualVector b i) = 1

A basis vector of W pairs with its own dual vector to 1.

theorem TauCeti.SpinPolarizationData.isOrtho_basis_dualVector {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} (b : Module.Basis ι K ↥P.W) {i j : ι} (hij : i ≠ j) : QuadraticMap.IsOrtho Q ↑(b i) ↑(P.dualVector b j)

Off the diagonal a basis vector of W is orthogonal to a dual vector.

theorem TauCeti.SpinPolarizationData.nondegenerate_of_line_eq_bot {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : QuadraticMap.Nondegenerate

A polarization without an orthogonal remainder has nondegenerate quadratic form.

theorem TauCeti.SpinPolarizationData.nondegenerate {K : Type u} [CommRing K] [IsReduced K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (h2 : IsSMulRegular K 2) : QuadraticMap.Nondegenerate

A polarization has nondegenerate quadratic form, whatever its orthogonal remainder, over a reduced ring in which 2 is a regular scalar. So over such a ring nondegeneracy never needs to be assumed alongside polarization data. When the remainder vanishes, TauCeti.SpinPolarizationData.nondegenerate_of_line_eq_bot gives the same conclusion with neither hypothesis.

theorem TauCeti.SpinPolarizationData.finrank_line_le_one {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : Module.finrank K ↥P.line ≤ 1

The orthogonal remainder of a polarization is at most a line, over any commutative ring.

The dimensions of the three summands

A polarization is a decomposition V = W ⊕ W' ⊕ L in which the polar form identifies W' with the dual of W and L sits inside the scalar line. The first fact makes the two isotropic summands equidimensional and the second, finrank_line_le_one above, bounds the remainder by one dimension, so the dimension of V determines the dimension of W up to the parity of finrank V.

theorem TauCeti.SpinPolarizationData.finrank_W'_eq_finrank_W {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : Module.finrank K ↥P.W' = Module.finrank K ↥P.W

The two isotropic summands of a polarization have the same dimension.

theorem TauCeti.SpinPolarizationData.lineCoordinate_surjective_of_ne_bot {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line ≠ ⊥) : Function.Surjective ⇑P.lineCoordinate

A nonzero orthogonal remainder is coordinatized onto the scalars: its coordinate takes every value in the base field.

theorem TauCeti.SpinPolarizationData.finrank_eq_two_mul_finrank_W_add_finrank_line {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] : Module.finrank K V = 2 * Module.finrank K ↥P.W + Module.finrank K ↥P.line

The dimension of a polarized quadratic space: twice the dimension of the isotropic summand W, plus the dimension of the remainder. Together with finrank_line_le_one this pins finrank W to finrank V / 2.

theorem TauCeti.SpinPolarizationData.line_eq_bot_of_even_finrank {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] (h : Even (Module.finrank K V)) : P.line = ⊥

In even dimension a polarization has no remainder. This is the hypothesis under which the exterior parity of ⋀·W splits the spin representation into its two half-spin representations.

theorem TauCeti.SpinPolarizationData.even_finrank_of_line_eq_bot {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] (hline : P.line = ⊥) : Even (Module.finrank K V)

A polarization with no remainder has even dimension. This is the converse of SpinPolarizationData.line_eq_bot_of_even_finrank, so the even-dimensional theory can be stated with the single hypothesis P.line = ⊥ that the parity splitting of the spinor module needs.

theorem TauCeti.SpinPolarizationData.finrank_W_eq_of_finrank_eq_two_mul {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] {l : ℕ} (hV : Module.finrank K V = 2 * l) : Module.finrank K ↥P.W = l

In even dimension the isotropic summand has half the dimension. The isotropic summand W of a polarization of a 2l-dimensional space has dimension l. This is the type Dₗ case, where the spinor module ⋀·W has dimension 2ˡ.

theorem TauCeti.SpinPolarizationData.finrank_W_eq_of_finrank_eq_two_mul_add_one {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] {l : ℕ} (hV : Module.finrank K V = 2 * l + 1) : Module.finrank K ↥P.W = l

In odd dimension the isotropic summand again has half the dimension, rounded down. The isotropic summand W of a polarization of a 2l + 1-dimensional space has dimension l, the odd dimension being taken up by the remainder. This is the type Bₗ case, where the spinor module ⋀·W again has dimension 2ˡ but the parity splitting is not one of representations.

theorem TauCeti.SpinPolarizationData.finrank_line_eq_one_of_finrank_eq_two_mul_add_one {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [FiniteDimensional K V] {l : ℕ} (hV : Module.finrank K V = 2 * l + 1) : Module.finrank K ↥P.line = 1

In odd dimension the remainder is exactly a line. It is spanned by an anisotropic vector, whose action mixes the two exterior parities of the spinor module, which is why they are not subrepresentations in the type Bₗ case.