Splitting a Clifford algebra along a central odd square root of one

An element ω of CliffordAlgebra Q which is central, odd, and squares to 1 splits the algebra in two. The elements

e₊ = ½ (1 + ω), e₋ = ½ (1 - ω)

are complementary orthogonal idempotents — central as soon as ω is, and that much is general algebra, recorded for an arbitrary R-algebra in TauCeti/RingTheory/Idempotents/SquareRootOne.lean — and the resulting decomposition Cliff(Q) = e₊ Cliff(Q) ⊕ e₋ Cliff(Q) has both summands isomorphic to the even subalgebra: the map

CliffordAlgebra.ofEvenProd : even Q × even Q →ₐ[R] CliffordAlgebra Q, (x, y) ↦ e₊ x + e₋ y

is an isomorphism of R-algebras. That is the content of this file, and it needs nothing beyond 2 being invertible — no field, no finiteness, no nondegeneracy. Centrality is more than the proofs use: multiplication only ever moves ω past even elements, so the declarations below ask only that ω commute with even Q, and it is the volume element application that supplies a genuinely central ω.

Both halves of the proof are short once the grade involution CliffordAlgebra.involute is brought in. Injectivity is the statement that an even x with e₊ x = 0 vanishes: from x + ω x = 0, applying involute (which fixes x and negates ω) gives x - ω x = 0, and adding the two kills ω and leaves 2 x = 0. Surjectivity never mentions dimensions either: the image of an algebra map is a subalgebra, the generators ι Q v are in it because

e₊ (ω · ι Q v) + e₋ (-(ω · ι Q v)) = (e₊ - e₋) · ω · ι Q v = ω² · ι Q v = ι Q v

with ω · ι Q v even, and CliffordAlgebra.adjoin_range_ι says the generators generate.

The element the theorem is meant for is the volume element of TauCeti/LinearAlgebra/CliffordAlgebra/VolumeElement.lean: the ordered product ω = v₁ ⋯ vₙ of a pairwise orthogonal spanning list of odd length is central (CliffordAlgebra.prod_map_ι_mem_center_of_odd_length) and odd, and its square is the scalar (-1) ^ (n.choose 2) ∏ᵢ Q vᵢ (CliffordAlgebra.prod_map_ι_sq_scalar). Rescaling ω by a scalar s whose square inverts that constant normalizes the square to 1, which is what CliffordAlgebra.equivEvenProdOfOddLength asks for; over a separably closed field of characteristic not two the rescaling always exists, and CliffordAlgebra.nonempty_algEquiv_even_prod_of_isSepClosed drops the hypothesis in favour of the orthogonal basis having no isotropic vector.

Only the odd case splits this way. For a list of even length the volume element anticommutes with the generators coming from the span of the list rather than commuting with them (CliffordAlgebra.prod_map_ι_mul_ι_of_even_length). Anticommutation does not by itself rule out centrality — in an exterior algebra the volume element annihilates the generators and is central all the same, as VolumeElement.lean records — but it does rule it out under the hypotheses this file works with: were an even-length ω with ω * ω = 1 central, then 2 being invertible would give ι Q m * ω = 0, hence ι Q m = ι Q m * ω * ω = 0, for every m in the span of the list. The even-dimensional Clifford algebra over a separably closed field is instead a matrix algebra, proved from the spin module in TauCeti/RepresentationTheory/Spin/Structure.lean. Combining that file's even-dimensional structure theorem with the splitting below is what turns an odd-dimensional Clifford algebra into a product of two matrix algebras; the identification of even Q for an odd-dimensional form with the Clifford algebra of an even-dimensional one is a separate step and is not carried out here.

Main definitions

• CliffordAlgebra.ofEvenProd: the algebra map (x, y) ↦ e₊ x + e₋ y from two copies of the even subalgebra, built on TauCeti.halfOneAdd.
• CliffordAlgebra.equivEvenProd: the splitting, that map promoted to an algebra isomorphism and read as CliffordAlgebra Q ≃ₐ[R] even Q × even Q.
• CliffordAlgebra.equivEvenProdOfOddLength: the splitting run on the volume element of a pairwise orthogonal spanning list of odd length, once its square has been normalized.

Main results

• CliffordAlgebra.eq_zero_of_mem_even_of_halfOneAdd_mul_eq_zero: an even element killed by e₊ is zero — the grade involution argument that makes the splitting injective.
• CliffordAlgebra.ofEvenProd_injective and CliffordAlgebra.ofEvenProd_surjective: the two halves of CliffordAlgebra.equivEvenProd.
• CliffordAlgebra.coe_equivEvenProd_apply_fst and CliffordAlgebra.coe_equivEvenProd_apply_snd: the forward direction of the splitting, x ↦ (e₊ x + e₋ x̂, e₋ x + e₊ x̂) with x̂ the grade involution of x.
• CliffordAlgebra.nonempty_algEquiv_even_prod_of_isSepClosed: over a separably closed field of characteristic not two, an orthogonal spanning list of odd length with no isotropic member always normalizes, so the Clifford algebra is a product of two copies of its even subalgebra. The scalar rescaling comes from an existential there, which is why this one is a Nonempty statement rather than a definition.
• CliffordAlgebra.nonempty_algEquiv_even_prod_of_odd_finrank: the same conclusion for a nondegenerate form on a finite-dimensional space of odd dimension, the orthogonal spanning list being supplied by QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho.

Implementation notes

CliffordAlgebra.equivEvenProd is oriented CliffordAlgebra Q ≃ₐ[R] even Q × even Q, matching CliffordAlgebra.equivEven and the direction in which the structure theorem is usually quoted; its underlying algebra map CliffordAlgebra.ofEvenProd runs the other way, which is the direction in which the formula (x, y) ↦ e₊ x + e₋ y is the readable one, so that formula is stated for .symm. The forward direction is read off the same two idempotents together with the grade involution, one lemma per component, stated at the level of the underlying Clifford element so that no membership proof has to appear in the statement.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 1, "The odd-dimensional case": the two central idempotents split the odd Clifford algebra, while the even subalgebra stays a single block.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry, Princeton University Press (1989), Chapter I, Proposition 3.7 and Theorem 4.3.
• C. Chevalley, The Algebraic Theory of Spinors, Columbia University Press (1954), Chapter II.

The splitting

theorem CliffordAlgebra.eq_zero_of_mem_even_of_halfOneAdd_mul_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hodd : ω ∈ evenOdd Q 1) {x : CliffordAlgebra Q} (hx : x ∈ evenOdd Q 0) (h : TauCeti.halfOneAdd R ω * x = 0) : x = 0

An even element annihilated by ½ (1 + ω) vanishes, for ω odd.

The grade involution fixes x and negates ω, so from x + ω x = 0 it produces x - ω x = 0; the two together give 2 x = 0. Nothing else about ω is used, so the same statement at -ω covers the complementary idempotent.

noncomputable def CliffordAlgebra.ofEvenProd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hsq : ω * ω = 1) : ↥(even Q) × ↥(even Q) →ₐ[R] CliffordAlgebra Q

The splitting map: (x, y) ↦ ½ (1 + ω) x + ½ (1 - ω) y from two copies of the even subalgebra to the whole Clifford algebra, for an ω squaring to 1 which commutes with the even subalgebra. Multiplication only ever moves ω past the two even components, so commutation with even Q is all that is asked; a central ω — the case the volume element supplies — is a special case.

The proofs are Prop arguments, so two instances built from different proofs of the same hypotheses are equal by proof irrelevance.

Equations

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

@[simp]

theorem CliffordAlgebra.ofEvenProd_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hsq : ω * ω = 1) (p : ↥(even Q) × ↥(even Q)) : (ofEvenProd Q ω hcomm hsq) p = TauCeti.halfOneAdd R ω * ↑p.1 + TauCeti.halfOneAdd R (-ω) * ↑p.2

theorem CliffordAlgebra.ofEvenProd_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) : Function.Injective ⇑(ofEvenProd Q ω hcomm hsq)

The splitting map is injective: multiplying by one idempotent isolates one component, and CliffordAlgebra.eq_zero_of_mem_even_of_halfOneAdd_mul_eq_zero kills it.

theorem CliffordAlgebra.ofEvenProd_surjective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) : Function.Surjective ⇑(ofEvenProd Q ω hcomm hsq)

The splitting map is surjective: its range is a subalgebra containing every generator ι Q v, because ω · ι Q v is even and (e₊ - e₋) ω = ω² = 1.

theorem CliffordAlgebra.ofEvenProd_bijective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) : Function.Bijective ⇑(ofEvenProd Q ω hcomm hsq)

The two halves together: the splitting map is bijective.

noncomputable def CliffordAlgebra.equivEvenProd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) : CliffordAlgebra Q ≃ₐ[R] ↥(even Q) × ↥(even Q)

The splitting: an odd ω with ω * ω = 1 commuting with the even subalgebra presents the Clifford algebra as two copies of that subalgebra, glued along the complementary idempotents ½ (1 ± ω).

Equations

• CliffordAlgebra.equivEvenProd Q ω hcomm hodd hsq = (AlgEquiv.ofBijective (CliffordAlgebra.ofEvenProd Q ω hcomm hsq) ⋯).symm

@[simp]

theorem CliffordAlgebra.equivEvenProd_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) (p : ↥(even Q) × ↥(even Q)) : (equivEvenProd Q ω hcomm hodd hsq).symm p = TauCeti.halfOneAdd R ω * ↑p.1 + TauCeti.halfOneAdd R (-ω) * ↑p.2

theorem CliffordAlgebra.involute_halfOneAdd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hodd : ω ∈ evenOdd Q 1) : involute (TauCeti.halfOneAdd R ω) = TauCeti.halfOneAdd R (-ω)

The grade involution swaps the two idempotents, for ω odd.

theorem CliffordAlgebra.involute_halfOneAdd_neg {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hodd : ω ∈ evenOdd Q 1) : involute (TauCeti.halfOneAdd R (-ω)) = TauCeti.halfOneAdd R ω

The grade involution swaps the two idempotents, read in the other direction.

@[simp]

theorem CliffordAlgebra.coe_equivEvenProd_apply_fst {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) (x : CliffordAlgebra Q) : ↑((equivEvenProd Q ω hcomm hodd hsq) x).1 = TauCeti.halfOneAdd R ω * x + TauCeti.halfOneAdd R (-ω) * involute x

The first component of the splitting: x ↦ ½ (1 + ω) x + ½ (1 - ω) x̂, where x̂ is the grade involution of x. Together with CliffordAlgebra.coe_equivEvenProd_apply_snd this reads the forward direction off the same idempotents the inverse is built from.

@[simp]

theorem CliffordAlgebra.coe_equivEvenProd_apply_snd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (ω : CliffordAlgebra Q) (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) (x : CliffordAlgebra Q) : ↑((equivEvenProd Q ω hcomm hodd hsq) x).2 = TauCeti.halfOneAdd R (-ω) * x + TauCeti.halfOneAdd R ω * involute x

The second component of the splitting: x ↦ ½ (1 - ω) x + ½ (1 + ω) x̂, the first component read at -ω.

theorem CliffordAlgebra.equivEvenProd_star {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {ω : CliffordAlgebra Q} (hcomm : ∀ (x : ↥(even Q)), Commute ω ↑x) (hodd : ω ∈ evenOdd Q 1) (hsq : ω * ω = 1) (hstar : star ω = ω) (x : CliffordAlgebra Q) : (equivEvenProd Q ω hcomm hodd hsq) (star x) = ((reverseEven Q) ((equivEvenProd Q ω hcomm hodd hsq) x).1, (reverseEven Q) ((equivEvenProd Q ω hcomm hodd hsq) x).2)

A splitting element fixed by Clifford conjugation makes the odd splitting carry conjugation to componentwise reversal on the two even factors.

The volume element as the splitting element

noncomputable def CliffordAlgebra.equivEvenProdOfOddLength {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) {s : R} (hs : s * s * ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod) = 1) : CliffordAlgebra Q ≃ₐ[R] ↥(even Q) × ↥(even Q)

The odd-dimensional splitting, run on the volume element. For a pairwise orthogonal list of vectors spanning M, of odd length, whose volume element has been rescaled by s so as to square to 1, the Clifford algebra is the product of two copies of its even subalgebra.

The normalization hypothesis is exactly (s ω)² = 1 read through CliffordAlgebra.prod_map_ι_sq_scalar; it forces each Q vᵢ to be a unit, so it carries the nondegeneracy the statement needs without naming it.

Equations

• CliffordAlgebra.equivEvenProdOfOddLength hl hlen hspan hs = CliffordAlgebra.equivEvenProd Q (s • (List.map (⇑(CliffordAlgebra.ι Q)) l).prod) ⋯ ⋯ ⋯

@[simp]

theorem CliffordAlgebra.equivEvenProdOfOddLength_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) {s : R} (hs : s * s * ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod) = 1) (p : ↥(even Q) × ↥(even Q)) : (equivEvenProdOfOddLength hl hlen hspan hs).symm p = TauCeti.halfOneAdd R (s • (List.map (⇑(ι Q)) l).prod) * ↑p.1 + TauCeti.halfOneAdd R (-(s • (List.map (⇑(ι Q)) l).prod)) * ↑p.2

The inverse of CliffordAlgebra.equivEvenProdOfOddLength, read off CliffordAlgebra.equivEvenProd_symm_apply at the rescaled volume element.

@[simp]

theorem CliffordAlgebra.coe_equivEvenProdOfOddLength_apply_fst {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) {s : R} (hs : s * s * ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod) = 1) (x : CliffordAlgebra Q) : ↑((equivEvenProdOfOddLength hl hlen hspan hs) x).1 = TauCeti.halfOneAdd R (s • (List.map (⇑(ι Q)) l).prod) * x + TauCeti.halfOneAdd R (-(s • (List.map (⇑(ι Q)) l).prod)) * involute x

The first component of CliffordAlgebra.equivEvenProdOfOddLength, read off CliffordAlgebra.coe_equivEvenProd_apply_fst at the rescaled volume element.

@[simp]

theorem CliffordAlgebra.coe_equivEvenProdOfOddLength_apply_snd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) {s : R} (hs : s * s * ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod) = 1) (x : CliffordAlgebra Q) : ↑((equivEvenProdOfOddLength hl hlen hspan hs) x).2 = TauCeti.halfOneAdd R (-(s • (List.map (⇑(ι Q)) l).prod)) * x + TauCeti.halfOneAdd R (s • (List.map (⇑(ι Q)) l).prod) * involute x

The second component of CliffordAlgebra.equivEvenProdOfOddLength, read off CliffordAlgebra.coe_equivEvenProd_apply_snd at the rescaled volume element.

theorem CliffordAlgebra.equivEvenProdOfOddLength_star {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {l : List M} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span R {x : M | x ∈ l} = ⊤) {s : R} (hs : s * s * ((-1) ^ l.length.choose 2 * (List.map (⇑Q) l).prod) = 1) (hstar : star (s • (List.map (⇑(ι Q)) l).prod) = s • (List.map (⇑(ι Q)) l).prod) (x : CliffordAlgebra Q) : (equivEvenProdOfOddLength hl hlen hspan hs) (star x) = ((reverseEven Q) ((equivEvenProdOfOddLength hl hlen hspan hs) x).1, (reverseEven Q) ((equivEvenProdOfOddLength hl hlen hspan hs) x).2)

If the normalized odd volume is fixed by Clifford conjugation, its splitting carries conjugation to componentwise reversal on the two even factors.

theorem CliffordAlgebra.nonempty_algEquiv_even_prod_of_isSepClosed {K : Type u_1} {V : Type u_2} [Field K] [IsSepClosed K] [AddCommGroup V] [Module K V] [NeZero 2] {Q : QuadraticForm K V} {l : List V} (hl : List.Pairwise (QuadraticMap.IsOrtho Q) l) (hlen : Odd l.length) (hspan : Submodule.span K {x : V | x ∈ l} = ⊤) (hQ : ∀ v ∈ l, Q v ≠ 0) : Nonempty (CliffordAlgebra Q ≃ₐ[K] ↥(even Q) × ↥(even Q))

Over a separably closed field of characteristic not two the normalization is automatic.

An orthogonal spanning list of odd length with no isotropic member has a volume element whose square is a nonzero scalar, and a separably closed field supplies its inverse square root, so the Clifford algebra of such a form is the product of two copies of its even subalgebra. The square root is only known to exist, so the conclusion is a Nonempty; fixing a root and applying CliffordAlgebra.equivEvenProdOfOddLength names the isomorphism. This is the odd-dimensional half of the structure theorem, up to the identification of the even subalgebra with a matrix algebra.

theorem CliffordAlgebra.nonempty_algEquiv_even_prod_of_odd_finrank {K : Type u_1} {V : Type u_2} [Field K] [IsSepClosed K] [AddCommGroup V] [Module K V] [NeZero 2] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hV : Odd (Module.finrank K V)) : Nonempty (CliffordAlgebra Q ≃ₐ[K] ↥(even Q) × ↥(even Q))

A nondegenerate odd-dimensional Clifford algebra splits into two copies of its even subalgebra, over a separably closed field of characteristic not two. An orthogonal basis of a nondegenerate form has no isotropic member (QuadraticMap.Nondegenerate.exists_list_pairwise_isOrtho), so its volume element is a central odd element with invertible square, which is what CliffordAlgebra.nonempty_algEquiv_even_prod_of_isSepClosed asks for.