The scalar-part trace of a Clifford algebra

Over a commutative ring in which 2 is invertible, Mathlib's CliffordAlgebra.equivExterior identifies CliffordAlgebra Q with ExteriorAlgebra R M as a module. Reading off the degree-zero component on the exterior side gives a linear functional

CliffordAlgebra.scalarTrace Q : CliffordAlgebra Q →ₗ[R] R,

the scalar part τ of a multivector. It is normalized by τ 1 = 1, kills every generator, and on a product of two generators returns the symmetric bilinear form of Q: τ (ι Q a * ι Q b) = QuadraticMap.associated Q a b.

Although it is defined without any finiteness, τ behaves like a trace: it is invariant under the grade involution and under reversion, it vanishes on the odd part, and it is cyclic, τ (x * y) = τ (y * x). When M is spanned by pairwise orthogonal vectors these properties characterize it: every cyclic functional invariant under the grade involution is a multiple of τ. Applied to the trace of the left regular representation this gives the regular-trace formula: over a field in which 2 is invertible, for every quadratic form on a finite-dimensional space, τ x = 2 ^ (-finrank K V) * trace (x * ·). In particular τ is preserved by every algebra isomorphism between Clifford algebras of finite-dimensional spaces.

Main definitions

• CliffordAlgebra.scalarTrace: the scalar part of a multivector.

Main results

• CliffordAlgebra.scalarTrace_one, CliffordAlgebra.scalarTrace_ι and CliffordAlgebra.scalarTrace_ι_mul_ι: the values on 1, on a generator and on a product of two generators.
• CliffordAlgebra.scalarTrace_involute and CliffordAlgebra.scalarTrace_reverse: invariance under the grade involution and under reversion.
• CliffordAlgebra.scalarTrace_eq_zero_of_mem_evenOdd_one: the scalar part of an odd element is zero.
• CliffordAlgebra.scalarTrace_mul_comm: cyclicity, τ (x * y) = τ (y * x).
• CliffordAlgebra.scalarTrace_prod_map_ι_append_cons_eq_zero: a product of vectors with a factor orthogonal to all the others has scalar part zero.
• CliffordAlgebra.eq_smul_scalarTrace: for M spanned by pairwise orthogonal vectors, every cyclic functional invariant under the grade involution is f 1 • τ.
• CliffordAlgebra.trace_mulLeft_eq_finrank_mul_scalarTrace: the regular-trace formula for a finite free module spanned by pairwise orthogonal vectors, and its field form CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace, with no hypothesis on the form.
• CliffordAlgebra.scalarTrace_eq_of_algEquiv: over a field, the scalar part is preserved by algebra isomorphisms between Clifford algebras of finite-dimensional spaces.

Implementation notes

The invariances are transported from the exterior algebra, where the constant term ExteriorAlgebra.algebraMapInv is visibly invariant, along equivExterior; this needs that equivExterior intertwines the grade involutions and the reversions (CliffordAlgebra.equivExterior_involute, CliffordAlgebra.equivExterior_reverse). Cyclicity reduces, by induction on the left factor, to moving one generator ι Q m from the left of x to its right; Mathlib's CliffordAlgebra.changeForm_ι_mul and its right-handed counterpart CliffordAlgebra.changeForm_mul_ι turn the two scalar parts into the constant terms of a left and a right contraction, which agree by ExteriorAlgebra.algebraMapInv_contractRight.

The characterization needs no basis of the Clifford algebra: the products of the spanning orthogonal vectors span it (CliffordAlgebra.span_prod_map_ι_sublist_eq_top), and a cyclic functional invariant under the grade involution kills each nonempty such product, because the product is either odd or anticommutes with its first factor.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I.
• D. Grinberg, The Clifford algebra and the Chevalley map, for the contraction operators and the change of form.

noncomputable def CliffordAlgebra.scalarTrace {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) : CliffordAlgebra Q →ₗ[R] R

The scalar part of an element of a Clifford algebra: its degree-zero component under the module isomorphism CliffordAlgebra.equivExterior with the exterior algebra.

theorem CliffordAlgebra.scalarTrace_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : (scalarTrace Q) x = ExteriorAlgebra.algebraMapInv ((equivExterior Q) x)

The scalar part is the constant term of the image in the exterior algebra.

@[simp]

theorem CliffordAlgebra.scalarTrace_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (r : R) : (scalarTrace Q) ((algebraMap R (CliffordAlgebra Q)) r) = r

@[simp]

theorem CliffordAlgebra.scalarTrace_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} : (scalarTrace Q) 1 = 1

@[simp]

theorem CliffordAlgebra.scalarTrace_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (m : M) : (scalarTrace Q) ((ι Q) m) = 0

@[simp]

theorem CliffordAlgebra.scalarTrace_ι_mul_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (a b : M) : (scalarTrace Q) ((ι Q) a * (ι Q) b) = ((QuadraticMap.associated Q) a) b

The scalar part of a product of two generators is the symmetric bilinear form of Q.

@[simp]

theorem CliffordAlgebra.scalarTrace_involute {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) : (scalarTrace Q) (involute x) = (scalarTrace Q) x

The scalar part is invariant under the grade involution.

@[simp]

theorem CliffordAlgebra.scalarTrace_reverse {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) : (scalarTrace Q) (reverse x) = (scalarTrace Q) x

The scalar part is invariant under reversion.

theorem CliffordAlgebra.scalarTrace_eq_zero_of_mem_evenOdd_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x ∈ evenOdd Q 1) : (scalarTrace Q) x = 0

The scalar part of an odd element is zero.

theorem CliffordAlgebra.scalarTrace_mul_comm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} (x y : CliffordAlgebra Q) : (scalarTrace Q) (x * y) = (scalarTrace Q) (y * x)

Cyclicity of the scalar part: τ (x * y) = τ (y * x).

Uniqueness and the regular trace

theorem CliffordAlgebra.scalarTrace_prod_map_ι_append_cons_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {l₁ l₂ : List M} {a : M} (h : ∀ x ∈ l₁ ++ l₂, QuadraticMap.IsOrtho Q x a) : (scalarTrace Q) (List.map (⇑(ι Q)) (l₁ ++ a :: l₂)).prod = 0

A product with a factor orthogonal to all the others has scalar part zero: if the factor a of l₁ ++ a :: l₂ is orthogonal to every other factor, then τ vanishes on the product. Cyclicity moves l₁ behind the remaining factors, so that a comes first.

theorem CliffordAlgebra.eq_smul_scalarTrace {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) (f : CliffordAlgebra Q →ₗ[R] R) (hmul : ∀ (x y : CliffordAlgebra Q), f (x * y) = f (y * x)) (hinv : ∀ (x : CliffordAlgebra Q), f (involute x) = f x) : f = f 1 • scalarTrace Q

The scalar part is the unique normalized cyclic functional invariant under the grade involution, as soon as M is spanned by a list of pairwise orthogonal vectors: every such functional f is f 1 • scalarTrace Q. Both sides vanish on every product of at least one of the spanning vectors, and these products span the Clifford algebra.

theorem CliffordAlgebra.trace_mulLeft_eq_finrank_mul_scalarTrace {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} [Module.Free R M] [Module.Finite R M] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) (x : CliffordAlgebra Q) : (LinearMap.trace R (CliffordAlgebra Q)) (LinearMap.mulLeft R x) = ↑(Module.finrank R (CliffordAlgebra Q)) * (scalarTrace Q) x

The scalar part is the normalized trace of the left regular representation, for a finite free module spanned by a list of pairwise orthogonal vectors: trace (x * ·) = finrank R (CliffordAlgebra Q) * scalarTrace Q x.

theorem CliffordAlgebra.trace_mulLeft_eq_two_pow_mul_scalarTrace {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [FiniteDimensional K V] {Q : QuadraticForm K V} (x : CliffordAlgebra Q) : (LinearMap.trace K (CliffordAlgebra Q)) (LinearMap.mulLeft K x) = 2 ^ Module.finrank K V * (scalarTrace Q) x

The scalar part is the normalized regular trace: over a field in which 2 is invertible, for every quadratic form on a finite-dimensional space, trace (x * ·) = 2 ^ finrank K V * scalarTrace Q x. Every such form has an orthogonal basis, so CliffordAlgebra.trace_mulLeft_eq_finrank_mul_scalarTrace applies.

theorem CliffordAlgebra.scalarTrace_eq_inv_two_pow_mul_trace_mulLeft {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [FiniteDimensional K V] {Q : QuadraticForm K V} (x : CliffordAlgebra Q) : (scalarTrace Q) x = (2 ^ Module.finrank K V)⁻¹ * (LinearMap.trace K (CliffordAlgebra Q)) (LinearMap.mulLeft K x)

The scalar part as the normalized regular trace, scalarTrace Q x = (2 ^ finrank K V)⁻¹ * trace (x * ·).

theorem CliffordAlgebra.scalarTrace_eq_of_algEquiv {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] [FiniteDimensional K V] {Q : QuadraticForm K V} {V' : Type u_1} [AddCommGroup V'] [Module K V'] {Q' : QuadraticForm K V'} (e : CliffordAlgebra Q ≃ₐ[K] CliffordAlgebra Q') (x : CliffordAlgebra Q) : (scalarTrace Q') (e x) = (scalarTrace Q) x

The scalar part is invariant under algebra isomorphisms between Clifford algebras of finite-dimensional spaces: scalarTrace Q' (e x) = scalarTrace Q x. Both sides are normalized regular traces, and the two spaces have the same dimension since their Clifford algebras do. The target space is automatically finite-dimensional, since it embeds in its Clifford algebra.