Freeness and dimension of a Clifford algebra

The Clifford relation ι Q m * ι Q m = Q m does not preserve the number of generators in a product, so a Clifford algebra is not graded by degree; what it does do is leave the size of the algebra alone. Over a ring in which 2 is invertible this is Mathlib's CliffordAlgebra.equivExterior, a linear (not algebra) isomorphism CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M valid for every quadratic form. Deforming the form therefore deforms the multiplication and nothing else, and the underlying module of CliffordAlgebra Q is as free, and as large, as the exterior algebra of M.

This file records that. Over a commutative ring in which 2 is invertible, CliffordAlgebra Q is a free R-module whenever M is, with an explicit basis CliffordAlgebra.basis Q b : Basis (Finset I) R (CliffordAlgebra Q) attached to a basis b of M indexed by a linearly ordered I, and it is finite of rank 2 ^ finrank R M whenever M is finite free. The 2 ^ n is ∑ₖ (n choose k) (finrank_eq_sum_choose), the count that a degree-graded argument would produce one exterior power at a time; here it is the count of subsets of a basis index set instead, because the basis is transported from Mathlib's basis Module.Basis.ExteriorAlgebra of the exterior algebra, indexed by finite subsets.

A second section splits that count in half along Mathlib's ℤ/2-grading evenOdd Q. Over a field the two halves of the grading of the Clifford algebra of a nonzero space are isomorphic for every quadratic form, by the odd linear automorphism of TauCeti/LinearAlgebra/CliffordAlgebra/ParitySwap.lean, so over a field in which 2 is invertible, where the count 2 ^ n above is available, each has dimension 2 ^ (n - 1), as does the even subalgebra CliffordAlgebra.even Q.

These counts are what make the structure theory of Clifford algebras run: over an algebraically closed field a nondegenerate Q on a 2l-dimensional space has finrank (CliffordAlgebra Q) = 2 ^ (2 * l) = (2 ^ l) ^ 2, matching Module.End of the 2 ^ l-dimensional spin module, so a surjection between the two is forced to be an isomorphism, while finrank (even Q) = 2 ^ (2 * l - 1) = 2 * (2 ^ (l - 1)) ^ 2 matches the product of two matrix algebras one size down, acting on the two half-spin summands.

Implementation notes

basis transports Mathlib's Module.Basis.ExteriorAlgebra along equivExterior, so its elements are not by definition the products ι Q (b i₁) * ⋯ * ι Q (b iₖ) of generators: equivExterior is built from CliffordAlgebra.changeForm, which corrects a product of generators by lower-order terms. Nothing below needs the products, only their number. Identifying the two families is the Clifford analogue of a Poincaré-Birkhoff-Witt theorem, and is the content of the associated-graded isomorphism gr (CliffordAlgebra Q) ≅ ExteriorAlgebra R M against the degree filtration of TauCeti/LinearAlgebra/CliffordAlgebra/Filtration.lean; it is left to that separate milestone.

Main definitions

• CliffordAlgebra.basis: the basis of CliffordAlgebra Q indexed by the finite subsets of the index set of a basis of M, over a ring in which 2 is invertible.

Main results

• CliffordAlgebra.rank_eq_rank_exteriorAlgebra and CliffordAlgebra.finrank_eq_finrank_exteriorAlgebra: the rank of CliffordAlgebra Q is the rank of ExteriorAlgebra R M. The right-hand sides do not mention Q, so this is the statement that the size of a Clifford algebra does not depend on the quadratic form.
• CliffordAlgebra.instFree and CliffordAlgebra.instFinite: the Clifford algebra of a free module is free, and of a finite free module is finite.
• CliffordAlgebra.finrank_eq_two_pow: finrank R (CliffordAlgebra Q) = 2 ^ finrank R M, with CliffordAlgebra.finrank_eq_sum_choose the same count as a sum of binomial coefficients.
• CliffordAlgebra.two_mul_finrank_evenOdd: over a field, each half of the grading of the Clifford algebra of a nonzero space is exactly half of it, for every quadratic form, and CliffordAlgebra.finrank_evenOdd_of_finrank_eq_two_pow reads that half off any count of the whole algebra by a power of two.
• CliffordAlgebra.finrank_evenOdd and CliffordAlgebra.finrank_even: over a field in which 2 is invertible, each half of the grading of the Clifford algebra of a nonzero finite-dimensional space, and in particular the even subalgebra, has dimension 2 ^ (finrank K V - 1).
• CliffordAlgebra.finrank_evenOdd_zero: the same count for the zero form — the even and the odd half of an exterior algebra — where the total count is available over every field, so no invertibility of 2 is needed.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 0, "The associated graded is the exterior algebra (a PBW-type theorem)".
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.

noncomputable def CliffordAlgebra.basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {I : Type w} [LinearOrder I] (b : Module.Basis I R M) : Module.Basis (Finset I) R (CliffordAlgebra Q)

The basis of CliffordAlgebra Q attached to a basis b of M, indexed by the finite subsets of the index set of b, obtained by transporting Mathlib's basis of ExteriorAlgebra R M along CliffordAlgebra.equivExterior.

Its elements are not products of generators by construction; see the implementation notes.

@[expose] because the characteristic equation basis_apply below is a public theorem whose proof has to unfold this definition.

Equations

• CliffordAlgebra.basis Q b = b.ExteriorAlgebra.map (CliffordAlgebra.equivExterior Q).symm

@[simp]

theorem CliffordAlgebra.basis_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (s : Finset I) : (basis Q b) s = (equivExterior Q).symm (b.ExteriorAlgebra s)

theorem CliffordAlgebra.equivExterior_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {I : Type w} [LinearOrder I] (b : Module.Basis I R M) (s : Finset I) : (equivExterior Q) ((basis Q b) s) = b.ExteriorAlgebra s

CliffordAlgebra.equivExterior sends the basis element basis Q b s back to the exterior algebra basis element b.ExteriorAlgebra s it was transported from.

Not a simp lemma: simp unfolds CliffordAlgebra.equivExterior to the underlying CliffordAlgebra.changeForm, so the left-hand side is not in normal form.

instance CliffordAlgebra.instFree {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) [Module.Free R M] : Module.Free R (CliffordAlgebra Q)

The Clifford algebra of a free module is a free module, over a ring in which 2 is invertible.

instance CliffordAlgebra.instFinite {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) [Module.Free R M] [Module.Finite R M] : Module.Finite R (CliffordAlgebra Q)

The Clifford algebra of a finite free module is a finite module, over a ring in which 2 is invertible.

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

A Clifford algebra has the rank of the exterior algebra of the same module. The right-hand side does not mention Q: deforming the quadratic form deforms the multiplication and leaves the underlying module alone.

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

A Clifford algebra has the finite rank of the exterior algebra of the same module; the finite-rank form of rank_eq_rank_exteriorAlgebra, again independent of Q.

theorem CliffordAlgebra.finrank_eq_two_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) [Nontrivial R] [Module.Free R M] [Module.Finite R M] : Module.finrank R (CliffordAlgebra Q) = 2 ^ Module.finrank R M

The Clifford algebra of a finite free module of rank n has rank 2 ^ n, for every quadratic form on it.

theorem CliffordAlgebra.finrank_eq_sum_choose {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) [Nontrivial R] [Module.Free R M] [Module.Finite R M] : Module.finrank R (CliffordAlgebra Q) = ∑ k ∈ Finset.range (Module.finrank R M + 1), (Module.finrank R M).choose k

The rank of a Clifford algebra as a sum of binomial coefficients: 2 ^ n = ∑ₖ (n choose k), the count that adding up the exterior powers ⋀[R]^k M, of ranks (n choose k), produces.

theorem CliffordAlgebra.finrank_pos {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) [Nontrivial R] [Module.Free R M] [Module.Finite R M] : 0 < Module.finrank R (CliffordAlgebra Q)

A Clifford algebra of a finite free module has positive rank, its rank being a power of two.

theorem CliffordAlgebra.two_mul_finrank_evenOdd {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Nontrivial V] [Module.Finite K (CliffordAlgebra Q)] (i : ZMod 2) : 2 * Module.finrank K ↥(evenOdd Q i) = Module.finrank K (CliffordAlgebra Q)

Each half of the ℤ/2-grading is exactly half of the Clifford algebra, over a field and for a nonzero space, whatever the quadratic form.

The two halves are complementary (CliffordAlgebra.evenOdd_isCompl), so their dimensions add up to the whole; and they are equidimensional by CliffordAlgebra.nonempty_evenOddEquivAddOne, which produces an odd linear automorphism out of a vector and a linear functional rather than out of an anisotropic vector, so it covers the zero form — the exterior algebra — as well. The hypothesis V ≠ 0 cannot be dropped: for V = 0 the Clifford algebra is K and entirely even.

Nothing here needs 2 to be invertible; that hypothesis enters only with CliffordAlgebra.finrank_eq_two_pow, which evaluates the right-hand side.

theorem CliffordAlgebra.finrank_evenOdd_of_finrank_eq_two_pow {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Nontrivial V] [Module.Finite K (CliffordAlgebra Q)] {n : ℕ} (hn : 0 < n) (hQ : Module.finrank K (CliffordAlgebra Q) = 2 ^ n) (i : ZMod 2) : Module.finrank K ↥(evenOdd Q i) = 2 ^ (n - 1)

Half of a power of two is one power of two down. Whenever the Clifford algebra of a nonzero space is counted by a positive power of two, CliffordAlgebra.two_mul_finrank_evenOdd splits that count and each half of the ℤ/2-grading has dimension 2 ^ (n - 1).

The count of the whole algebra is left as a hypothesis because there are two sources for it, with different requirements: CliffordAlgebra.finrank_eq_two_pow for an arbitrary quadratic form, which needs 2 to be invertible, and the exterior-algebra count for the zero form, which does not.

theorem CliffordAlgebra.finrank_evenOdd {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] [Module.Finite K V] [Nontrivial V] (i : ZMod 2) : Module.finrank K ↥(evenOdd Q i) = 2 ^ (Module.finrank K V - 1)

Over a field in which 2 is invertible, each half of the ℤ/2-grading of the Clifford algebra of a nonzero finite-dimensional space has half the dimension of the whole: 2 ^ (n - 1) for n = finrank K V. The invertibility of 2 is inherited from CliffordAlgebra.finrank_eq_two_pow, which counts the whole algebra; the halving itself is CliffordAlgebra.two_mul_finrank_evenOdd and needs no hypothesis on the quadratic form.

theorem CliffordAlgebra.finrank_evenOdd_zero {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Module.Finite K V] [Nontrivial V] (i : ZMod 2) : Module.finrank K ↥(evenOdd 0 i) = 2 ^ (Module.finrank K V - 1)

Each half of an exterior algebra has dimension 2 ^ (n - 1): the Clifford algebra of the zero form on a nonzero finite-dimensional space is the exterior algebra, whose total dimension 2 ^ n is TauCeti.ExteriorAlgebra.finrank_eq_two_pow — available over every field. So unlike CliffordAlgebra.finrank_evenOdd, this needs no invertibility of 2.

This is the count behind the two half-spin summands ⋀ᵉᵛᵉⁿ W and ⋀ᵒᵈᵈ W of a spinor module.

theorem CliffordAlgebra.finrank_even {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [Invertible 2] [Module.Finite K V] [Nontrivial V] : Module.finrank K ↥(even Q) = 2 ^ (Module.finrank K V - 1)

Over a field in which 2 is invertible, the even Clifford algebra of a nonzero finite-dimensional space has dimension 2 ^ (n - 1), one power of two below the whole algebra. This is the dimension count behind the identification of the even subalgebra with a product of two matrix algebras one size down.