The ordered-product basis of an orthogonal basis, and the trace pairing

Let b be a basis of M, indexed by a linearly ordered type I, and let Q be a quadratic form on M over a commutative ring in which 2 is invertible. The basis CliffordAlgebra.basis Q b of CliffordAlgebra Q, indexed by the finite subsets of I, is transported from the exterior-algebra basis along CliffordAlgebra.equivExterior, which corrects a product of generators by lower-order contractions. When b is orthogonal for Q these corrections all vanish, and the basis vector indexed by s is the ordered product e_s = ι Q (b i₁) * ⋯ * ι Q (b iₖ) for s.sort = [i₁, …, iₖ]. So the ordered products of an orthogonal basis form a basis of the Clifford algebra, for every Q, degenerate or not.

The scalar part τ = CliffordAlgebra.scalarTrace Q makes these basis vectors orthogonal for the pairing (x, y) ↦ τ (reverse x * y):

τ (reverse e_s * e_t) = if s = t then ∏ i ∈ s, Q (b i) else 0.

For s = t the product reverse e_s * e_s collapses to the scalar ∏ i ∈ s, Q (b i). For s ≠ t some index lies in exactly one of s and t, so its basis vector occurs exactly once in the product and is orthogonal to every other factor, and the scalar part of such a product vanishes. Expanding in the basis then computes the pairing of arbitrary elements coordinatewise, τ (reverse x * y) = ∑ₛ xₛ * (∏ i ∈ s, Q (b i)) * yₛ. Over an ordered ring this gives positivity of the pairing: if every Q (b i) is nonnegative then τ (reverse x * x) ≥ 0, and if every Q (b i) is positive then τ (reverse x * x) = 0 only for x = 0.

Main results

• CliffordAlgebra.basis_repr_empty: for every basis, the coordinate at the empty index set is the scalar part.
• CliffordAlgebra.basis_eq_prod_map_sort: for an orthogonal basis, the basis vector indexed by s is the product of the generators of s in increasing order.
• CliffordAlgebra.exists_basis_eq_ι_mul: for an orthogonal basis, a two-element index set s can be written {k, l} so that the basis vector indexed by s is ι Q (b k) * ι Q (b l).
• CliffordAlgebra.involute_basis and CliffordAlgebra.basis_repr_involute: for an orthogonal basis, the grade involution acts on e_s and on the coordinate at s by (-1) ^ |s|.
• CliffordAlgebra.basis_mul_basis_of_disjoint: for an orthogonal basis, basis vectors with disjoint index sets multiply to the signed basis vector of the union.
• CliffordAlgebra.basis_insert_of_forall_lt: for an orthogonal basis, adjoining an index below all of s multiplies e_s on the left by its generator.
• CliffordAlgebra.basis_mul_ι_of_mem and CliffordAlgebra.basis_mul_ι_of_notMem: a basis vector e_s and a basis generator ι Q (b i) commute up to the sign (-1) ^ (|s| - 1) when i ∈ s, and up to (-1) ^ |s| when i ∉ s.
• CliffordAlgebra.basis_comm_ι_iff: a basis vector commutes with every basis generator exactly when its support is empty or is the full index set of odd cardinality, under unit-square hypotheses.
• CliffordAlgebra.basis_univ_mem_center_of_odd_card: the product of an odd number of orthogonal basis generators is central.
• CliffordAlgebra.ι_mul_basis and CliffordAlgebra.basis_mul_basis: for an orthogonal basis, the product of a generator, respectively a basis vector e_s, with a basis vector e_t is (-1) ^ N * (∏ i ∈ s ∩ t, Q (b i)) • e_{s ∆ t}, where N counts the pairs of an index of s and a smaller index of t.
• CliffordAlgebra.basis_mul_basis_eq_or and CliffordAlgebra.basis_mul_self_eq_or: signed multiplication and square laws when the generators square to ±1.
• CliffordAlgebra.basis_commuteOrNeg: basis products commute up to sign for every orthogonal basis.
• CliffordAlgebra.isUnit_basis: a basis monomial is a unit when its generator squares are units.
• CliffordAlgebra.scalarTrace_reverse_basis_mul_basis: the pairing of two basis vectors.
• CliffordAlgebra.scalarTrace_reverse_basis_mul: pairing against a basis vector extracts a coordinate, τ (reverse e_s * x) = (∏ i ∈ s, Q (b i)) * xₛ.
• CliffordAlgebra.scalarTrace_reverse_mul: the pairing in coordinates.
• CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg and CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff: positivity and faithfulness of the pairing over an ordered ring.
• CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff_basis_repr_eq_zero: for a form nonnegative on the basis, the null vectors of the pairing are the elements whose coordinates vanish at every monomial of nonzero quadratic weight.

References

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

@[simp]

theorem CliffordAlgebra.basis_repr_empty {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] (b : Module.Basis I R M) (x : CliffordAlgebra Q) : ((basis Q b).repr x) ∅ = (scalarTrace Q) x

The coordinate at the empty index set is the scalar part, for the basis CliffordAlgebra.basis Q b attached to any basis b of M.

theorem CliffordAlgebra.forall_prod_ne_zero_basis_repr_eq_zero_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} {S : Type u_4} [CommMonoidWithZero S] [NoZeroDivisors S] [Nontrivial S] {w : I → S} (hw : ∀ (i : I), w i ≠ 0) {x : CliffordAlgebra Q} : (∀ (s : Finset I), ∏ i ∈ s, w i ≠ 0 → ((basis Q b).repr x) s = 0) ↔ x = 0

If no weight w i vanishes, then the coordinates of x vanish at every monomial of nonzero weight ∏ i ∈ s, w i exactly when x = 0.

theorem LinearMap.IsOrthoᵢ.pairwise_isOrtho_map_sort {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : Finset I) : List.Pairwise (QuadraticMap.IsOrtho Q) (List.map (⇑b) (s.sort fun (a b : I) => a ≤ b))

The generators of a finite set of indices of an orthogonal basis, listed in increasing order, are pairwise orthogonal.

theorem CliffordAlgebra.basis_eq_prod_map_sort {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : Finset I) : (basis Q b) s = (List.map (⇑(ι Q)) (List.map (⇑b) (s.sort fun (a b : I) => a ≤ b))).prod

For an orthogonal basis b, the Clifford basis vector indexed by s is the ordered product ι Q (b i₁) * ⋯ * ι Q (b iₖ) of the generators of s.sort = [i₁, …, iₖ]. No hypothesis on Q is needed beyond the orthogonality of b; in particular Q may be degenerate.

theorem CliffordAlgebra.exists_basis_eq_ι_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : ↑(Set.powersetCard I 2)) : ∃ (k : I) (l : I), (∀ (i : I), i ∈ ↑s ↔ i = k ∨ i = l) ∧ (basis Q b) ↑s = (ι Q) (b k) * (ι Q) (b l)

For an orthogonal basis b, a two-element index set s is {k, l}, and the Clifford basis vector indexed by s is ι Q (b k) * ι Q (b l).

theorem CliffordAlgebra.involute_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : Finset I) : involute ((basis Q b) s) = (-1) ^ s.card • (basis Q b) s

For an orthogonal basis, the grade involution multiplies the Clifford basis vector indexed by s by the sign (-1) ^ |s| of its degree.

theorem CliffordAlgebra.basis_repr_involute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (x : CliffordAlgebra Q) (s : Finset I) : ((basis Q b).repr (involute x)) s = (-1) ^ s.card * ((basis Q b).repr x) s

For an orthogonal basis, the grade involution multiplies the coordinate at s by the sign (-1) ^ |s|.

theorem CliffordAlgebra.basis_univ_mem_center_of_odd_card {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [Fintype I] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hodd : Odd (Fintype.card I)) : (basis Q b) Finset.univ ∈ Subalgebra.center R (CliffordAlgebra Q)

The full-support Clifford basis vector of an odd-dimensional orthogonal basis is central.

theorem CliffordAlgebra.basis_mul_basis_eq_symm_equivExterior {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) {s t : Finset I} (h : Disjoint s t) : (basis Q b) s * (basis Q b) t = (equivExterior Q).symm (b.ExteriorAlgebra s * b.ExteriorAlgebra t)

For an orthogonal basis, multiplying basis vectors with disjoint index sets is transported from the exterior algebra: the Clifford product of e_s and e_t is the image of the exterior product of the corresponding exterior basis vectors, since no generator meets itself.

theorem CliffordAlgebra.basis_mul_basis_of_disjoint {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) {m n : ℕ} {s : ↑(Set.powersetCard I m)} {t : ↑(Set.powersetCard I n)} (h : Disjoint ↑s ↑t) : (basis Q b) ↑s * (basis Q b) ↑t = Equiv.Perm.sign (Set.powersetCard.permOfDisjoint h) • (basis Q b) ↑(Set.powersetCard.disjUnion h)

The multiplication rule for basis vectors with disjoint index sets: for an orthogonal basis, e_s * e_t = ε • e_{s ∪ t}, where ε is the sign of the shuffle listing s before t. This is the Clifford counterpart of Mathlib's ExteriorAlgebra.basis_mul_of_disjoint.

theorem CliffordAlgebra.basis_mul_ι_of_mem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) {s : Finset I} {i : I} (hi : i ∈ s) : (basis Q b) s * (ι Q) (b i) = (-1) ^ (s.card - 1) • ((ι Q) (b i) * (basis Q b) s)

A basis generator crosses a basis vector containing it at the cost of (-1) ^ (|s| - 1), for an orthogonal basis: e_s * ι Q (b i) = (-1) ^ (|s| - 1) • (ι Q (b i) * e_s) when i ∈ s.

theorem CliffordAlgebra.basis_mul_ι_of_notMem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) {s : Finset I} {i : I} (hi : i ∉ s) : (basis Q b) s * (ι Q) (b i) = (-1) ^ s.card • ((ι Q) (b i) * (basis Q b) s)

A basis generator crosses a basis vector not containing it at the cost of (-1) ^ |s|, for an orthogonal basis: e_s * ι Q (b i) = (-1) ^ |s| • (ι Q (b i) * e_s) when i ∉ s.

theorem CliffordAlgebra.basis_insert_of_forall_lt {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) {a : I} {s : Finset I} (ha : ∀ x ∈ s, a < x) : (basis Q b) (insert a s) = (ι Q) (b a) * (basis Q b) s

For an orthogonal basis, adjoining an index a smaller than every index of s multiplies the basis vector e_s on the left by the generator ι Q (b a).

theorem CliffordAlgebra.ι_mul_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (a : I) (t : Finset I) : (ι Q) (b a) * (basis Q b) t = ((-1) ^ {x ∈ t | x < a}.card * if a ∈ t then Q (b a) else 1) • (basis Q b) (symmDiff t {a})

A generator times a basis vector, for an orthogonal basis: ι Q (b a) * e_t is the basis vector of t ∆ {a}, with the sign (-1) ^ k for the number k of indices of t below a, and the scalar Q (b a) when a ∈ t, since the generator then meets itself.

theorem CliffordAlgebra.basis_mul_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s t : Finset I) : (basis Q b) s * (basis Q b) t = (((-1) ^ ∑ i ∈ s, {x ∈ t | x < i}.card) * ∏ i ∈ s ∩ t, Q (b i)) • (basis Q b) (symmDiff s t)

The multiplication rule for the basis of an orthogonal basis: e_s * e_t = ((-1) ^ N * ∏ i ∈ s ∩ t, Q (b i)) • e_{s ∆ t}, where N = ∑ i ∈ s, #{j ∈ t | j < i} counts the pairs of an index of s and a smaller index of t. Each common index contributes the square Q (b i) of its generator. For disjoint s and t, CliffordAlgebra.basis_mul_basis_of_disjoint writes the same product with the sign of a shuffle permutation.

theorem CliffordAlgebra.basis_mul_basis_eq_or {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), Q (b i) = 1 ∨ Q (b i) = -1) (s t : Finset I) : (basis Q b) s * (basis Q b) t = (basis Q b) (symmDiff s t) ∨ (basis Q b) s * (basis Q b) t = -(basis Q b) (symmDiff s t)

When every generator squares to ±1, the product of two basis vectors is ±e_{s ∆ t}.

theorem CliffordAlgebra.basis_commuteOrNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s t : Finset I) : TauCeti.CommuteOrNeg ((basis Q b) s) ((basis Q b) t)

For an orthogonal basis, two basis-vector products commute or anticommute.

theorem CliffordAlgebra.basis_mul_self_eq_or {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), Q (b i) = 1 ∨ Q (b i) = -1) (s : Finset I) : (basis Q b) s * (basis Q b) s = 1 ∨ (basis Q b) s * (basis Q b) s = -1

When every generator squares to ±1, each basis vector e_s squares to ±1.

theorem CliffordAlgebra.isUnit_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : Finset I) (hQ : ∀ i ∈ s, IsUnit (Q (b i))) : IsUnit ((basis Q b) s)

An orthogonal basis vector is a unit whenever the squares of its generators are units.

theorem CliffordAlgebra.basis_comm_ι_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [Fintype I] [Nontrivial R] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), IsUnit (Q (b i))) (s : Finset I) : (∀ (i : I), (basis Q b) s * (ι Q) (b i) = (ι Q) (b i) * (basis Q b) s) ↔ s = ∅ ∨ s = Finset.univ ∧ Odd s.card

A basis vector commutes with every basis generator exactly when its support is empty or is the full index set of odd cardinality, for an orthogonal basis whose vectors have unit squares over a nontrivial commutative ring in which 2 is invertible.

theorem CliffordAlgebra.scalarTrace_reverse_basis_mul_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s t : Finset I) : (scalarTrace Q) (reverse ((basis Q b) s) * (basis Q b) t) = if s = t then ∏ i ∈ s, Q (b i) else 0

The basis of an orthogonal basis is orthogonal for the trace pairing (x, y) ↦ τ (reverse x * y), and the basis vector indexed by s pairs with itself to ∏ i ∈ s, Q (b i).

theorem CliffordAlgebra.scalarTrace_reverse_basis_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (s : Finset I) (x : CliffordAlgebra Q) : (scalarTrace Q) (reverse ((basis Q b) s) * x) = (∏ i ∈ s, Q (b i)) * ((basis Q b).repr x) s

Pairing against a basis vector extracts a coordinate: for an orthogonal basis, τ (reverse e_s * x) = (∏ i ∈ s, Q (b i)) * xₛ, where xₛ is the coordinate of x at s.

theorem CliffordAlgebra.scalarTrace_reverse_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (x y : CliffordAlgebra Q) : (scalarTrace Q) (reverse x * y) = ((basis Q b).repr x).sum fun (s : Finset I) (c : R) => c * ((∏ i ∈ s, Q (b i)) * ((basis Q b).repr y) s)

The trace pairing in coordinates: for an orthogonal basis b, τ (reverse x * y) = ∑ₛ xₛ * ((∏ i ∈ s, Q (b i)) * yₛ), the sum running over the support of the coordinates of x.

theorem CliffordAlgebra.scalarTrace_reverse_mul_self_nonneg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [LinearOrder R] [IsOrderedRing R] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), 0 ≤ Q (b i)) (x : CliffordAlgebra Q) : 0 ≤ (scalarTrace Q) (reverse x * x)

Positivity of the trace pairing: if Q is nonnegative on an orthogonal basis, then τ (reverse x * x) ≥ 0 for every x.

theorem CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff_basis_repr_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} [LinearOrder I] {b : Module.Basis I R M} [LinearOrder R] [IsStrictOrderedRing R] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), 0 ≤ Q (b i)) {x : CliffordAlgebra Q} : (scalarTrace Q) (reverse x * x) = 0 ↔ ∀ (s : Finset I), ∏ i ∈ s, Q (b i) ≠ 0 → ((basis Q b).repr x) s = 0

Null vectors of the trace pairing in coordinates: if Q is nonnegative on an orthogonal basis, then τ (reverse x * x) = 0 exactly when the coordinates of x vanish at every monomial of nonzero quadratic weight.

theorem CliffordAlgebra.scalarTrace_reverse_mul_self_eq_zero_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] {Q : QuadraticForm R M} {I : Type u_3} {b : Module.Basis I R M} [LinearOrder R] [IsStrictOrderedRing R] (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b) (hQ : ∀ (i : I), 0 < Q (b i)) {x : CliffordAlgebra Q} : (scalarTrace Q) (reverse x * x) = 0 ↔ x = 0

Faithfulness of the trace pairing: if Q is positive on an orthogonal basis, then τ (reverse x * x) = 0 only for x = 0. The index type of the basis need not be ordered.