Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.OrthonormalBasis

Orthonormal bases in the Clifford algebra of minus the squared norm #

Let V be a real inner product space and Q a quadratic form on V with Q v = -‖v‖², the sign convention under which the Clifford relation reads c(v) c(w) + c(w) c(v) = -2 ⟪v, w⟫. Then orthogonality for Q is orthogonality for the inner product, so an orthonormal basis e of V is an orthogonal basis for Q with Q (eᵢ) = -1. The general orthogonal-basis results of TauCeti.LinearAlgebra.CliffordAlgebra.OrthogonalBasis therefore apply to e, and the Clifford basis vector e_s indexed by a finite set s of indices squares to the sign (-1) ^ ((|s| + 1).choose 2).

Main results #

References #

source
theorem QuadraticMap.isOrtho_iff_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {x y : V} :
IsOrtho Q x y ↔ inner ℝ x y = 0

For Q v = -‖v‖², orthogonality for Q is orthogonality for the inner product.

source
theorem OrthonormalBasis.isOrthoᵢ_associated {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ V) :
LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b.toBasis

For Q v = -‖v‖², an orthonormal basis is orthogonal for the polar form of Q.

source
theorem OrthonormalBasis.isOrtho_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ V) {i j : ι} (hij : i ≠ j) :
QuadraticMap.IsOrtho Q (b i) (b j)

For Q v = -‖v‖², distinct orthonormal basis vectors are orthogonal for Q.

source
theorem OrthonormalBasis.pairwise_isOrtho_map {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ V) {l : List ι} (hl : l.Nodup) :
List.Pairwise (QuadraticMap.IsOrtho Q) (List.map (⇑b) l)

For Q v = -‖v‖², the members of a list of distinct orthonormal basis vectors are pairwise orthogonal for Q.

source
theorem OrthonormalBasis.map_apply_mul_map_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ V) (i j : ι) :
Q (b i) * Q (b j) = 1

For Q v = -‖v‖², the product of the values of Q at two orthonormal basis vectors is one.

source
theorem OrthonormalBasis.prod_map_map_eq_neg_one_pow {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] (b : OrthonormalBasis ι ℝ V) (l : List ι) :
(List.map (⇑Q) (List.map (⇑b) l)).prod = (-1) ^ l.length

For Q v = -‖v‖², Q takes the value -1 at every member of a list of orthonormal basis vectors.

source
theorem CliffordAlgebra.even_ι_bilin_add_swap_eq_neg_two_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (u v : V) :
((even.ι Q).bilin u) v + ((even.ι Q).bilin v) u = (algebraMap ℝ ↥(even Q)) (-2 * inner ℝ u v)

For Q v = -‖v‖², the even Clifford relation is c(u) c(v) + c(v) c(u) = -2 ⟪u, v⟫.

source
theorem CliffordAlgebra.basis_mul_self_of_orthonormal {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) {ι : Type u_2} [Fintype ι] [LinearOrder ι] (b : OrthonormalBasis ι ℝ V) (s : Finset ι) :
(basis Q b.toBasis) s * (basis Q b.toBasis) s = (-1) ^ (s.card + 1).choose 2

The square of a Clifford basis vector of an orthonormal basis: for Q v = -‖v‖², the ordered product e_s of the generators indexed by s satisfies e_s * e_s = (-1) ^ ((|s| + 1).choose 2). Reordering contributes (-1) ^ (|s|.choose 2) and each generator squares to -1.