Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.VolumeElement

The volume element of a Clifford algebra #

The volume element (or pseudoscalar) of a quadratic space is the ordered Clifford product ι Q v₁ * ⋯ * ι Q vₙ of an orthogonal basis. This file proves the facts that make it useful: how it commutes past a vector, how reversal acts on it, what its square is, and, over a field, that it moves each of its anisotropic factors out of the vectors once there are at least three of them and evenly many.

The ordered product is spelled (l.map (ι Q)).prod for a list l of vectors, the spelling Mathlib already uses for it (CliffordAlgebra.involute_prod_map_ι, CliffordAlgebra.reverse_prod_map_ι) and the one the sibling file Filtration.lean uses (CliffordAlgebra.prod_map_ι_mem_filtration); the results below are named prod_map_ι_* to match. Orthogonality is a hypothesis of each result rather than part of the object, so the name "volume element" is reserved for the informal reading.

Both facts come from the single relation ι Q a * ι Q b = -(ι Q b * ι Q a) for orthogonal a and b. Pushing a vector ι Q m from one side of a product of n mutually orthogonal vectors to the other costs a sign (-1) ^ n when m is orthogonal to every factor (CliffordAlgebra.prod_map_ι_mul_ι_of_forall_isOrtho). When m is instead one of the factors, one of the n transpositions is a vector past itself, which is free, so the cost is (-1) ^ (n - 1). That sign does not depend on m, and the condition is linear in m, so it propagates from the factors to their span (CliffordAlgebra.prod_map_ι_mul_ι_of_mem_span).

This is the even/odd dichotomy of the Clifford algebra as seen from the volume element. If there are oddly many factors, the volume element commutes with every generator coming from their span (CliffordAlgebra.prod_map_ι_mul_ι_of_odd_length), so once the factors span M it is central (CliffordAlgebra.prod_map_ι_mem_center_of_odd_length); if there are evenly many, it anticommutes with those generators instead (CliffordAlgebra.prod_map_ι_mul_ι_of_even_length). Centrality is all the odd case claims: under these hypotheses the volume element may well be a scalar already, and is 0 as soon as one of its factors is. That it is a further central element, and that the centre is then exactly a rank-two algebra rather than the scalars, is not proved here and needs hypotheses this file does not make — a nondegenerate form over a field away from characteristic two, with the list an orthogonal basis. For Q = 0 on R ^ 3 the Clifford algebra is the exterior algebra and its centre is much larger instead. The odd-dimensional splitting does run on the volume element: TauCeti/LinearAlgebra/CliffordAlgebra/OddSplitting.lean splits the Clifford algebra as two copies of its even subalgebra along a central odd square root of one, and CliffordAlgebra.equivEvenProdOfOddLength feeds it the volume element of an orthogonal spanning list of odd length, rescaled so that the square below is 1. What remains open there is the identification of even Q with a matrix algebra, for which TauCeti/RepresentationTheory/Spin/Structure.lean proves the even-dimensional structure theorem.

The square is a scalar, ω * ω = (-1) ^ (n.choose 2) * Q v₁ ⋯ Q vₙ (CliffordAlgebra.prod_map_ι_sq_scalar), the sign counting the n.choose 2 transpositions needed to interleave two copies of the product. So the volume element is a unit as soon as the product of the values Q vᵢ is a unit — over a field, whenever no factor is isotropic. That last statement (CliffordAlgebra.isUnit_prod_map_ι) needs no orthogonality at all, each factor being a unit already because its square Q vᵢ is.

Nothing here needs 2 to be invertible, a field, or any finiteness. Beyond pairwise orthogonality of the list — which the unit statement does not even ask for — the only hypotheses are the ones each statement names: that the vector crossing the product lies in the span of the list (or that the list spans M, for the centrality statement), and, for the unit statement, that the product of the values Q vᵢ is a unit.

Main results #

References #

Moving a vector across the volume element #

source
theorem CliffordAlgebra.prod_map_ι_mul_ι_of_forall_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} {m : M} (h : ∀ x ∈ l, QuadraticMap.IsOrtho Q x m) :
(List.map (⇑(ι Q)) l).prod * (ι Q) m = (-1) ^ l.length • ((ι Q) m * (List.map (⇑(ι Q)) l).prod)

A vector orthogonal to every factor crosses the volume element at the cost of (-1) ^ n, n the number of factors: each transposition with a factor contributes one sign.

source
theorem CliffordAlgebra.prod_map_ι_mul_ι_of_mem_span {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) {m : M} (hm : m ∈ Submodule.span R {x : M | x ∈ l}) :
(List.map (⇑(ι Q)) l).prod * (ι Q) m = (-1) ^ (l.length - 1) • ((ι Q) m * (List.map (⇑(ι Q)) l).prod)

The crossing sign propagates from the factors to their span. The sign (-1) ^ (n - 1) does not depend on the vector, and both sides of the crossing identity are linear in it, so the identity holds on the whole span of the list — in particular on all of M when the list spans.

The even/odd dichotomy #

source
theorem CliffordAlgebra.prod_map_ι_mul_ι_of_odd_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) {m : M} (hm : m ∈ Submodule.span R {x : M | x ∈ l}) :
(List.map (⇑(ι Q)) l).prod * (ι Q) m = (ι Q) m * (List.map (⇑(ι Q)) l).prod

The volume element of an odd number of pairwise orthogonal vectors commutes with every generator coming from their span, the crossing sign (-1) ^ (n - 1) now being 1.

This is the odd half of the dichotomy, in the same span-relative form as its even counterpart prod_map_ι_mul_ι_of_even_length; prod_map_ι_mem_center_of_odd_length is the case of a spanning list, where commuting with the generators upgrades to centrality.

source
theorem CliffordAlgebra.prod_map_ι_mem_center_of_odd_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) :
(List.map (⇑(ι Q)) l).prod ∈ Subalgebra.center R (CliffordAlgebra Q)

The volume element of an odd number of pairwise orthogonal vectors spanning M is central.

Crossing a generator costs (-1) ^ (n - 1), and n - 1 is even, so the volume element commutes with every generator; the generators generate the algebra, so it commutes with everything.

Centrality is all that is claimed. Under these hypotheses the volume element may already be a scalar, and is 0 as soon as one of its factors is; it is the element expected to generate the centre beyond the scalars in the odd-dimensional case, but that expectation rests on nondegeneracy hypotheses made nowhere in this file.

source
theorem CliffordAlgebra.prod_map_ι_mul_ι_of_even_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) {m : M} (hm : m ∈ Submodule.span R {x : M | x ∈ l}) :
(List.map (⇑(ι Q)) l).prod * (ι Q) m = -((ι Q) m * (List.map (⇑(ι Q)) l).prod)

The volume element of an even number of pairwise orthogonal vectors anticommutes with every generator coming from their span, the crossing sign (-1) ^ (n - 1) now being -1.

Anticommuting does not by itself rule out centrality: it says exactly that 2 • (ι Q m * ω) = 0 whenever ω is central, which happens in characteristic two, and also whenever ω annihilates the generators, as it does in an exterior algebra.

The square of the volume element #

source
@[simp]
theorem CliffordAlgebra.prod_map_ι_sq_scalar {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) :
(List.map (⇑(ι Q)) l).prod * (List.map (⇑(ι Q)) l).prod = (algebraMap R (CliffordAlgebra Q)) ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod)

The square of the volume element of a pairwise orthogonal list is a scalar, (-1) ^ (n.choose 2) * Q v₁ ⋯ Q vₙ: interleaving the two copies of the product takes n.choose 2 transpositions, and each pair of equal adjacent factors collapses to Q vᵢ.

source
@[simp]
theorem CliffordAlgebra.reverse_prod_map_ι_of_pairwise_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) :
reverse (List.map (⇑(ι Q)) l).prod = (-1) ^ l.length.choose 2 • (List.map (⇑(ι Q)) l).prod

Reversal multiplies the volume element of a pairwise orthogonal list by (-1) ^ (n.choose 2), the same sign as in its square CliffordAlgebra.prod_map_ι_sq_scalar. In particular the volume element is reverse-symmetric for n ≡ 0, 1 (mod 4) and reverse-antisymmetric for n ≡ 2, 3 (mod 4).

source
theorem CliffordAlgebra.ι_mul_ι_mul_self_of_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {a b : M} (h : QuadraticMap.IsOrtho Q a b) :
(ι Q) a * (ι Q) b * ((ι Q) a * (ι Q) b) = -(algebraMap R (CliffordAlgebra Q)) (Q a * Q b)

The square of the product of two orthogonal generators is the scalar -(Q a * Q b). This is CliffordAlgebra.prod_map_ι_sq_scalar at the two-element list [a, b], whose sign (-1) ^ Nat.choose 2 2 is the displayed minus. In particular the square vanishes as soon as one of the two vectors is isotropic.

source
theorem CliffordAlgebra.isUnit_prod_map_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (h : IsUnit (List.map (⇑Q) l).prod) :
IsUnit (List.map (⇑(ι Q)) l).prod

An ordered product of generators is a unit as soon as the product of the values Q vᵢ is.

No orthogonality is needed: each Q vᵢ divides the unit ∏ᵢ Q vᵢ, hence is a unit, so each factor ι Q vᵢ is a unit by CliffordAlgebra.isUnit_ι_of_isUnit and so is their product. For a pairwise orthogonal list this is the volume element, and prod_map_ι_sq_scalar identifies its square as that product up to sign; in particular the volume element of an orthogonal basis of a quadratic space over a field is a unit whenever no basis vector is isotropic.

The volume element moves its factors out of the vectors #

The scalar square of an anisotropic volume element #

source
theorem CliffordAlgebra.neg_one_pow_choose_two_mul_prod_map_ne_zero {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {l : List V} (haniso : ∀ v ∈ l, Q v ≠ 0) :
(-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod ≠ 0

Over a field, the scalar square (-1) ^ (n.choose 2) * Q v₁ ⋯ Q vₙ of the volume element (CliffordAlgebra.prod_map_ι_sq_scalar) is nonzero as soon as no member of the list is isotropic.

source
theorem CliffordAlgebra.prod_map_ι_mul_ι_notMem_range_ι {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Even l.length) (h3 : 3 ≤ l.length) (haniso : ∀ v ∈ l, Q v ≠ 0) {v : V} (hv : v ∈ l) :
(List.map (⇑(ι Q)) l).prod * (ι Q) v ∉ (ι Q).range

The volume element of an orthogonal anisotropic list of even length at least three moves each member of the list out of the vectors. Length two is genuinely excluded: there the volume element sends each member to a multiple of the other.