Clifford bivectors and exterior squares

This module packages the generic half-normalized Clifford commutator into an alternating map and the induced linear map from the second exterior power. Its action on a Clifford generator is given by the polarization of the quadratic form.

The formula is valid over every commutative ring in which 2 is invertible. The factor ⅟2 is forced: the commutator of the unnormalized expression acts by twice the desired infinitesimal rotation.

This is a shared generic prerequisite for the roadmap's Layer 3 standard-form normalization and the later Layer 9 arbitrary-form realization. It constructs neither bivectorEquivSo nor soEquivQuadratic, and it does not construct a transported Lie bracket, a Spin action, or the Layer 9 CAR worked instance.

Main definitions

• CliffordAlgebra.bivector: the half-normalized commutator of two Clifford generators.
• CliffordAlgebra.bivectorAlternating: the corresponding alternating map.
• CliffordAlgebra.bivectorExterior: the induced linear map from the second exterior power.

Main results

• CliffordAlgebra.bivector_lie_ι: its commutator action on a generator is the infinitesimal rotation determined by QuadraticMap.polar.
• CliffordAlgebra.ι_mul_ι_eq_bivector_add: the product of two generators is its Clifford bivector plus its scalar symmetric part.
• CliffordAlgebra.bivector_eq_ι_mul_ι_of_isOrtho and CliffordAlgebra.bivector_mul_self_of_isOrtho: for orthogonal generators the bivector is their plain product, and its square is the scalar -(Q a * Q b).
• CliffordAlgebra.bivectorExterior_apply_ιMulti: the exterior-square map on a decomposable bivector.
• CliffordAlgebra.equivExterior_bivector, CliffordAlgebra.equivExterior_bivectorExterior, and CliffordAlgebra.bivectorExterior_injective: the exterior model sends bivectors to exterior products, so the exterior-square map is injective.
• CliffordAlgebra.bivector_mem_evenOdd_zero and CliffordAlgebra.bivector_mem_filtration_two: it is even and has filtration degree at most two.
• CliffordAlgebra.bivectorExterior_range_le_of_bivector_mem: the exterior-square map lands in any submodule containing the Clifford bivectors.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 3, "the Lie algebra 𝔰𝔬(V) ≅ ⋀²V inside the Clifford algebra".

noncomputable def CliffordAlgebra.bivector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : CliffordAlgebra Q

The half-normalized Clifford commutator of two generators. Its action on a third generator is the infinitesimal rotation in bivector_lie_ι; that action, rather than this expression, fixes the normalization.

Equations

• CliffordAlgebra.bivector Q a b = ⅟2 • ((CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b - (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)

theorem CliffordAlgebra.bivector_def {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : bivector Q a b = ⅟2 • ((ι Q) a * (ι Q) b - (ι Q) b * (ι Q) a)

The defining half-normalized commutator formula for a Clifford bivector.

theorem CliffordAlgebra.ι_mul_ι_eq_bivector_add {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : (ι Q) a * (ι Q) b = bivector Q a b + ⅟2 • (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b)

The product of two Clifford generators is its bivector plus its scalar symmetric part.

theorem CliffordAlgebra.bivector_eq_ι_mul_ι_of_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {a b : M} (h : QuadraticMap.IsOrtho Q a b) : bivector Q a b = (ι Q) a * (ι Q) b

For orthogonal generators the bivector is the plain product. The scalar symmetric part of ι a * ι b is ⅟2 times the polar form of the two vectors, so it disappears exactly when they are orthogonal.

theorem CliffordAlgebra.bivector_mul_self_of_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {a b : M} (h : QuadraticMap.IsOrtho Q a b) : bivector Q a b * bivector Q a b = -(algebraMap R (CliffordAlgebra Q)) (Q a * Q b)

The square of the bivector of two orthogonal generators is a scalar, namely -(Q a * Q b). In particular it vanishes as soon as one of the two vectors is isotropic, which is what makes a root vector of a hyperbolic pair act by a square-zero operator on a Clifford module.

This is CliffordAlgebra.ι_mul_ι_mul_self_of_isOrtho, the bivector being the plain product.

noncomputable def CliffordAlgebra.bivectorAlternating {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : M [⋀^Fin 2]→ₗ[R] CliffordAlgebra Q

The alternating map whose value on two vectors is their half-normalized Clifford bivector.

Equations

• CliffordAlgebra.bivectorAlternating Q = { toFun := fun (v : Fin 2 → M) => CliffordAlgebra.bivector Q (v 0) (v 1), map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem CliffordAlgebra.bivectorAlternating_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : (bivectorAlternating Q) ![a, b] = bivector Q a b

The alternating map agrees with the half-normalized Clifford bivector on a pair of vectors.

noncomputable def CliffordAlgebra.bivectorExterior {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(⋀[R]^2 M) →ₗ[R] CliffordAlgebra Q

The linear map from the second exterior power induced by the Clifford bivector.

Equations

• CliffordAlgebra.bivectorExterior Q = exteriorPower.alternatingMapLinearEquiv (CliffordAlgebra.bivectorAlternating Q)

@[simp]

theorem CliffordAlgebra.bivectorExterior_apply_ιMulti {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : (bivectorExterior Q) ((exteriorPower.ιMulti R 2) ![a, b]) = bivector Q a b

The exterior-square Clifford bivector map on a decomposable bivector.

theorem CliffordAlgebra.equivExterior_bivector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : (equivExterior Q) (bivector Q a b) = (ExteriorAlgebra.ι R) a * (ExteriorAlgebra.ι R) b

The exterior model sends a half-normalized Clifford bivector to its exterior product.

theorem CliffordAlgebra.equivExterior_bivectorExterior {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(⋀[R]^2 M)) : (equivExterior Q) ((bivectorExterior Q) x) = ↑x

The exterior model is a left inverse of the exterior-square Clifford bivector map.

As with equivExterior_basis, this is not a simp lemma because simp unfolds equivExterior before rewriting its applications.

theorem CliffordAlgebra.bivectorExterior_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Function.Injective ⇑(bivectorExterior Q)

The exterior-square Clifford bivector map is injective.

theorem CliffordAlgebra.bivector_swap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : bivector Q b a = -bivector Q a b

Interchanging the two vectors negates their Clifford bivector.

@[simp]

theorem CliffordAlgebra.bivector_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a : M) : bivector Q a a = 0

The Clifford bivector of a repeated vector is zero.

theorem CliffordAlgebra.bivector_mem_evenOdd_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : bivector Q a b ∈ evenOdd Q 0

Clifford bivectors are even.

theorem CliffordAlgebra.bivector_mem_filtration_two {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b : M) : bivector Q a b ∈ filtration Q 2

Clifford bivectors have filtration degree at most two.

theorem CliffordAlgebra.bivectorExterior_range_le_of_bivector_mem {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (P : Submodule R (CliffordAlgebra Q)) (hP : ∀ (a b : M), bivector Q a b ∈ P) : (bivectorExterior Q).range ≤ P

The image of the exterior-square Clifford bivector map lands in any submodule containing every Clifford bivector: the decomposable bivectors generate ⋀[R]^2 M.

theorem CliffordAlgebra.bivector_lie_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b x : M) : ⁅bivector Q a b, (ι Q) x⁆ = (ι Q) (QuadraticMap.polar (⇑Q) b x • a - QuadraticMap.polar (⇑Q) a x • b)

The action-normalization identity for the half-normalized Clifford bivector.