The vectors and the scalars inside a Clifford algebra

The generators of a Clifford algebra are the elements ι Q m, and the first thing one wants to know about them is that they are a faithful copy of M: that ι Q is injective, so that M is the module of vectors LinearMap.range (ι Q) sitting inside CliffordAlgebra Q, and that no nonzero vector is a scalar.

Mathlib proves all of this for the exterior algebra, which is the Clifford algebra of the zero form (ExteriorAlgebra.ι_leftInverse, ExteriorAlgebra.ι_inj, ExteriorAlgebra.ι_eq_algebraMap_iff, ExteriorAlgebra.ι_range_disjoint_one), using the square-zero extension TrivSqZeroExt R M as an auxiliary algebra. That trick is unavailable for a general Q: in TrivSqZeroExt R M the square of a vector is 0, so it computes Q = 0 and nothing else. What is available instead is Mathlib's module isomorphism CliffordAlgebra.equivExterior Q : CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M, valid whenever 2 is invertible, which sends generators to generators and scalars to scalars. This file transports the exterior-algebra statements along it, so all of them hold for an arbitrary quadratic form over a commutative ring in which 2 is invertible; no hypothesis on Q — no nondegeneracy, no finiteness, no freeness — is needed.

The payoff is CliffordAlgebra.ιRangeEquiv, the linear equivalence M ≃ₗ[R] range (ι Q). It is what turns a statement about elements of CliffordAlgebra Q that happen to lie in range (ι Q) into a statement about vectors of M: Mathlib's twisted conjugation lemmas (lipschitzGroup.conjAct_smul_range_ι, spinGroup.involute_act_ι_mem_range_ι) say only that the Lipschitz and spin groups act on range (ι Q), and it is ιRangeEquiv that transports such an action to an honest linear automorphism of M. Landing in the orthogonal group of Q is a further step: a linear automorphism is not orthogonal for free, and that the transported action preserves Q has to be proved separately.

Against the degree filtration CliffordAlgebra.filtration, whose first step is spanned by the scalars and the vectors, the disjointness of the two pins that step down to R ⊕ M: CliffordAlgebra.filtrationOneEquiv.

Main definitions

• CliffordAlgebra.ιInv: the linear left inverse of ι Q, the vector part of an element of the Clifford algebra.
• CliffordAlgebra.ιRangeEquiv: the vector equivalence M ≃ₗ[R] range (ι Q).
• CliffordAlgebra.scalarAddVector and CliffordAlgebra.filtrationOneEquiv: the map (r, m) ↦ r + ι Q m out of R × M, and the equivalence with the first step of the degree filtration that it induces.

Main results

• CliffordAlgebra.ι_injective, CliffordAlgebra.ι_inj and CliffordAlgebra.ι_eq_zero_iff: the generators are a faithful copy of M.
• CliffordAlgebra.commute_ι_iff_exists_eq_smul: two vectors commute exactly when they are proportional, once the first has unit value under Q.
• CliffordAlgebra.eq_zero_of_commute_ι_of_isOrtho: over a field, a vector commuting with two orthogonal anisotropic vectors is zero.
• CliffordAlgebra.eq_zero_or_exists_ι_eq_smul_of_mul_self_eq_algebraMap: over a field, if a vector plus a multiple of a commuting element with nonzero scalar square has scalar square, then the multiple vanishes or the vector is a multiple of that element.
• CliffordAlgebra.mul_ι_notMem_range_ι_of_mul_ι_eq_neg: over a field, a nonzero element anticommuting with two orthogonal anisotropic companions of an anisotropic vector v sends ι Q v outside the vectors.
• CliffordAlgebra.ι_eq_algebraMap_iff, CliffordAlgebra.ι_ne_one and CliffordAlgebra.ι_range_disjoint_one: a vector is a scalar only when both vanish.
• CliffordAlgebra.mem_range_ι_iff: membership of range (ι Q) is detected by the vector part.
• CliffordAlgebra.finrank_filtration_one: the first step of the degree filtration has one more dimension than M.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 2, "Vectors from the Clifford algebra".
• N. Bourbaki, Algebra I, Chapters 1-3 (1989), §9.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

The comparison with the exterior algebra

Mathlib's CliffordAlgebra.equivExterior is only a linear equivalence. Its scalar equation is recorded in the general Clifford-algebra API; here we record the generator equation needed for the vector API. Both are immediate from its definition as a changeForm.

theorem CliffordAlgebra.equivExterior_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) : (equivExterior Q) ((ι Q) m) = (ExteriorAlgebra.ι R) m

CliffordAlgebra.equivExterior sends a generator to the corresponding generator of the exterior algebra.

The vector part

def CliffordAlgebra.ιInv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : CliffordAlgebra Q →ₗ[R] M

The vector part of an element of a Clifford algebra: a linear left inverse of ι Q.

This is ExteriorAlgebra.ιInv transported along CliffordAlgebra.equivExterior, which is where the hypothesis [Invertible (2 : R)] comes from; the square-zero extension that builds ExteriorAlgebra.ιInv directly sees only the zero quadratic form.

Equations

• CliffordAlgebra.ιInv Q = ExteriorAlgebra.ιInv ∘ₗ ↑(CliffordAlgebra.equivExterior Q)

@[simp]

theorem CliffordAlgebra.ιInv_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) : (ιInv Q) ((ι Q) m) = m

theorem CliffordAlgebra.ι_leftInverse {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Function.LeftInverse ⇑(ιInv Q) ⇑(ι Q)

@[simp]

theorem CliffordAlgebra.ιInv_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (r : R) : (ιInv Q) ((algebraMap R (CliffordAlgebra Q)) r) = 0

The vector part of a scalar vanishes.

The exterior-algebra half of the argument is that ExteriorAlgebra.map 0 fixes scalars while it kills vector parts (ExteriorAlgebra.ιInv_comp_map).

ι is injective

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

The generators of a Clifford algebra are a faithful copy of M. When 2 is invertible this needs no hypothesis on Q.

@[simp]

theorem CliffordAlgebra.ι_inj {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m n : M) : (ι Q) m = (ι Q) n ↔ m = n

Two generators are equal exactly when the vectors they come from are.

@[simp]

theorem CliffordAlgebra.ι_eq_zero_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) : (ι Q) m = 0 ↔ m = 0

The only generator that vanishes is the one coming from 0.

Commuting vectors are proportional

theorem CliffordAlgebra.commute_ι_iff_exists_eq_smul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {u w : M} (hu : IsUnit (Q u)) : Commute ((ι Q) u) ((ι Q) w) ↔ ∃ (c : R), w = c • u

Two vectors commute in the Clifford algebra exactly when they are proportional, provided the first has unit value under Q.

Vectors are not scalars

@[simp]

theorem CliffordAlgebra.ι_eq_algebraMap_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) (r : R) : (ι Q) m = (algebraMap R (CliffordAlgebra Q)) r ↔ m = 0 ∧ r = 0

A generator is a scalar only in the trivial way: both the vector and the scalar vanish.

@[simp]

theorem CliffordAlgebra.ι_ne_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] [Nontrivial R] (m : M) : (ι Q) m ≠ 1

No generator is the unit of a Clifford algebra.

theorem CliffordAlgebra.ι_range_disjoint_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Disjoint (ι Q).range 1

The vectors of a Clifford algebra are disjoint from its scalars. Together with TauCeti.Algebra.wordFiltration_one, which writes the first step of the degree filtration as 1 ⊔ LinearMap.range (ι Q), this is what makes that step a direct sum of R and M; see CliffordAlgebra.filtrationOneEquiv.

The vector equivalence

noncomputable def CliffordAlgebra.ιRangeEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : M ≃ₗ[R] ↥(ι Q).range

The vector equivalence: M is the module of vectors LinearMap.range (ι Q) inside its Clifford algebra.

Mathlib's twisted-conjugation lemmas say that the Lipschitz and spin groups act on LinearMap.range (ι Q); this equivalence is what transports such an action to a linear automorphism of M. It says nothing about Q: to place that automorphism in the orthogonal group one still has to prove that it preserves Q.

Equations

• CliffordAlgebra.ιRangeEquiv Q = LinearEquiv.ofInjective (CliffordAlgebra.ι Q) ⋯

@[simp]

theorem CliffordAlgebra.coe_ιRangeEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (m : M) : ↑((ιRangeEquiv Q) m) = (ι Q) m

@[simp]

theorem CliffordAlgebra.ι_ιRangeEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(ι Q).range) : (ι Q) ((ιRangeEquiv Q).symm x) = ↑x

theorem CliffordAlgebra.ι_ιInv_of_mem {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : CliffordAlgebra Q} (hx : x ∈ (ι Q).range) : (ι Q) ((ιInv Q) x) = x

The vector part reconstructs a vector.

theorem CliffordAlgebra.mem_range_ι_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : CliffordAlgebra Q} : x ∈ (ι Q).range ↔ (ι Q) ((ιInv Q) x) = x

Membership of the module of vectors is detected by the vector part.

theorem CliffordAlgebra.ιRangeEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(ι Q).range) : (ιRangeEquiv Q).symm x = (ιInv Q) ↑x

On a vector, the retraction ιInv computes the inverse of the vector equivalence.

The first step of the degree filtration

def CliffordAlgebra.scalarAddVector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : R × M →ₗ[R] CliffordAlgebra Q

The elements of degree at most one, as a map out of R × M: (r, m) ↦ r + ι Q m. It is injective with image CliffordAlgebra.filtration Q 1.

Equations

• CliffordAlgebra.scalarAddVector Q = (Algebra.linearMap R (CliffordAlgebra Q)).coprod (CliffordAlgebra.ι Q)

@[simp]

theorem CliffordAlgebra.scalarAddVector_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : R × M) : (scalarAddVector Q) x = (algebraMap R (CliffordAlgebra Q)) x.1 + (ι Q) x.2

theorem CliffordAlgebra.range_scalarAddVector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : (scalarAddVector Q).range = filtration Q 1

The scalars and the vectors span exactly the first step of the degree filtration.

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

A scalar and a vector summing to zero both vanish, the scalars and the vectors being disjoint (CliffordAlgebra.ι_range_disjoint_one).

noncomputable def CliffordAlgebra.filtrationOneEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (R × M) ≃ₗ[R] ↥(filtration Q 1)

The first step of the degree filtration is R ⊕ M. The scalars and the vectors span it (TauCeti.Algebra.wordFiltration_one) and meet only in 0 (CliffordAlgebra.ι_range_disjoint_one), so together they parametrize it faithfully.

Equations

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

@[simp]

theorem CliffordAlgebra.coe_filtrationOneEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : R × M) : ↑((filtrationOneEquiv Q) x) = (algebraMap R (CliffordAlgebra Q)) x.1 + (ι Q) x.2

theorem CliffordAlgebra.finrank_filtration_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] [FiniteDimensional K V] : Module.finrank K ↥(filtration Q 1) = Module.finrank K V + 1

Counting dimensions in CliffordAlgebra.filtrationOneEquiv: the first step of the degree filtration is one dimension bigger than the space of vectors.

A vector commuting with two orthogonal anisotropic vectors is zero

theorem CliffordAlgebra.eq_zero_of_commute_ι_of_isOrtho {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] {u₁ u₂ w : V} (hu₁ : Q u₁ ≠ 0) (hu₂ : Q u₂ ≠ 0) (hu₁u₂ : QuadraticMap.IsOrtho Q u₁ u₂) (h₁ : Commute ((ι Q) u₁) ((ι Q) w)) (h₂ : Commute ((ι Q) u₂) ((ι Q) w)) : w = 0

A vector commuting with two orthogonal anisotropic vectors is zero. Commuting with an anisotropic u makes w proportional to u (commute_ι_iff_exists_eq_smul), so w is proportional to both u₁ and u₂, and pairing with u₁ gives 2 c₁ Q u₁ = polar Q u₁ w = 0.

A vector plus a commuting element with scalar square

theorem CliffordAlgebra.eq_zero_or_exists_ι_eq_smul_of_mul_self_eq_algebraMap {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] {ω : CliffordAlgebra Q} {w : V} (hω : Commute ω ((ι Q) w)) {s : K} (hsq : ω * ω = (algebraMap K (CliffordAlgebra Q)) s) (hs : s ≠ 0) {c q : K} (h : ((ι Q) w + c • ω) * ((ι Q) w + c • ω) = (algebraMap K (CliffordAlgebra Q)) q) : c = 0 ∨ ∃ (t : K), (ι Q) w = t • ω

A vector plus a multiple of a commuting element with nonzero scalar square has scalar square only if the multiple vanishes or the vector is itself a multiple of that element. Let ω commute with ι Q w and have ω * ω the nonzero scalar s. If (ι Q w + c • ω) ^ 2 is a scalar, then either c = 0 or ι Q w is a multiple of ω: the cross term 2 c • (ω * ι Q w) is a scalar, and multiplying it by ω once more isolates ι Q w. Only commutation with the single vector ι Q w is needed; a central ω (such as a volume element in odd dimension) supplies it.

An anticommuting element moves an anisotropic vector out of the vectors

theorem CliffordAlgebra.mul_ι_notMem_range_ι_of_mul_ι_eq_neg {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} [Invertible 2] {ω : CliffordAlgebra Q} (hω : ω ≠ 0) {v u₁ u₂ : V} (hv : Q v ≠ 0) (hu₁ : Q u₁ ≠ 0) (hu₂ : Q u₂ ≠ 0) (hvu₁ : QuadraticMap.IsOrtho Q v u₁) (hvu₂ : QuadraticMap.IsOrtho Q v u₂) (hu₁u₂ : QuadraticMap.IsOrtho Q u₁ u₂) (h₁ : ω * (ι Q) u₁ = -((ι Q) u₁ * ω)) (h₂ : ω * (ι Q) u₂ = -((ι Q) u₂ * ω)) : ω * (ι Q) v ∉ (ι Q).range

A nonzero element anticommuting with two orthogonal anisotropic companions of an anisotropic vector v sends ι Q v outside the vectors. Only the two anticommutation relations are required of ω; the volume element of an orthogonal list of even length containing u₁ and u₂ satisfies them.