Complex conjugation on a complexified real Clifford algebra

For a real quadratic form Q, the complexified Clifford algebra Cℓ(ℂ ⊗ V, Q_ℂ) carries two commuting involutions: Mathlib's complex-linear Clifford conjugation star = reverse ∘ involute, which negates every vector, and complex conjugation CliffordAlgebra.complexConj of the coefficients, which fixes the real vectors ι (1 ⊗ₜ v). Their composite CliffordAlgebra.conjStar is the conjugate-linear anti-automorphism of the complexified algebra. For the negative-definite form Q = -g of a Euclidean space this is the involution with respect to which a representation on a Hermitian space is a *-representation, so that Clifford multiplication by a real vector is skew-Hermitian.

Under the identification CliffordAlgebra.equivBaseChange with the tensor carrier ℂ ⊗[ℝ] Cℓ(V, Q), CliffordAlgebra.complexConj is conj ⊗ id and CliffordAlgebra.conjStar is the tensor-product star, that is conj ⊗ star. The latter uses the real StarModule structure CliffordAlgebra.starModule_of_trivialStar, enabled locally.

Main definitions

• CliffordAlgebra.complexConj: coefficientwise complex conjugation, a real algebra automorphism of Cℓ(ℂ ⊗ V, Q_ℂ).
• CliffordAlgebra.conjStar: the conjugate-linear map complexConj ∘ star.

Main results

• CliffordAlgebra.complexConj_smul: complexConj is conjugate-linear.
• CliffordAlgebra.complexConj_unique: complexConj is the unique conjugate-linear ring endomorphism fixing the real vectors.
• CliffordAlgebra.complexConj_complexConj: complexConj is involutive.
• CliffordAlgebra.complexConj_eq_self_iff: the elements fixed by complexConj are exactly the real Clifford elements, the image of CliffordAlgebra.ofBaseChangeAux.
• CliffordAlgebra.ofBaseChangeAux_mem_range_ι_iff: a real Clifford element is a vector exactly when it is a vector of the complexification.
• CliffordAlgebra.conjStar_mul and CliffordAlgebra.conjStar_conjStar: conjStar is an involutive anti-automorphism.
• CliffordAlgebra.toBaseChange_conjStar: on the tensor carrier conjStar is the tensor-product star.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I.
• L. Nicolaescu, Lectures on the Geometry of Manifolds, the chapter on Dirac operators.

Complex conjugation of coefficients

noncomputable def CliffordAlgebra.complexConj {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) : CliffordAlgebra (QuadraticForm.baseChange ℂ Q) ≃+* CliffordAlgebra (QuadraticForm.baseChange ℂ Q)

Complex conjugation of the coefficients of the complexified Clifford algebra: the ring automorphism of Cℓ(ℂ ⊗ V, Q_ℂ) conjugating scalars and fixing the real vectors ι (1 ⊗ₜ v). It is CliffordAlgebra.baseChangeCongr for Complex.conjAe, stated as a ring equivalence since its conjugate-linearity is recorded by CliffordAlgebra.complexConj_smul.

theorem CliffordAlgebra.complexConj_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) x = (baseChangeCongr Complex.conjAe Q) x

@[simp]

theorem CliffordAlgebra.toBaseChange_complexConj {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (toBaseChange ℂ Q) ((complexConj Q) x) = (Algebra.TensorProduct.congr Complex.conjAe AlgEquiv.refl) ((toBaseChange ℂ Q) x)

On the tensor carrier ℂ ⊗[ℝ] Cℓ(V, Q), CliffordAlgebra.complexConj is conj ⊗ id.

@[simp]

theorem CliffordAlgebra.complexConj_algebraMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (z : ℂ) : (complexConj Q) ((algebraMap ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q))) z) = (algebraMap ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q))) ((starRingEnd ℂ) z)

@[simp]

theorem CliffordAlgebra.complexConj_ι_tmul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : (complexConj Q) ((ι (QuadraticForm.baseChange ℂ Q)) (z ⊗ₜ[ℝ] v)) = (ι (QuadraticForm.baseChange ℂ Q)) ((starRingEnd ℂ) z ⊗ₜ[ℝ] v)

@[simp]

theorem CliffordAlgebra.complexConj_ofBaseChangeAux {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q) : (complexConj Q) ((ofBaseChangeAux ℂ Q) x) = (ofBaseChangeAux ℂ Q) x

CliffordAlgebra.complexConj fixes the real Clifford algebra.

@[simp]

theorem CliffordAlgebra.complexConj_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (z : ℂ) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) (z • x) = (starRingEnd ℂ) z • (complexConj Q) x

CliffordAlgebra.complexConj is conjugate-linear.

theorem CliffordAlgebra.complexConj_unique {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (f : CliffordAlgebra (QuadraticForm.baseChange ℂ Q) →+* CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) (hsmul : ∀ (z : ℂ) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)), f (z • x) = (starRingEnd ℂ) z • f x) (hι : ∀ (v : V), f ((ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) = (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) : f = ↑(complexConj Q)

CliffordAlgebra.complexConj is the unique conjugate-linear ring endomorphism of the complexified Clifford algebra fixing the real vectors ι (1 ⊗ₜ v).

@[simp]

theorem CliffordAlgebra.complexConj_complexConj {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) ((complexConj Q) x) = x

CliffordAlgebra.complexConj is involutive.

@[simp]

theorem CliffordAlgebra.complexConj_symm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) : (complexConj Q).symm = complexConj Q

CliffordAlgebra.complexConj is its own inverse.

@[simp]

theorem CliffordAlgebra.complexConj_involute {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) (involute x) = involute ((complexConj Q) x)

@[simp]

theorem CliffordAlgebra.complexConj_reverse {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) (reverse x) = reverse ((complexConj Q) x)

@[simp]

theorem CliffordAlgebra.complexConj_star {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (complexConj Q) (star x) = star ((complexConj Q) x)

theorem CliffordAlgebra.complexConj_ι {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (w : TensorProduct ℝ ℂ V) : (complexConj Q) ((ι (QuadraticForm.baseChange ℂ Q)) w) = (ι (QuadraticForm.baseChange ℂ Q)) ((TauCeti.tmulConj V) w)

CliffordAlgebra.complexConj acts on the generators through the conjugation TauCeti.tmulConj V of ℂ ⊗[ℝ] V.

The real elements

@[simp]

theorem CliffordAlgebra.complexConj_eq_self_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) {x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)} : (complexConj Q) x = x ↔ ∃ (y : CliffordAlgebra Q), (ofBaseChangeAux ℂ Q) y = x

The real elements of the complexified Clifford algebra. An element is fixed by complex conjugation of the coefficients exactly when it lies in the image of the real Clifford algebra.

theorem CliffordAlgebra.ofBaseChangeAux_mem_range_ι_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {Q : QuadraticForm ℝ V} {x : CliffordAlgebra Q} : (ofBaseChangeAux ℂ Q) x ∈ (ι (QuadraticForm.baseChange ℂ Q)).range ↔ x ∈ (ι Q).range

A real Clifford element is a vector exactly when its image in the complexified Clifford algebra is a vector.

The conjugate-linear Clifford involution

noncomputable def CliffordAlgebra.conjStar {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) : CliffordAlgebra (QuadraticForm.baseChange ℂ Q) →ₗ⋆[ℂ] CliffordAlgebra (QuadraticForm.baseChange ℂ Q)

The conjugate-linear Clifford involution of the complexified Clifford algebra: Clifford conjugation star = reverse ∘ involute followed by complex conjugation of the coefficients. It is an involutive anti-automorphism (CliffordAlgebra.conjStar_mul, CliffordAlgebra.conjStar_conjStar) negating the real vectors.

theorem CliffordAlgebra.conjStar_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (conjStar Q) x = (complexConj Q) (star x)

theorem CliffordAlgebra.conjStar_apply' {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (conjStar Q) x = star ((complexConj Q) x)

@[simp]

theorem CliffordAlgebra.conjStar_mul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x y : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (conjStar Q) (x * y) = (conjStar Q) y * (conjStar Q) x

CliffordAlgebra.conjStar reverses products.

@[simp]

theorem CliffordAlgebra.conjStar_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) : (conjStar Q) 1 = 1

@[simp]

theorem CliffordAlgebra.conjStar_conjStar {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (conjStar Q) ((conjStar Q) x) = x

CliffordAlgebra.conjStar is involutive.

@[simp]

theorem CliffordAlgebra.conjStar_algebraMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (z : ℂ) : (conjStar Q) ((algebraMap ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q))) z) = (algebraMap ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q))) ((starRingEnd ℂ) z)

@[simp]

theorem CliffordAlgebra.conjStar_ι_tmul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : (conjStar Q) ((ι (QuadraticForm.baseChange ℂ Q)) (z ⊗ₜ[ℝ] v)) = -(ι (QuadraticForm.baseChange ℂ Q)) ((starRingEnd ℂ) z ⊗ₜ[ℝ] v)

CliffordAlgebra.conjStar negates vectors and conjugates their coefficients; in particular it negates the real vectors ι (1 ⊗ₜ v).

theorem CliffordAlgebra.conjStar_ι {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (w : TensorProduct ℝ ℂ V) : (conjStar Q) ((ι (QuadraticForm.baseChange ℂ Q)) w) = -(ι (QuadraticForm.baseChange ℂ Q)) ((TauCeti.tmulConj V) w)

CliffordAlgebra.conjStar sends the generator of a complex vector w to minus the generator of its conjugate TauCeti.tmulConj V w.

@[simp]

theorem CliffordAlgebra.conjStar_ofBaseChangeAux {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q) : (conjStar Q) ((ofBaseChangeAux ℂ Q) x) = (ofBaseChangeAux ℂ Q) (star x)

On the real Clifford algebra, CliffordAlgebra.conjStar is Clifford conjugation.

theorem CliffordAlgebra.toBaseChange_conjStar {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Q : QuadraticForm ℝ V) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (toBaseChange ℂ Q) ((conjStar Q) x) = star ((toBaseChange ℂ Q) x)

On the tensor carrier ℂ ⊗[ℝ] Cℓ(V, Q), CliffordAlgebra.conjStar is the tensor-product star, acting by z ⊗ₜ a ↦ conj z ⊗ₜ star a.