The 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. The volume element CliffordAlgebra.volumeElement Q o is the quantization, under CliffordAlgebra.equivExterior, of the unit volume element of ⋀ⁿ V. It is defined without a frame. For every positively oriented orthonormal basis e it is the top Clifford basis vector CliffordAlgebra.basis Q e univ, the quantization of e₁ ∧ ⋯ ∧ eₙ; when e is moreover orthogonal for Q, for instance for the geometric form Q v = -‖v‖², this is the Clifford product c(e₁) ⋯ c(eₙ) (CliffordAlgebra.volumeElement_eq). That every such frame gives the same product is the independence of the volume element under orientation-preserving orthonormal changes of frame; reversing the orientation changes its sign.

For an arbitrary quadratic form the volume element is a multiple of the top Clifford basis vector of every basis (CliffordAlgebra.volumeElement_eq_inv_smul_basis), hence of the ordered product of a Q-orthogonal basis. The commutation rules of such products in TauCeti/LinearAlgebra/CliffordAlgebra/VolumeElement/Basic.lean then show that in even dimension it anticommutes with every vector and in odd dimension it commutes with every vector.

The volume element is the real input of the normalized complex volume element of TauCeti/LinearAlgebra/CliffordAlgebra/VolumeElement/Complex.lean, and in dimension four it is minus the chirality element CliffordAlgebra.chirality of TauCeti/LinearAlgebra/CliffordAlgebra/Chirality.lean.

Main definitions

• CliffordAlgebra.volumeElement Q o: the volume element of CliffordAlgebra Q.

Main results

• CliffordAlgebra.volumeElement_eq: the volume element is c(e₁) ⋯ c(eₙ) for every positively oriented orthonormal basis e that is orthogonal for Q.
• CliffordAlgebra.volumeElement_neg_orientation: reversing the orientation negates it.
• CliffordAlgebra.map_volumeElement: an isometry of quadratic forms that also preserves the norms carries the volume element to that of the transported orientation.
• CliffordAlgebra.involute_volumeElement, CliffordAlgebra.reverse_volumeElement and CliffordAlgebra.star_volumeElement: the grade involution, reversal and Clifford conjugation multiply it by (-1) ^ n, (-1) ^ ⌊n / 2⌋ and (-1) ^ ⌊(n + 1) / 2⌋.
• CliffordAlgebra.volumeElement_mul_ι_of_even and CliffordAlgebra.volumeElement_mul_ι_of_odd: it anticommutes with every vector in even dimension and commutes with every vector in odd dimension.
• CliffordAlgebra.volumeElement_mul_eq_involute_mul: in even dimension the raw volume intertwines the grade involution.
• CliffordAlgebra.volumeElement_mul_self: for Q v = -‖v‖² it squares to (-1) ^ ⌊(n + 1) / 2⌋.
• CliffordAlgebra.algebraMap_add_smul_volumeElement_inj: in positive dimension, r + s · vol determines r and s. When the volume element squares to -1, for instance for an oriented plane with Q v = -‖v‖², the elements r + s · vol multiply as the complex numbers r + s i (CliffordAlgebra.algebraMap_add_smul_volumeElement_mul), with spinor norm r² + s² (CliffordAlgebra.algebraMap_add_smul_volumeElement_mul_star_self).
• CliffordAlgebra.volumeElement_eq_ι_mul_ι: in dimension two the volume element is c(e₀) c(e₁).
• CliffordAlgebra.involute_eq_volumeElement_mul_mul: in rank divisible by four, left and right multiplication by the negative-metric raw volume recover parity.
• CliffordAlgebra.volumeElement_mul_basis: for Q v = -‖v‖² it sends the Clifford basis vector e_s of a positively oriented orthonormal basis to a signed e_{sᶜ}.

References

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

noncomputable def CliffordAlgebra.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)) : CliffordAlgebra Q

The volume element of the Clifford algebra of an oriented real inner product space: the quantization of the unit volume element of the top exterior power. It is the top Clifford basis vector of every positively oriented orthonormal basis e (CliffordAlgebra.volumeElement_eq_basis), and the product c(e₁) ⋯ c(eₙ) when e is moreover orthogonal for Q (CliffordAlgebra.volumeElement_eq).

theorem CliffordAlgebra.volumeElement_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)) : volumeElement Q o = (equivExterior Q).symm ↑(o.volumeEquiv.symm 1)

Unfolding lemma for CliffordAlgebra.volumeElement.

theorem CliffordAlgebra.volumeElement_eq_basis {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) : volumeElement Q o = (basis Q b.toBasis) Finset.univ

In terms of the Clifford basis of a positively oriented orthonormal basis e, the volume element is the basis vector indexed by all of Fin n.

@[simp]

theorem CliffordAlgebra.volumeElement_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)) : volumeElement Q (-o) = -volumeElement Q o

Reversing the orientation negates the volume element.

theorem CliffordAlgebra.map_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)) {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) (volumeElement Q o) = volumeElement Q' ((Orientation.map (Fin n) e.toLinearEquiv) o)

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

@[simp]

theorem CliffordAlgebra.involute_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)) : involute (volumeElement Q o) = (-1) ^ n • volumeElement Q o

The volume element is homogeneous of degree n: the grade involution multiplies it by (-1) ^ n.

@[simp]

theorem CliffordAlgebra.reverse_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)) : reverse (volumeElement Q o) = (-1) ^ (n / 2) • volumeElement Q o

Reversal multiplies the volume element by (-1) ^ ⌊n / 2⌋, the sign of the order-reversing permutation of n letters.

@[simp]

theorem CliffordAlgebra.star_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)) : star (volumeElement Q o) = (-1) ^ ((n + 1) / 2) • volumeElement Q o

Clifford conjugation multiplies the volume element by (-1) ^ ⌊(n + 1) / 2⌋.

theorem CliffordAlgebra.volumeElement_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) : volumeElement Q o = (List.map (⇑(ι Q)) (List.map (⇑b) (List.finRange n))).prod

Frame formula for the volume element: volumeElement Q o = 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.volumeElement_eq_inv_smul_basis {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {n : ℕ} [Fact (Module.finrank ℝ V = n)] {Q : QuadraticForm ℝ V} (o : Orientation ℝ V (Fin n)) {ι : Type u_2} [Fintype ι] [LinearOrder ι] (f : Module.Basis ι ℝ V) : volumeElement Q o = (o.volumeEquiv f.topVector)⁻¹ • (basis Q f) Finset.univ

The volume element is a multiple of the top Clifford basis vector of every basis f: the scalar is the inverse of the volume of f₁ ∧ ⋯ ∧ fₙ. For a positively oriented orthonormal basis this scalar is 1 (CliffordAlgebra.volumeElement_eq_basis).

theorem CliffordAlgebra.volumeElement_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) (v : V) : volumeElement Q o * (ι Q) v = -((ι Q) v * volumeElement Q o)

In even dimension the volume element anticommutes with every vector.

theorem CliffordAlgebra.volumeElement_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 Q) : volumeElement Q o * x = involute x * volumeElement Q o

In even dimension the raw volume element intertwines the grade involution: ω x = involute x * ω.

theorem CliffordAlgebra.volumeElement_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) (v : V) : volumeElement Q o * (ι Q) v = (ι Q) v * volumeElement Q o

In odd dimension the volume element commutes with every vector.

@[simp]

theorem CliffordAlgebra.volumeElement_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) : volumeElement Q o * volumeElement Q o = (-1) ^ ((n + 1) / 2)

For Q v = -‖v‖², the volume element squares to (-1) ^ ⌊(n + 1) / 2⌋.

theorem CliffordAlgebra.algebraMap_add_smul_volumeElement_inj {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 : n ≠ 0) {r s r' s' : ℝ} : (algebraMap ℝ (CliffordAlgebra Q)) r + s • volumeElement Q o = (algebraMap ℝ (CliffordAlgebra Q)) r' + s' • volumeElement Q o ↔ r = r' ∧ s = s'

The coordinates of r + s · vol: in positive dimension, the scalar r and the volume coefficient s of r + s · vol are determined by the element.

theorem CliffordAlgebra.algebraMap_add_smul_volumeElement_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)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hn : Odd ((n + 1) / 2)) (a b c d : ℝ) : ((algebraMap ℝ (CliffordAlgebra Q)) a + b • volumeElement Q o) * ((algebraMap ℝ (CliffordAlgebra Q)) c + d • volumeElement Q o) = (algebraMap ℝ (CliffordAlgebra Q)) (a * c - b * d) + (a * d + b * c) • volumeElement Q o

For Q v = -‖v‖² in a dimension n with ⌊(n + 1) / 2⌋ odd, for instance n = 2, the volume element squares to -1, so the elements r + s · vol multiply as the complex numbers r + s i.

theorem CliffordAlgebra.algebraMap_add_smul_volumeElement_mul_star_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) (hn : Odd ((n + 1) / 2)) (r s : ℝ) : ((algebraMap ℝ (CliffordAlgebra Q)) r + s • volumeElement Q o) * star ((algebraMap ℝ (CliffordAlgebra Q)) r + s • volumeElement Q o) = (algebraMap ℝ (CliffordAlgebra Q)) (r ^ 2 + s ^ 2)

For Q v = -‖v‖² in a dimension n with ⌊(n + 1) / 2⌋ odd, for instance n = 2, the spinor norm x x⋆ of x = r + s · vol is the scalar r² + s².

theorem CliffordAlgebra.volumeElement_eq_ι_mul_ι {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) : volumeElement Q o = (ι Q) (b 0) * (ι Q) (b 1)

Frame formula in dimension two: the volume element of an oriented plane is c(e₀) c(e₁) for every positively oriented orthonormal basis e that is orthogonal for Q.

theorem CliffordAlgebra.involute_eq_volumeElement_mul_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)) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hn : 4 ∣ n) (s : CliffordAlgebra Q) : involute s = volumeElement Q o * s * volumeElement Q o

In rank divisible by four, parity is left times right raw negative volume. No orientation choice remains on the right, since reversing it changes both factors' signs.

theorem CliffordAlgebra.volumeElement_mul_basis {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) (b : OrthonormalBasis (Fin n) ℝ V) (hb : b.toBasis.orientation = o) {k l : ℕ} (hcard : l + k = Fintype.card (Fin n)) (s : ↑(Set.powersetCard (Fin n) k)) : volumeElement Q o * (basis Q b.toBasis) ↑s = ((-1) ^ (k + 1).choose 2 * ↑↑(Set.powersetCard.sign ((Set.powersetCard.compl hcard) s))) • (basis Q b.toBasis) ↑((Set.powersetCard.compl hcard) s)

For Q v = -‖v‖², the Clifford product of the volume element with the basis vector e_s of a positively oriented orthonormal basis is the signed basis vector (-1) ^ ((k + 1).choose 2) ε(sᶜ) e_{sᶜ}, where ε(sᶜ) is the shuffle sign of the complement.