Orthonormal bases as isometries with the compact coordinate form

Let V be a real inner product space and Q a quadratic form on V with Q v = -‖v‖², the sign convention of geometric Clifford multiplication. The coordinates x ↦ ∑ i, x i • b i of an orthonormal basis b of V are an isometry from the negated positive-definite coordinate form -realCliffordForm n 0 to Q. Composed with the comparisons of a form with its negative, it compares the even Clifford algebra and the Spin group of the compact coordinate form with those of Q, along the frame b (OrthonormalBasis.realEvenCliffordEquiv and OrthonormalBasis.realSpinGroupEquiv).

For a form with Q v = ‖v‖² instead, the coordinates v ↦ (b.repr v i)ᵢ are an isometry from Q to the positive-definite coordinate form realCliffordForm n 0 itself, the form defining the compact Spin group Spin(n). This is the frame identification of the Spin group of Q with Spin(n).

Main definitions

• OrthonormalBasis.negRealCliffordFormIsometryEquiv b hQ: the coordinates of an orthonormal basis b, as an isometry from -realCliffordForm n 0 to a form Q v = -‖v‖².
• OrthonormalBasis.realEvenCliffordEquiv b hQ: the comparison of the even Clifford algebras of the positive-definite coordinate form and of Q along b.
• OrthonormalBasis.isometryEquivRealCliffordFormZero b hQ: for Q v = ‖v‖², the coordinates of b, as an isometry from Q to realCliffordForm n 0.

Main results

• OrthonormalBasis.negRealCliffordFormIsometryEquiv_apply: the isometry sends x to ∑ i, x i • b i.
• OrthonormalBasis.negRealCliffordFormIsometryEquiv_single: it sends the i-th coordinate vector to b i.
• OrthonormalBasis.negRealCliffordFormIsometryEquiv_symm_apply: its inverse takes coordinates in b.
• OrthonormalBasis.coe_realEvenCliffordEquiv_apply: the even frame comparison is evenEquivEvenNeg followed by the map induced by the coordinates of b.
• OrthonormalBasis.realEvenCliffordEquiv_ι: the even frame comparison sends a bivector eᵢ eⱼ to -c(bᵢ) c(bⱼ).
• OrthonormalBasis.isometryEquivRealCliffordFormZero_apply_self: the positive coordinate isometry sends b i to the i-th coordinate vector.

References

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

theorem OrthonormalBasis.ne_zero_of_neg_norm_sq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) [Nonempty (Fin n)] : Q ≠ 0

A negative norm-square form on a space with a nonempty orthonormal basis is nonzero.

noncomputable def OrthonormalBasis.negRealCliffordFormIsometryEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) : QuadraticMap.IsometryEquiv (-TauCeti.realCliffordForm n 0) Q

The coordinates of an orthonormal basis b, x ↦ ∑ i, x i • b i, as an isometry from the negated positive-definite coordinate form -realCliffordForm n 0 to a form Q v = -‖v‖².

theorem OrthonormalBasis.negRealCliffordFormIsometryEquiv_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (x : Fin (n + 0) → ℝ) : (b.negRealCliffordFormIsometryEquiv hQ) x = ∑ i : Fin (n + 0), x i • b i

OrthonormalBasis.negRealCliffordFormIsometryEquiv sends x to ∑ i, x i • b i.

@[simp]

theorem OrthonormalBasis.negRealCliffordFormIsometryEquiv_single {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (i : Fin n) : (b.negRealCliffordFormIsometryEquiv hQ) (Pi.single i 1) = b i

OrthonormalBasis.negRealCliffordFormIsometryEquiv sends the i-th coordinate vector to b i.

@[simp]

theorem OrthonormalBasis.negRealCliffordFormIsometryEquiv_symm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (v : V) (i : Fin n) : (b.negRealCliffordFormIsometryEquiv hQ).symm v i = (b.repr v).ofLp i

The inverse of OrthonormalBasis.negRealCliffordFormIsometryEquiv takes the coordinates b.repr v of a vector v.

noncomputable def OrthonormalBasis.realEvenCliffordEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) : ↥(CliffordAlgebra.even (TauCeti.realCliffordForm n 0)) ≃ₐ[ℝ] ↥(CliffordAlgebra.even Q)

The comparison of the even Clifford algebras of the positive-definite coordinate form and of a form Q v = -‖v‖², along the orthonormal basis b. It sends a bivector eᵢ eⱼ to -c(bᵢ) c(bⱼ) (OrthonormalBasis.realEvenCliffordEquiv_ι).

theorem OrthonormalBasis.coe_realEvenCliffordEquiv_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (x : ↥(CliffordAlgebra.even (TauCeti.realCliffordForm n 0))) : ↑((b.realEvenCliffordEquiv hQ) x) = (CliffordAlgebra.map (b.negRealCliffordFormIsometryEquiv hQ).toIsometry) ↑((CliffordAlgebra.evenEquivEvenNeg (TauCeti.realCliffordForm n 0)) x)

The Clifford value of OrthonormalBasis.realEvenCliffordEquiv b hQ x is obtained by applying evenEquivEvenNeg and then the map induced by the coordinates of b.

@[simp]

theorem OrthonormalBasis.realEvenCliffordEquiv_ι {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (x y : Fin (n + 0) → ℝ) : (b.realEvenCliffordEquiv hQ) (((CliffordAlgebra.even.ι (TauCeti.realCliffordForm n 0)).bilin x) y) = -((CliffordAlgebra.even.ι Q).bilin ((b.negRealCliffordFormIsometryEquiv hQ) x)) ((b.negRealCliffordFormIsometryEquiv hQ) y)

OrthonormalBasis.realEvenCliffordEquiv sends a bivector m n to -c(m') c(n'), where m' and n' are the vectors with coordinates m and n in the basis b.

noncomputable def OrthonormalBasis.isometryEquivRealCliffordFormZero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) : QuadraticMap.IsometryEquiv Q (TauCeti.realCliffordForm n 0)

The coordinates v ↦ (b.repr v i)ᵢ of an orthonormal basis b, as an isometry from a form Q v = ‖v‖² to the positive-definite coordinate form realCliffordForm n 0.

@[simp]

theorem OrthonormalBasis.isometryEquivRealCliffordFormZero_toLinearEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) : (b.isometryEquivRealCliffordFormZero hQ).toLinearEquiv = b.toBasis.equivFun

The linear equivalence underlying OrthonormalBasis.isometryEquivRealCliffordFormZero is the coordinate equivalence of b.

@[simp]

theorem OrthonormalBasis.isometryEquivRealCliffordFormZero_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) (v : V) (i : Fin (n + 0)) : (b.isometryEquivRealCliffordFormZero hQ) v i = (b.repr v).ofLp i

OrthonormalBasis.isometryEquivRealCliffordFormZero takes the coordinates of a vector in the basis b.

theorem OrthonormalBasis.isometryEquivRealCliffordFormZero_symm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) (x : Fin (n + 0) → ℝ) : (b.isometryEquivRealCliffordFormZero hQ).symm x = ∑ i : Fin (n + 0), x i • b i

The inverse of OrthonormalBasis.isometryEquivRealCliffordFormZero sends x to ∑ i, x i • b i.

@[simp]

theorem OrthonormalBasis.isometryEquivRealCliffordFormZero_apply_self {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) (i : Fin n) : (b.isometryEquivRealCliffordFormZero hQ) (b i) = Pi.single i 1

OrthonormalBasis.isometryEquivRealCliffordFormZero sends b i to the i-th coordinate vector.

@[simp]

theorem OrthonormalBasis.isometryEquivRealCliffordFormZero_symm_single {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = ‖v‖ ^ 2) (i : Fin n) : (b.isometryEquivRealCliffordFormZero hQ).symm (Pi.single i 1) = b i

The inverse of OrthonormalBasis.isometryEquivRealCliffordFormZero sends the i-th coordinate vector to b i.