Even-Clifford transport along a negative vector

Multiplying a Clifford generator on the right by a fixed generator produces a linear map into the even Clifford algebra. When the fixed vector has quadratic value -1, conjugation by its negated generator preserves the even subalgebra. These constructions provide the algebraic transport used by low-rank Spin action comparisons without depending on Spin groups.

Main definitions

• CliffordAlgebra.rightIotaEven Q e is the linear map m ↦ ι(m)ι(e) into the even Clifford algebra.
• CliffordAlgebra.conjugateNegativeIotaEven Q e he restricts conjugation by -ι(e) to the even algebra when Q(e) = -1.

def CliffordAlgebra.rightIotaEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (e : M) : M →ₗ[R] ↥(even Q)

The linear map into the even Clifford algebra obtained by multiplying a generating vector on the right by another generating vector.

Equations

• CliffordAlgebra.rightIotaEven Q e = (CliffordAlgebra.even.ι Q).bilin.flip e

@[simp]

theorem CliffordAlgebra.rightIotaEven_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (e m : M) : (rightIotaEven Q e) m = ((even.ι Q).bilin m) e

Evaluating rightIotaEven gives the canonical bilinear generator of the even algebra.

theorem CliffordAlgebra.coe_rightIotaEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (e m : M) : ↑((rightIotaEven Q e) m) = (ι Q) m * (ι Q) e

The ambient Clifford value of rightIotaEven.

@[simp]

theorem CliffordAlgebra.coe_even_ι_bilin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m e : M) : ↑(((even.ι Q).bilin m) e) = (ι Q) m * (ι Q) e

Coercing a canonical bilinear generator of the even algebra gives the product of its two Clifford generators.

noncomputable def CliffordAlgebra.conjugateNegativeIotaEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (e : M) (he : Q e = -1) : ↥(even Q) →ₐ[R] ↥(even Q)

If Q(e) = -1, conjugation by the unit -ι(e) preserves the even Clifford algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.coe_conjugateNegativeIotaEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (e : M) (he : Q e = -1) (x : ↥(even Q)) : ↑((conjugateNegativeIotaEven Q e he) x) = -(ι Q) e * ↑x * (ι Q) e

The ambient Clifford value of conjugation by -ι(e) on the even subalgebra.