Reading the ℤ/2-grading: base cases, exterior bases, and ordered products

An induction over the ℤ/2-grading of a Clifford algebra — Mathlib's CliffordAlgebra.evenOdd_induction — hands its base case back as membership in a power of LinearMap.range (ι Q) whose exponent is a ZMod.val. Since (0 : ZMod 2).val is 0 and (1 : ZMod 2).val is 1, that membership says "a scalar" in the even case and "a vector" in the odd one. Reading it that way is bookkeeping that every such induction repeats, so it is recorded here once and shared.

In the other direction, the ordered product (l.map (ι Q)).prod of a list of vectors — the spelling TauCeti/LinearAlgebra/CliffordAlgebra/VolumeElement.lean uses for the volume element — is homogeneous of degree l.length, which is Mathlib's SetLike.list_prod_map_mem_graded for the graded monoid CliffordAlgebra.evenOdd Q with the degree of each factor read off CliffordAlgebra.ι_mem_evenOdd_one. Reading it off by the parity of the length is what matters downstream.

The coordinate basis of an exterior algebra is homogeneous for this grading: the basis vector indexed by s has degree s.card, and — over a nontrivial ring, where a basis vector is nonzero and the two graded pieces meet only in 0 — that degree is the only one it has. This statement belongs to the grading API independently of any spin representation.

Main results

• CliffordAlgebra.exists_algebraMap_of_mem_range_ι_pow_zero: in the even base case the element is a scalar.
• CliffordAlgebra.exists_ι_of_mem_range_ι_pow_one: in the odd base case it is a vector.
• CliffordAlgebra.ι_range_pow_le_evenOdd: the n-th power of the range of ι lies in the graded piece of degree n.
• CliffordAlgebra.prod_map_ι_mem_evenOdd: an ordered product of n generators is homogeneous of degree n, and CliffordAlgebra.prod_map_ι_mem_evenOdd_zero_of_even_length and CliffordAlgebra.prod_map_ι_mem_evenOdd_one_of_odd_length read that off in the even and the odd case.
• Module.Basis.exteriorAlgebra_mem_evenOdd_card: an exterior coordinate-basis vector is homogeneous of degree given by the cardinality of its index set, and Module.Basis.exteriorAlgebra_mem_evenOdd_iff says that this is the only degree it has.
• Module.Basis.mem_evenOdd_iff_exteriorAlgebra_repr_eq_zero: an exterior element is homogeneous of a given parity exactly when its coordinates vanish at every index set of the other parity.

theorem CliffordAlgebra.exists_algebraMap_of_mem_range_ι_pow_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {v : CliffordAlgebra Q} (hv : v ∈ (ι Q).range ^ ZMod.val 0) : ∃ (r : R), (algebraMap R (CliffordAlgebra Q)) r = v

An element of the (0 : ZMod 2).val-th power of the range of ι is a scalar. This is the i = 0 half of the range_ι_pow hypothesis of CliffordAlgebra.evenOdd_induction.

theorem CliffordAlgebra.exists_ι_of_mem_range_ι_pow_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {v : CliffordAlgebra Q} (hv : v ∈ (ι Q).range ^ ZMod.val 1) : ∃ (a : M), (ι Q) a = v

An element of the (1 : ZMod 2).val-th power of the range of ι is a vector. This is the i = 1 half of the range_ι_pow hypothesis of CliffordAlgebra.evenOdd_induction.

theorem CliffordAlgebra.ι_range_pow_le_evenOdd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (n : ℕ) : (ι Q).range ^ n ≤ evenOdd Q ↑n

The n-th power of the vectors is homogeneous of degree n for the ℤ/2 grading: it is one of the summands defining CliffordAlgebra.evenOdd Q n.

theorem CliffordAlgebra.prod_map_ι_mem_evenOdd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (l : List M) : (List.map (⇑(ι Q)) l).prod ∈ evenOdd Q ↑l.length

An ordered product of n generators is homogeneous of degree n for the ℤ/2 grading.

theorem CliffordAlgebra.prod_map_ι_mem_evenOdd_zero_of_even_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hlen : Even l.length) : (List.map (⇑(ι Q)) l).prod ∈ evenOdd Q 0

The ordered product of an even number of vectors is even.

theorem CliffordAlgebra.prod_map_ι_mem_evenOdd_one_of_odd_length {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {l : List M} (hlen : Odd l.length) : (List.map (⇑(ι Q)) l).prod ∈ evenOdd Q 1

The ordered product of an odd number of vectors is odd.

@[simp]

theorem Module.Basis.exteriorAlgebra_mem_evenOdd_card {R : Type u} {M : Type v} {I : Type w} [CommRing R] [AddCommGroup M] [Module R M] [LinearOrder I] (b : Basis I R M) (s : Finset I) : b.ExteriorAlgebra s ∈ CliffordAlgebra.evenOdd 0 ↑s.card

An exterior coordinate-basis vector is homogeneous of degree its number of coordinates.

@[simp]

theorem Module.Basis.exteriorAlgebra_mem_evenOdd_iff {R : Type u} {M : Type v} {I : Type w} [CommRing R] [AddCommGroup M] [Module R M] [LinearOrder I] [Nontrivial R] (b : Basis I R M) (s : Finset I) (i : ZMod 2) : b.ExteriorAlgebra s ∈ CliffordAlgebra.evenOdd 0 i ↔ ↑s.card = i

An exterior coordinate-basis vector is homogeneous of exactly one degree: it lies in the graded piece i precisely when i is the parity of its number of coordinates.

theorem Module.Basis.mem_evenOdd_iff_exteriorAlgebra_repr_eq_zero {R : Type u} {M : Type v} {I : Type w} [CommRing R] [AddCommGroup M] [Module R M] [LinearOrder I] (b : Basis I R M) {i : ZMod 2} {x : _root_.ExteriorAlgebra R M} : x ∈ CliffordAlgebra.evenOdd 0 i ↔ ∀ (t : Finset I), ↑t.card ≠ i → (b.ExteriorAlgebra.repr x) t = 0

An exterior element is homogeneous of parity i exactly when it has no coordinates of the other parity: its coordinate in the exterior coordinate basis vanishes at every index set whose cardinality has the other parity.