The normalized complex volume element of an oriented Euclidean space

Let V be an oriented real inner product space of dimension n and Q a quadratic form on V. For the geometric convention Q v = -‖v‖², so that c(v) c(w) + c(w) c(v) = -2 ⟪v, w⟫, the normalized complex volume element is

Γ = i ^ ⌊(n + 1) / 2⌋ c(e₁) ⋯ c(eₙ)

in the complexified Clifford algebra Cℓ(ℂ ⊗ V, Q_ℂ), for any positively oriented orthonormal basis e. It is defined without a frame, as i ^ ⌊(n + 1) / 2⌋ times the image of the real volume element CliffordAlgebra.volumeElement Q o, so the frame formula CliffordAlgebra.complexVolume_eq is its independence under orientation-preserving orthonormal changes of frame, and reversing the orientation changes its sign.

In even dimension n = 2ℓ this is Γ = i ^ ℓ c(e₁) ⋯ c(e₂ₗ), the chirality operator: it anticommutes with every vector, so its ±1 eigenspaces in a Clifford module are exchanged by Clifford multiplication, and conjugation by Γ is the grade involution. In odd dimension n = 2ℓ + 1 it is ω_ℂ = i ^ (ℓ + 1) c(e₁) ⋯ c(eₙ), a central element whose ±1 eigenspaces separate the two irreducible Clifford modules. The power of i is chosen so that Γ squares to 1 and is fixed by the conjugate-linear Clifford involution CliffordAlgebra.conjStar, so that it acts as a self-adjoint involution in every *-representation. The complex-linear Clifford conjugation star instead multiplies it by (-1) ^ ⌊(n + 1) / 2⌋. In rank zero, Γ is 1 for the positive orientation and -1 for the negative one.

Main definitions

• CliffordAlgebra.complexVolume Q o: the normalized complex volume element Γ of CliffordAlgebra (Q.baseChange ℂ).

Main results

• CliffordAlgebra.complexVolume_eq: Γ = i ^ ⌊(n + 1) / 2⌋ c(e₁) ⋯ c(eₙ) for every positively oriented orthonormal basis e that is orthogonal for Q, and CliffordAlgebra.complexVolume_eq_prod_pairs: in dimension 2ℓ it groups as Γ = i ^ ℓ (c(e₁) c(e₂)) ⋯ (c(e₂ℓ₋₁) c(e₂ℓ)), while CliffordAlgebra.complexVolume_eq_prod_pairs_mul: in dimension 2ℓ + 1 it groups as ω_ℂ = i ^ (ℓ + 1) (c(e₁) c(e₂)) ⋯ (c(e₂ℓ₋₁) c(e₂ℓ)) c(e₂ℓ₊₁).
• CliffordAlgebra.ofBaseChangeAux_volumeElement: conversely, the real volume element is (-i) ^ ⌊(n + 1) / 2⌋ Γ.
• CliffordAlgebra.complexVolume_neg_orientation: reversing the orientation negates Γ, and CliffordAlgebra.complexVolume_positiveOrientation: in rank zero, Γ = 1.
• CliffordAlgebra.map_complexVolume: the complexification of an isometry of quadratic forms that also preserves the norms carries Γ to Γ for the transported orientation.
• CliffordAlgebra.complexVolume_mul_self: Γ² = 1 for Q v = -‖v‖².
• CliffordAlgebra.complexVolume_smul_complexVolume_smul, CliffordAlgebra.lsmul_complexVolume_involutive: Γ acts as an involution on every module.
• CliffordAlgebra.conjStar_complexVolume: Γ is fixed by the conjugate-linear Clifford involution, while CliffordAlgebra.star_complexVolume computes the complex-linear Clifford conjugation star Γ = (-1) ^ ⌊(n + 1) / 2⌋ Γ; in dimension 2ℓ this is (-1) ^ ℓ Γ.
• CliffordAlgebra.complexVolume_mul_eq_involute_mul: in even dimension, Γ x = involute x Γ; hence Γ anticommutes with odd elements (CliffordAlgebra.complexVolume_mul_of_mem_odd), in particular with vectors (CliffordAlgebra.complexVolume_mul_ι_of_even). For Q v = -‖v‖², conjugation by Γ is the grade involution (CliffordAlgebra.complexVolume_mul_mul_complexVolume).
• CliffordAlgebra.complexVolume_mem_center: in odd dimension, Γ is central.
• CliffordAlgebra.commute_complexVolume_of_mem_even: in every dimension, Γ commutes with even elements.

Only the statements involving Γ² assume Q v = -‖v‖²; the others hold for every Q.

References

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

noncomputable def CliffordAlgebra.complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] (Q : QuadraticForm ℝ V) (o : Orientation ℝ V (Fin n)) : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)

The normalized complex volume element Γ = i ^ ⌊(n + 1) / 2⌋ c(e₁) ⋯ c(eₙ) of the complexified Clifford algebra of an oriented real inner product space of dimension n, for any positively oriented orthonormal basis e that is orthogonal for Q (CliffordAlgebra.complexVolume_eq). It is fixed by CliffordAlgebra.conjStar; in even dimension it anticommutes with every vector, and in odd dimension it is central. For Q v = -‖v‖² it squares to 1, so in even dimension it is the chirality operator.

theorem CliffordAlgebra.complexVolume_def {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] (Q : QuadraticForm ℝ V) (o : Orientation ℝ V (Fin n)) : complexVolume Q o = Complex.I ^ ((n + 1) / 2) • (ofBaseChangeAux ℂ Q) (volumeElement Q o)

Unfolding lemma for CliffordAlgebra.complexVolume.

theorem CliffordAlgebra.ofBaseChangeAux_volumeElement {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : (ofBaseChangeAux ℂ Q) (volumeElement Q o) = (-Complex.I) ^ ((n + 1) / 2) • complexVolume Q o

The real volume element is (-i) ^ ⌊(n + 1) / 2⌋ Γ in the complexified Clifford algebra; in dimension two it is -i Γ.

@[simp]

theorem CliffordAlgebra.complexVolume_neg_orientation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : complexVolume Q (-o) = -complexVolume Q o

Reversing the orientation negates the normalized complex volume element.

theorem CliffordAlgebra.complexVolume_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (b : OrthonormalBasis (Fin n) ℝ V) (hb : b.toBasis.orientation = o) (hQb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b.toBasis) : complexVolume Q o = Complex.I ^ ((n + 1) / 2) • (List.map (fun (v : V) => (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) (List.map (⇑b) (List.finRange n))).prod

Frame independence of Γ: Γ = i ^ ⌊(n + 1) / 2⌋ c(e₁) ⋯ c(eₙ) for every positively oriented orthonormal basis e that is orthogonal for Q, for instance for Q v = -‖v‖² (OrthonormalBasis.isOrthoᵢ_associated).

theorem CliffordAlgebra.complexVolume_eq_prod_pairs {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} {ℓ : ℕ} [Fact (Module.finrank ℝ V = 2 * ℓ)] {o : Orientation ℝ V (Fin (2 * ℓ))} (b : OrthonormalBasis (Fin (2 * ℓ)) ℝ V) (hb : b.toBasis.orientation = o) (hQb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b.toBasis) : complexVolume Q o = Complex.I ^ ℓ • (List.ofFn fun (k : Fin ℓ) => (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] b ⟨2 * ↑k, ⋯⟩) * (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] b ⟨2 * ↑k + 1, ⋯⟩)).prod

Γ as a product of adjacent pairs: in dimension 2ℓ, Γ = i ^ ℓ (c(e₁) c(e₂)) ⋯ (c(e₂ℓ₋₁) c(e₂ℓ)) for every positively oriented orthonormal basis e that is orthogonal for Q.

theorem CliffordAlgebra.complexVolume_eq_prod_pairs_mul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} {ℓ : ℕ} [Fact (Module.finrank ℝ V = 2 * ℓ + 1)] {o : Orientation ℝ V (Fin (2 * ℓ + 1))} (b : OrthonormalBasis (Fin (2 * ℓ + 1)) ℝ V) (hb : b.toBasis.orientation = o) (hQb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b.toBasis) : complexVolume Q o = Complex.I ^ (ℓ + 1) • ((List.ofFn fun (k : Fin ℓ) => (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] b ⟨2 * ↑k, ⋯⟩) * (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] b ⟨2 * ↑k + 1, ⋯⟩)).prod * (ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] b (Fin.last (2 * ℓ))))

ω_ℂ as a product of adjacent pairs and a last vector: in dimension 2ℓ + 1, ω_ℂ = i ^ (ℓ + 1) (c(e₁) c(e₂)) ⋯ (c(e₂ℓ₋₁) c(e₂ℓ)) c(e₂ℓ₊₁) for every positively oriented orthonormal basis e that is orthogonal for Q.

@[simp]

theorem CliffordAlgebra.complexVolume_positiveOrientation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} [Fact (Module.finrank ℝ V = 0)] : complexVolume Q positiveOrientation = 1

The normalized complex volume element in rank zero: for the positive orientation of a zero-dimensional space, Γ = 1. By CliffordAlgebra.complexVolume_neg_orientation, the negative orientation gives Γ = -1.

theorem CliffordAlgebra.map_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) {V' : Type u_2} [NormedAddCommGroup V'] [InnerProductSpace ℝ V'] [FiniteDimensional ℝ V'] [Fact (Module.finrank ℝ V' = n)] {Q' : QuadraticForm ℝ V'} (e : QuadraticMap.IsometryEquiv Q Q') (he : ∀ (v : V), ‖e v‖ = ‖v‖) : (map (e.toIsometry.baseChange ℂ)) (complexVolume Q o) = complexVolume Q' ((Orientation.map (Fin n) e.toLinearEquiv) o)

Naturality of Γ: the complexification of an isometric equivalence e of the quadratic forms that also preserves the norms carries Γ for o to Γ for the transported orientation. In particular an orientation-preserving isometry of V fixing Q fixes Γ, while an orientation-reversing one negates it (CliffordAlgebra.complexVolume_neg_orientation).

@[simp]

theorem CliffordAlgebra.involute_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : involute (complexVolume Q o) = (-1) ^ n • complexVolume Q o

The grade involution multiplies Γ by (-1) ^ n.

@[simp]

theorem CliffordAlgebra.reverse_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : reverse (complexVolume Q o) = (-1) ^ (n / 2) • complexVolume Q o

Reversal multiplies Γ by (-1) ^ ⌊n / 2⌋.

@[simp]

theorem CliffordAlgebra.star_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : star (complexVolume Q o) = (-1) ^ ((n + 1) / 2) • complexVolume Q o

Complex-linear Clifford conjugation multiplies Γ by (-1) ^ ⌊(n + 1) / 2⌋; in dimension 2ℓ this is star Γ = (-1) ^ ℓ Γ.

@[simp]

theorem CliffordAlgebra.complexConj_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : (complexConj Q) (complexVolume Q o) = (-1) ^ ((n + 1) / 2) • complexVolume Q o

Complex conjugation of the coefficients multiplies Γ by (-1) ^ ⌊(n + 1) / 2⌋.

@[simp]

theorem CliffordAlgebra.conjStar_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) : (conjStar Q) (complexVolume Q o) = complexVolume Q o

Γ is self-adjoint: it is fixed by the conjugate-linear Clifford involution CliffordAlgebra.conjStar, so it acts self-adjointly in every *-representation.

theorem CliffordAlgebra.complexVolume_mul_ι_of_even {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hn : Even n) (w : TensorProduct ℝ ℂ V) : complexVolume Q o * (ι (QuadraticForm.baseChange ℂ Q)) w = -((ι (QuadraticForm.baseChange ℂ Q)) w * complexVolume Q o)

In even dimension Γ anticommutes with every vector: Γ c(w) = -c(w) Γ.

theorem CliffordAlgebra.complexVolume_mul_eq_involute_mul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hn : Even n) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : complexVolume Q o * x = involute x * complexVolume Q o

In even dimension Γ intertwines the grade involution: Γ x = involute x Γ.

theorem CliffordAlgebra.complexVolume_mul_of_mem_odd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hn : Even n) {x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)} (hx : x ∈ evenOdd (QuadraticForm.baseChange ℂ Q) 1) : complexVolume Q o * x = -(x * complexVolume Q o)

In even dimension Γ anticommutes with every odd element.

theorem CliffordAlgebra.complexVolume_mul_ι_of_odd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hn : Odd n) (w : TensorProduct ℝ ℂ V) : complexVolume Q o * (ι (QuadraticForm.baseChange ℂ Q)) w = (ι (QuadraticForm.baseChange ℂ Q)) w * complexVolume Q o

In odd dimension Γ commutes with every vector.

theorem CliffordAlgebra.complexVolume_mem_center {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hn : Odd n) : complexVolume Q o ∈ Subalgebra.center ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q))

In odd dimension Γ is central.

theorem CliffordAlgebra.commute_complexVolume_of_mem_even {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) {x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)} (hx : x ∈ evenOdd (QuadraticForm.baseChange ℂ Q) 0) : Commute (complexVolume Q o) x

Γ commutes with every even element, in every dimension: in even dimension Γ intertwines the grade involution, and in odd dimension Γ is central.

@[simp]

theorem CliffordAlgebra.complexVolume_mul_self {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) : complexVolume Q o * complexVolume Q o = 1

Γ is an involution: Γ² = 1.

theorem CliffordAlgebra.complexVolume_smul_complexVolume_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {M : Type u_2} [MulAction (CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) M] (ψ : M) : complexVolume Q o • complexVolume Q o • ψ = ψ

Γ acts as an involution on every module: Γ • Γ • ψ = ψ.

theorem CliffordAlgebra.lsmul_complexVolume_involutive {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {M : Type u_2} [AddCommGroup M] [Module ℂ M] [Module (CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) M] [IsScalarTower ℂ (CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) M] : Function.Involutive ⇑((Algebra.lsmul ℂ ℂ M) (complexVolume Q o))

Multiplication by Γ is an involution of every module.

theorem CliffordAlgebra.complexVolume_mul_mul_complexVolume {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hn : Even n) (x : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : complexVolume Q o * x * complexVolume Q o = involute x

In even dimension, conjugation by Γ is the grade involution: Γ x Γ = involute x.