Sign-switch equivalence for Clifford algebras #
Adjoining one positive line identifies the Clifford algebras of a quadratic form and its negation. The construction is generic over a commutative ring.
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)
:
Adjoining a positive line to a quadratic form or to its negation gives equivalent Clifford algebras.
Equations
- CliffordAlgebra.signSwitchEquiv P = AlgEquiv.ofAlgHom (CliffordAlgebra.signSwitchTo✝ P (-P) ⋯) (CliffordAlgebra.signSwitchTo✝ (-P) P ⋯) ⋯ ⋯
Instances For
@[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 a generating pair to the product with the new positive generator plus its scalar component times the new positive generator.
@[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 has the same equation on Clifford generators.