Sign-switch equivalence for Clifford algebras

For a quadratic form P over a commutative ring, adjoining one positive line ⟨1⟩ makes the Clifford algebras of P and -P isomorphic: Cl(P ⊕ ⟨1⟩) ≃ₐ Cl(-P ⊕ ⟨1⟩). Writing e for the generator of the adjoined line, the isomorphism sends ι (m, r) to e * ι (m, 0) + r • e.

Main results

• CliffordAlgebra.signSwitchEquiv: the sign-switch algebra equivalence;
• CliffordAlgebra.signSwitchEquiv_ι: its equation on generators;
• CliffordAlgebra.signSwitchEquiv_symm_apply_ι: the inverse generator equation.

References

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

def CliffordAlgebra.signSwitchEquiv {R : Type u_1} {N : Type u_2} [CommRing R] [AddCommGroup N] [Module R N] (P : QuadraticForm R N) : CliffordAlgebra (QuadraticMap.prod P QuadraticMap.sq) ≃ₐ[R] CliffordAlgebra (QuadraticMap.prod (-P) QuadraticMap.sq)

Adjoining a positive line to a quadratic form or to its negation gives equivalent Clifford algebras: Cl(P ⊕ ⟨1⟩) ≃ₐ[R] Cl(-P ⊕ ⟨1⟩).

@[simp]

theorem CliffordAlgebra.signSwitchEquiv_ι {R : Type u_1} {N : Type u_2} [CommRing R] [AddCommGroup N] [Module R N] (P : QuadraticForm R N) (x : N × R) : (signSwitchEquiv P) ((ι (QuadraticMap.prod P QuadraticMap.sq)) x) = (ι (QuadraticMap.prod (-P) QuadraticMap.sq)) (0, 1) * (ι (QuadraticMap.prod (-P) QuadraticMap.sq)) (x.1, 0) + x.2 • (ι (QuadraticMap.prod (-P) QuadraticMap.sq)) (0, 1)

The sign-switch equivalence sends ι (m, r) to e * ι (m, 0) + r • e, where e = ι (0, 1) generates the adjoined positive line.

@[simp]

theorem CliffordAlgebra.signSwitchEquiv_symm_apply_ι {R : Type u_1} {N : Type u_2} [CommRing R] [AddCommGroup N] [Module R N] (P : QuadraticForm R N) (x : N × R) : (signSwitchEquiv P).symm ((ι (QuadraticMap.prod (-P) QuadraticMap.sq)) x) = (ι (QuadraticMap.prod P QuadraticMap.sq)) (0, 1) * (ι (QuadraticMap.prod P QuadraticMap.sq)) (x.1, 0) + x.2 • (ι (QuadraticMap.prod P QuadraticMap.sq)) (0, 1)

The inverse sign-switch equivalence is given by the same formula on generators.