The Clifford algebras of Q and -Q over a ring containing a square root of -1

There is in general no algebra isomorphism between the Clifford algebras of a quadratic form Q and of its negative; Mathlib's CliffordAlgebra.evenEquivEvenNeg only identifies their even subalgebras. If the coefficient ring contains an element u with u * u = -1, however, the vectors u • ι (-Q) m satisfy the Clifford relation of Q, and ι Q m ↦ u • ι (-Q) m extends to an algebra isomorphism CliffordAlgebra.equivNeg of the full Clifford algebras. Over ℂ, with u = Complex.I, this is the map v ↦ i v from the complexified Clifford algebra of a real form to that of its negative, which compares the positive-definite and negative-definite (geometric) sign conventions for Clifford multiplication.

The isomorphism preserves the ℤ/2-grading and commutes with the grade involution, reversal and Clifford conjugation. On the even subalgebra the factors of u pair up to u * u = -1, so a bivector ι Q a * ι Q b goes to -(ι (-Q) a * ι (-Q) b); this is the sign of CliffordAlgebra.evenToNeg, and CliffordAlgebra.equivNeg restricts to that map on even elements. In particular, the complex isomorphism of ℂ ⊗ V restricts on the image of the real even subalgebra to the scalar extension of CliffordAlgebra.evenEquivEvenNeg. For a nonzero real vector space it is not the scalar extension of any real isomorphism of the full algebras: it sends a nonzero real generator ι Q m to i • ι (-Q) m, which is not real. (When the vector space is zero, both algebras are the scalars and the isomorphism is the identity.)

The target form is a parameter Q' with a proof of Q' = -Q, as for Mathlib's CliffordAlgebra.evenToNeg. This covers the inverse direction, and the base-changed form (-Q).baseChange A, which is only propositionally equal to -(Q.baseChange A).

Main results

• CliffordAlgebra.equivNeg: the isomorphism CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra Q', ι Q m ↦ u • ι Q' m, for Q' = -Q and u * u = -1.
• CliffordAlgebra.equivNeg_symm: its inverse is the same construction for -u.
• CliffordAlgebra.equivNeg_ι_mul_ι: a bivector ι Q a * ι Q b goes to -(ι Q' a * ι Q' b).
• CliffordAlgebra.equivNeg_coe: on even elements it is CliffordAlgebra.evenToNeg.
• CliffordAlgebra.map_evenOdd_equivNeg: it carries evenOdd Q i onto evenOdd Q' i.
• CliffordAlgebra.equivNeg_involute, CliffordAlgebra.equivNeg_reverse, CliffordAlgebra.equivNeg_star: compatibility with the Clifford involutions.
• CliffordAlgebra.map_equivNeg: naturality along quadratic isometries.
• CliffordAlgebra.equivNeg_ofBaseChangeAux: after extension of scalars to an algebra containing u, it restricts on real even elements to CliffordAlgebra.evenEquivEvenNeg.

References

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

def CliffordAlgebra.equivNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) : CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra Q'

If u * u = -1, the Clifford algebras of Q and of Q' = -Q are isomorphic, by the algebra map sending a vector ι Q m to u • ι Q' m; this is CliffordAlgebra.equivOfIsometry for the isometry m ↦ u • m. Over ℂ, with u = Complex.I, this is the map v ↦ i v between the complexified Clifford algebras of a real form and of its negative.

@[simp]

theorem CliffordAlgebra.equivNeg_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (m : M) : (equivNeg Q Q' h hu) ((ι Q) m) = u • (ι Q') m

CliffordAlgebra.equivNeg multiplies each vector by u.

@[simp]

theorem CliffordAlgebra.equivNeg_symm_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (m : M) : (equivNeg Q Q' h hu).symm ((ι Q') m) = -(u • (ι Q) m)

The inverse of CliffordAlgebra.equivNeg multiplies each vector by -u.

theorem CliffordAlgebra.equivNeg_symm {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) : (equivNeg Q Q' h hu).symm = equivNeg Q' Q ⋯ ⋯

The inverse of CliffordAlgebra.equivNeg for u is CliffordAlgebra.equivNeg for -u, in the opposite direction.

theorem CliffordAlgebra.equivNeg_ι_mul_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (a b : M) : (equivNeg Q Q' h hu) ((ι Q) a * (ι Q) b) = -((ι Q') a * (ι Q') b)

A bivector ι Q a * ι Q b goes to the negative -(ι Q' a * ι Q' b) of the corresponding bivector, since the two factors of u multiply to -1.

@[simp]

theorem CliffordAlgebra.equivNeg_coe {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (x : ↥(even Q)) : (equivNeg Q Q' h hu) ↑x = ↑((evenToNeg Q Q' h) x)

On the even subalgebra, CliffordAlgebra.equivNeg is Mathlib's CliffordAlgebra.evenToNeg; for Q' = -Q this is CliffordAlgebra.evenEquivEvenNeg (CliffordAlgebra.evenEquivEvenNeg_apply). In particular it does not depend on the choice of u there.

@[simp]

theorem CliffordAlgebra.equivNeg_involute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (x : CliffordAlgebra Q) : (equivNeg Q Q' h hu) (involute x) = involute ((equivNeg Q Q' h hu) x)

CliffordAlgebra.equivNeg commutes with the grade involution.

@[simp]

theorem CliffordAlgebra.equivNeg_reverse {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (x : CliffordAlgebra Q) : (equivNeg Q Q' h hu) (reverse x) = reverse ((equivNeg Q Q' h hu) x)

CliffordAlgebra.equivNeg commutes with reversal.

@[simp]

theorem CliffordAlgebra.equivNeg_star {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (x : CliffordAlgebra Q) : (equivNeg Q Q' h hu) (star x) = star ((equivNeg Q Q' h hu) x)

CliffordAlgebra.equivNeg commutes with Clifford conjugation.

theorem CliffordAlgebra.map_evenOdd_equivNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) (i : ZMod 2) : Submodule.map (equivNeg Q Q' h hu).toLinearMap (evenOdd Q i) = evenOdd Q' i

CliffordAlgebra.equivNeg preserves the ℤ/2-grading: it carries evenOdd Q i onto evenOdd Q' i.

@[simp]

theorem CliffordAlgebra.equivNeg_mem_evenOdd_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} (h : Q' = -Q) {u : R} (hu : u * u = -1) {x : CliffordAlgebra Q} {i : ZMod 2} : (equivNeg Q Q' h hu) x ∈ evenOdd Q' i ↔ x ∈ evenOdd Q i

An element lies in evenOdd Q' i after applying CliffordAlgebra.equivNeg exactly when it lies in evenOdd Q i.

theorem CliffordAlgebra.map_equivNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q Q' : QuadraticForm R M) (h : Q' = -Q) {u : R} (hu : u * u = -1) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] {Q₂ Q₂' : QuadraticForm R M₂} (h₂ : Q₂' = -Q₂) (f : Q →qᵢ Q₂) (f' : Q' →qᵢ Q₂') (hf : f'.toLinearMap = f.toLinearMap) (x : CliffordAlgebra Q) : (map f') ((equivNeg Q Q' h hu) x) = (equivNeg Q₂ Q₂' h₂ hu) ((map f) x)

CliffordAlgebra.equivNeg is natural along quadratic isometries: for an isometry f from Q to Q₂, whose underlying linear map is also an isometry f' from Q' to Q₂', the isomorphisms for Q and for Q₂ intertwine the algebra maps induced by f and by f'.

theorem CliffordAlgebra.equivNeg_ofBaseChangeAux {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {A : Type u_3} [CommRing A] [Algebra R A] [Invertible 2] (Q : QuadraticForm R M) {u : A} (hu : u * u = -1) (x : ↥(even Q)) : (equivNeg (QuadraticForm.baseChange A Q) (QuadraticForm.baseChange A (-Q)) ⋯ hu) ((ofBaseChangeAux A Q) ↑x) = (ofBaseChangeAux A (-Q)) ↑((evenEquivEvenNeg Q) x)

After extension of scalars to an algebra containing u with u * u = -1, the isomorphism CliffordAlgebra.equivNeg of the extended Clifford algebras of Q and -Q restricts on the image of the even subalgebra to the scalar extension of CliffordAlgebra.evenEquivEvenNeg. Over ℂ, this compares v ↦ i v with the real even-algebra comparison of Q and -Q.