The Pin group acting on its quadratic space by twisted conjugation

The Pin group is the subgroup of the Lipschitz group consisting of elements whose Clifford norm star x * x is one. This file packages its twisted-conjugation homomorphism and reflection formulas. Both the Pin and Spin actions are restrictions of the common Lipschitz action defined in TauCeti.LinearAlgebra.CliffordAlgebra.Lipschitz.Action.

Main definitions

• CliffordAlgebra.pinToOrthogonal is the induced orthogonal action of the Pin group.

Main results

• CliffordAlgebra.pinToOrthogonal_ι_apply gives the explicit reflection m ↦ m + polar Q v m • v induced by a vector of norm -1.
• CliffordAlgebra.pinToOrthogonal_spinToPin identifies the Pin restriction with the Spin action.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2, and C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

The Pin group

def CliffordAlgebra.pinToOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(pinGroup Q) →* ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The twisted-conjugation homomorphism Pin(Q) → O(Q).

Equations

• CliffordAlgebra.pinToOrthogonal Q = (CliffordAlgebra.lipschitzToOrthogonal Q).comp (CliffordAlgebra.pinToLipschitz Q)

theorem CliffordAlgebra.coe_pinToOrthogonal_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(pinGroup Q)) (m : M) : ↑((pinToOrthogonal Q) x) m = (lipschitzVectorAction Q ((pinToLipschitz Q) x)) m

A Pin element acts through its image in the Lipschitz group. This is not @[simp]: it would rewrite away the pinToOrthogonal head of ι_pinToOrthogonal_apply and pinToOrthogonal_ι_apply, which are the intended normal forms for the Pin action.

theorem CliffordAlgebra.pinToOrthogonal_eq_lipschitzToOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(pinGroup Q)) : (pinToOrthogonal Q) x = (lipschitzToOrthogonal Q) ((pinToLipschitz Q) x)

The Pin action is the Lipschitz action through the canonical inclusion.

@[simp]

theorem CliffordAlgebra.ι_pinToOrthogonal_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(pinGroup Q)) (m : M) : (ι Q) (↑((pinToOrthogonal Q) x) m) = involute ↑x * (ι Q) m * star ↑x

A Pin element acts on a vector by twisted conjugation inside the Clifford algebra. Since a Pin element is unitary, the inverse appearing there is star.

@[simp]

theorem CliffordAlgebra.pinToOrthogonal_ι_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {v : M} (hv : Q v = -1) (m : M) : ↑((pinToOrthogonal Q) ⟨(ι Q) v, ⋯⟩) m = m + QuadraticMap.polar (⇑Q) v m • v

The reflection cut out by a Pin group vector with norm -1.

@[simp]

theorem CliffordAlgebra.pinToOrthogonal_spinToPin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(spinGroup Q)) : (pinToOrthogonal Q) ((spinToPin Q) x) = (spinToOrthogonal Q) x

On Spin, twisted conjugation agrees with the plain Spin action.

theorem CliffordAlgebra.spinToOrthogonal_eq_reflection_mul_reflection_of_coe_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] (x : ↥(spinGroup Q)) (v w : M) [Invertible (Q v)] [Invertible (Q w)] (hx : ↑x = (ι Q) v * (ι Q) w) : (spinToOrthogonal Q) x = TauCeti.QuadraticMap.reflectionOrthogonal Q v * TauCeti.QuadraticMap.reflectionOrthogonal Q w

A Spin element equal to ι Q v * ι Q w acts by the product reflectionOrthogonal Q v * reflectionOrthogonal Q w.