The two signs of the line coordinate

A polarization P of a quadratic space V = W ⊕ W' ⊕ L carries a coordinate on its orthogonal remainder L whose square is Q. Negating this coordinate preserves its square and gives a polarization P⁻ = P.negLineCoordinate with the same isotropic summands, the same decomposition and the same pairing. Both make the exterior algebra S = ⋀·W into a module over the Clifford algebra, and this file compares the two Fock actions c_P and c_{P⁻}.

The comparison is through the parity operator J = CliffordAlgebra.involute of S:

c_{P⁻}(x) = J ∘ c_P(involute x) ∘ J for every Clifford element x.

On an even element the grade involution does nothing, so J intertwines the two Fock actions of the even Clifford subalgebra, and in particular the two Spin representations: the choice of sign is invisible to Spin(V).

On the whole Clifford algebra it is visible in odd dimension. There the volume element ω of a spanning orthogonal list is central, odd, and squares to a scalar c, so whenever W is finite free it acts on S by a scalar λ with λ² = c under c_P, and by -λ under c_{P⁻}.

The scalar c vanishes for some spanning orthogonal lists, such as those containing zero vectors. For finite-dimensional V over a field of characteristic not two, take instead an orthogonal basis of the nondegenerate form Q, so that every Q vᵢ is nonzero. Then c is nonzero, so λ ≠ -λ and the two Fock actions are the two distinct characters of the centre F ⊕ F ω. Each of them alone kills one of the two central idempotents (1 ± λ⁻¹ ω) / 2, so neither is faithful, but together they are: the combined action x ↦ (c_P(x), c_{P⁻}(x)) is an algebra isomorphism from the Clifford algebra onto End S × End S. This is the operator form of the odd structure theorem CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one, with the two blocks labelled by the two signs of the line coordinate.

Main definitions

• TauCeti.SpinPolarizationData.negLineCoordinate: the polarization P⁻ with the line coordinate negated.
• TauCeti.SpinPolarizationData.spinRepEquivNegLineCoordinate: the parity operator, as an equivalence between the Spin representations of P and P⁻.
• TauCeti.SpinPolarizationData.cliffordEquivEndProd: in odd dimension, for finite-dimensional V over a field of characteristic not two, the combined Fock action of P and P⁻, as an algebra isomorphism CliffordAlgebra Q ≃ₐ[F] End S × End S.

Main results

• TauCeti.SpinPolarizationData.spinAction_negLineCoordinate_apply: c_{P⁻}(x) = J c_P(involute x) J.
• TauCeti.SpinPolarizationData.spinAction_negLineCoordinate_apply_of_mem_even: on even elements, c_{P⁻}(x) = J c_P(x) J.
• TauCeti.SpinPolarizationData.exists_spinAction_volume_eq_algebraMap: the volume element acts by opposite scalars λ and -λ under the two Fock actions, with λ² = c, when W is finite free.
• TauCeti.SpinPolarizationData.spinAction_prod_bijective: in odd dimension, for finite-dimensional V over a field of characteristic not two, the combined Fock action is bijective, so the direct sum of the two spinor modules is faithful.
• TauCeti.SpinPolarizationData.not_injective_spinAction_of_odd_finrank: under the same hypotheses, a single Fock action is not faithful.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §5: the two inequivalent irreducible Clifford modules in odd dimension, distinguished by the action of the volume element.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §20.1.

@[reducible, inline]

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

The polarization P⁻ with the same isotropic summands, decomposition and pairing as P, and the opposite line coordinate. Negating the coordinate preserves its square Q.

This is an abbrev so that the isotropic summand of P⁻ is reducibly that of P: the two Fock actions are then actions on one and the same spinor module ⋀·W, with its instances, and can be compared there.

theorem TauCeti.SpinPolarizationData.lineCoordinate_negLineCoordinate {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) : P.negLineCoordinate.lineCoordinate z = -P.lineCoordinate z

The line coordinate of P⁻ is the negative of that of P.

@[simp]

theorem TauCeti.SpinPolarizationData.negLineCoordinate_negLineCoordinate {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : P.negLineCoordinate.negLineCoordinate = P

Negating the line coordinate twice gives back the polarization.

theorem TauCeti.SpinPolarizationData.spinAction_negLineCoordinate_ι_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (v : V) (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P.negLineCoordinate) ((CliffordAlgebra.ι Q) v)) s = -CliffordAlgebra.involute (((spinAction Q P) ((CliffordAlgebra.ι Q) v)) (CliffordAlgebra.involute s))

The generators under the opposite line coordinate. A vector acts through P⁻ by minus the conjugate of its action through P by the parity operator J = involute of ⋀·W.

theorem TauCeti.SpinPolarizationData.spinAction_negLineCoordinate_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : CliffordAlgebra Q) (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P.negLineCoordinate) x) s = CliffordAlgebra.involute (((spinAction Q P) (CliffordAlgebra.involute x)) (CliffordAlgebra.involute s))

The two Fock actions differ by the parity operator. For every Clifford element x, c_{P⁻}(x) = J ∘ c_P(involute x) ∘ J, where J = involute is the grade involution of ⋀·W.

theorem TauCeti.SpinPolarizationData.spinAction_negLineCoordinate_apply_of_mem_even {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {x : CliffordAlgebra Q} (hx : x ∈ CliffordAlgebra.even Q) (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P.negLineCoordinate) x) s = CliffordAlgebra.involute (((spinAction Q P) x) (CliffordAlgebra.involute s))

On the even Clifford subalgebra the parity operator intertwines the two Fock actions: c_{P⁻}(x) = J ∘ c_P(x) ∘ J for x even.

noncomputable def TauCeti.SpinPolarizationData.spinRepEquivNegLineCoordinate {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : (spinRep Q P).Equiv (spinRep Q P.negLineCoordinate)

The sign of the line coordinate is invisible to the Spin group. The parity operator J = involute of ⋀·W is an equivalence between the Spin representations of P and of P⁻.

@[simp]

theorem TauCeti.SpinPolarizationData.spinRepEquivNegLineCoordinate_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (s : ExteriorAlgebra K ↥P.W) : P.spinRepEquivNegLineCoordinate s = CliffordAlgebra.involute s

@[simp]

theorem TauCeti.SpinPolarizationData.spinRepEquivNegLineCoordinate_symm_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (s : ExteriorAlgebra K ↥P.W) : P.spinRepEquivNegLineCoordinate.symm s = CliffordAlgebra.involute s

The inverse of the parity operator is again the grade involution of ⋀·W.

theorem TauCeti.SpinPolarizationData.exists_spinAction_volume_eq_algebraMap {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Module.Free K ↥P.W] [Module.Finite K ↥P.W] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) : ∃ (a : K), a * a = (-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod ∧ (spinAction Q P) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = (algebraMap K (Module.End K (ExteriorAlgebra K ↥P.W))) a ∧ (spinAction Q P.negLineCoordinate) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = (algebraMap K (Module.End K (ExteriorAlgebra K ↥P.W))) (-a)

The volume element acts by opposite scalars under the two signs. For a spanning list of pairwise orthogonal vectors of odd length, the volume element ω is central with ω² = c = (-1) ^ (n choose 2) ∏ Q vᵢ. When W is finite free, the Fock action of P sends ω to a scalar λ with λ² = c, and since ω is odd the Fock action of P⁻ sends it to -λ.

The two signs in odd dimension

theorem TauCeti.SpinPolarizationData.spinAction_prod_surjective {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) : Function.Surjective ⇑((spinAction Q P).prod (spinAction Q P.negLineCoordinate))

The combined Fock action of the two signs is onto in odd dimension: given endomorphisms f and g of ⋀·W, some Clifford element acts by f through P and by g through P⁻.

theorem TauCeti.SpinPolarizationData.spinAction_prod_bijective {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) : Function.Bijective ⇑((spinAction Q P).prod (spinAction Q P.negLineCoordinate))

The direct sum of the two spinor modules is faithful in odd dimension: the combined Fock action of P and P⁻ is a bijection from the Clifford algebra onto End S × End S.

noncomputable def TauCeti.SpinPolarizationData.cliffordEquivEndProd {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) : CliffordAlgebra Q ≃ₐ[F] Module.End F (ExteriorAlgebra F ↥P.W) × Module.End F (ExteriorAlgebra F ↥P.W)

The odd structure theorem, labelled by the two signs of the line coordinate: in odd dimension the combined Fock action of P and P⁻ is an algebra isomorphism from the Clifford algebra onto End S × End S, for S = ⋀·W.

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordEquivEndProd_apply {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) (x : CliffordAlgebra Q) : (P.cliffordEquivEndProd hodd) x = ((spinAction Q P) x, (spinAction Q P.negLineCoordinate) x)

theorem TauCeti.SpinPolarizationData.not_injective_spinAction_of_odd_finrank {F : Type u} [Field F] {V : Type v} [AddCommGroup V] [Module F V] [FiniteDimensional F V] {Q : QuadraticForm F V} (P : SpinPolarizationData Q) [NeZero 2] (hodd : Odd (Module.finrank F V)) : ¬Function.Injective ⇑(spinAction Q P)

A single Fock action is not faithful in odd dimension: the central idempotent attached to the opposite sign is a nonzero element acting by zero.