Normalized reflection-pair lifts in Spin groups

Two vectors of quadratic norm one determine a canonical element of the Spin group: the product of their Clifford generators. Its orthogonal action is the ordered product of the two corresponding reflections. This gives a concrete choice of lift for reflection products over positive-definite real quadratic spaces, where nonzero vectors have nonzero norm and can be normalized to unit norm.

Main results

• CliffordAlgebra.spinReflectionPair bundles the product of two unit Clifford generators as a Spin element.
• CliffordAlgebra.spinReflectionPair_self identifies a repeated pair with the identity.
• CliffordAlgebra.spinToOrthogonal_spinReflectionPair computes the orthogonal action of a normalized reflection pair.
• CliffordAlgebra.coe_spinToSpecialOrthogonal_spinReflectionPair gives the same computation for the special-orthogonal projection.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, Section 2.

def CliffordAlgebra.spinReflectionPair {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v w : M) (hv : Q v = 1) (hw : Q w = 1) : ↥(spinGroup Q)

The product of the Clifford generators of two unit vectors, as an element of the Spin group.

@[simp]

theorem CliffordAlgebra.coe_spinReflectionPair {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v w : M) (hv : Q v = 1) (hw : Q w = 1) : ↑(spinReflectionPair Q v w hv hw) = (ι Q) v * (ι Q) w

@[simp]

theorem CliffordAlgebra.spinReflectionPair_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) (hv : Q v = 1) : spinReflectionPair Q v v hv hv = 1

Repeating a unit vector in a reflection pair gives the identity Spin element.

@[simp]

theorem CliffordAlgebra.spinToOrthogonal_spinReflectionPair {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (v w : M) (hv : Q v = 1) (hw : Q w = 1) : have x := ⋯ ▸ invertibleOne; have x_1 := ⋯ ▸ invertibleOne; (spinToOrthogonal Q) (spinReflectionPair Q v w hv hw) = TauCeti.QuadraticMap.reflectionOrthogonal Q v * TauCeti.QuadraticMap.reflectionOrthogonal Q w

The orthogonal action of a normalized reflection-pair lift is the ordered product of the two reflections.

@[simp]

theorem CliffordAlgebra.coe_spinToSpecialOrthogonal_spinReflectionPair {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (v w : M) (hv : Q v = 1) (hw : Q w = 1) : have x := ⋯ ▸ invertibleOne; have x_1 := ⋯ ▸ invertibleOne; ↑((spinToSpecialOrthogonal Q) (spinReflectionPair Q v w hv hw)) = ↑(TauCeti.QuadraticMap.reflectionOrthogonal Q v * TauCeti.QuadraticMap.reflectionOrthogonal Q w)

The special-orthogonal projection of a normalized reflection-pair lift has underlying action the ordered product of the two orthogonal reflections.