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.

Main definitions

• CliffordAlgebra.bivector: the half-normalized commutator of two Clifford generators.
• CliffordAlgebra.bivectorAlternating: the corresponding alternating map.
• CliffordAlgebra.bivectorBilinear: the same operation as a linear map in each argument.
• 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.map_bivector_lie_ι: any ring homomorphism f out of the Clifford algebra satisfies ⁅f (bivector Q a b), f (ι Q x)⁆ = f (ι Q (QuadraticMap.polar Q b x • a - QuadraticMap.polar Q a x • b)).
• CliffordAlgebra.ι_mul_ι_lie_ι: the commutator of a product of two generators with a third, valid without inverting 2; CliffordAlgebra.commute_ι_mul_ι_ι_of_isOrtho: it vanishes when the third generator is orthogonal to the other two.
• 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.bivectorExterior_exteriorPower_basis: the exterior-square map sends the basis of ⋀² M attached to a basis b of M to the matching vectors of the Clifford basis CliffordAlgebra.basis Q b.
• 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.
• CliffordAlgebra.map_bivector and CliffordAlgebra.map_bivectorExterior: the algebra map induced by a quadratic isometry f sends bivectors to bivectors and intertwines the exterior-square map with ⋀² f.

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.

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.

@[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.bivectorBilinear {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : M →ₗ[R] M →ₗ[R] CliffordAlgebra Q

The half-normalized Clifford bivector, regarded as a linear map in each argument.

@[simp]

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

Evaluating the bilinear Clifford bivector map gives the half-normalized commutator.

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.

@[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.bivectorExterior_exteriorPower_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {I : Type u_1} [LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I 2)) : (bivectorExterior Q) ((Module.Basis.exteriorPower 2 b) s) = (basis Q b) ↑s

The exterior-square Clifford bivector map sends the vector of the basis b.exteriorPower 2 of ⋀² M indexed by s to the vector of the Clifford basis CliffordAlgebra.basis Q b indexed by s.

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.

theorem CliffordAlgebra.map_bivector_lie_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {A : Type u_1} [Ring A] {F : Type u_2} [FunLike F (CliffordAlgebra Q) A] [RingHomClass F (CliffordAlgebra Q) A] (f : F) (a b x : M) : ⁅f (bivector Q a b), f ((ι Q) x)⁆ = f ((ι Q) (QuadraticMap.polar (⇑Q) b x • a - QuadraticMap.polar (⇑Q) a x • b))

Any ring homomorphism f out of a Clifford algebra carries the normalized bivector commutator identity to the corresponding commutator in its target algebra: ⁅f (bivector Q a b), f (ι Q x)⁆ = f (ι Q (QuadraticMap.polar Q b x • a - QuadraticMap.polar Q a x • b)).

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

The commutator of a product of two generators with a third generator: ⁅ι a * ι b, ι x⁆ = ι (polar b x • a - polar a x • b). The product differs from the bivector of a and b by a scalar, so this is the same infinitesimal rotation as in bivector_lie_ι, but it holds without inverting 2.

theorem CliffordAlgebra.commute_ι_mul_ι_ι_of_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {a b x : M} (ha : QuadraticMap.IsOrtho Q a x) (hb : QuadraticMap.IsOrtho Q b x) : Commute ((ι Q) a * (ι Q) b) ((ι Q) x)

The product of two generators commutes with every generator orthogonal to both.

@[simp]

theorem CliffordAlgebra.map_bivector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {M₂ : Type u_1} [AddCommGroup M₂] [Module R M₂] {Q₂ : QuadraticForm R M₂} (f : Q →qᵢ Q₂) (a b : M) : (map f) (bivector Q a b) = bivector Q₂ (f a) (f b)

The algebra map induced by a quadratic isometry sends Clifford bivectors to Clifford bivectors.

theorem CliffordAlgebra.map_bivectorExterior {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {M₂ : Type u_1} [AddCommGroup M₂] [Module R M₂] {Q₂ : QuadraticForm R M₂} (f : Q →qᵢ Q₂) (x : ↥(⋀[R]^2 M)) : (map f) ((bivectorExterior Q) x) = (bivectorExterior Q₂) ((exteriorPower.map 2 f.toLinearMap) x)

Naturality of the Clifford bivector map: the algebra map induced by a quadratic isometry f intertwines bivectorExterior with the induced map ⋀² f of exterior squares.