The quadratic elements of a Clifford algebra as a Lie subalgebra

A Clifford algebra is an associative algebra, so its commutator makes it a Lie algebra. Inside it the quadratic elements — the span of the half-normalized commutators CliffordAlgebra.bivector Q a b of two generators — are closed under the bracket, and this file equips them with the resulting LieSubalgebra structure.

Closure is a two-line consequence of the action-normalization identity CliffordAlgebra.bivector_lie_ι, which says that a Clifford bivector brackets a generator to the infinitesimal rotation x ↦ polar Q b x • a - polar Q a x • b. Because bracketing with a fixed element is a derivation for the associative product, the bracket of two Clifford bivectors is obtained by rotating each of the two generators of the second one in turn, so it is again a sum of two Clifford bivectors (CliffordAlgebra.lie_bivector_bivector).

Nothing here needs the quadratic form to be nondegenerate, the module to be finite-dimensional, or the base to be a field: the statements hold over any commutative ring in which 2 is invertible. The identification of this subalgebra with 𝔰𝔬(V, Q) — Mathlib's skewAdjointLieSubalgebra (QuadraticMap.polarBilin Q) — does need those hypotheses, and is not proved here; the bridging fact this file does supply is that a quadratic element brackets every generator back into the generators (CliffordAlgebra.lie_ι_mem_range_ι_of_mem_quadraticLieSubalgebra), which is what makes that comparison map exist at all.

Following Mathlib's Mathlib/Algebra/Lie/SkewAdjoint.lean, the Lie ring structure on an associative ring is a local instance (LieRing.ofAssociativeRing): it cannot be global, since it would clash with the module bracket when a ring is regarded as a module over itself. A downstream file that states results about quadraticLieSubalgebra therefore has to put the same attribute in scope.

Main definitions

• CliffordAlgebra.quadraticLieSubalgebra: the quadratic elements of CliffordAlgebra Q, as a Lie subalgebra under the commutator bracket.

Main results

• CliffordAlgebra.lie_bivector_bivector: the bracket of two Clifford bivectors, as a sum of two Clifford bivectors.
• CliffordAlgebra.lie_ι_mul_ι_ι_mul_ι: the integral commutator formula for two products of Clifford generators.
• CliffordAlgebra.quadraticLieSubalgebra_toSubmodule_le_of_bivector_mem: the universal property of the underlying submodule, from which the containments below are read off.
• CliffordAlgebra.quadraticLieSubalgebra_le_evenOdd_zero, CliffordAlgebra.quadraticLieSubalgebra_le_even and CliffordAlgebra.quadraticLieSubalgebra_le_filtration_two: the quadratic elements are even and have filtration degree at most two.
• CliffordAlgebra.quadraticLieSubalgebra_toSubmodule_eq_range and CliffordAlgebra.mem_quadraticLieSubalgebra_iff: they are exactly the image of ⋀[R]^2 M under CliffordAlgebra.bivectorExterior.
• CliffordAlgebra.lie_ι_mem_range_ι_of_mem_quadraticLieSubalgebra: bracketing with a quadratic element preserves the generators.
• CliffordAlgebra.adjoin_quadraticLieSubalgebra and CliffordAlgebra.adjoin_coe_preimage_quadraticLieSubalgebra_eq_top: the quadratic elements generate the even subalgebra as an algebra.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 9, "the abstract quadratic realization".

theorem CliffordAlgebra.lie_ι_mul_ι_ι_mul_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x y z w : M) : ⁅(ι Q) x * (ι Q) y, (ι Q) z * (ι Q) w⁆ = QuadraticMap.polar (⇑Q) z y • ((ι Q) x * (ι Q) w) - QuadraticMap.polar (⇑Q) z x • ((ι Q) y * (ι Q) w) + QuadraticMap.polar (⇑Q) w y • ((ι Q) z * (ι Q) x) - QuadraticMap.polar (⇑Q) x w • ((ι Q) z * (ι Q) y)

The commutator of two products of Clifford generators, in a form that does not divide by 2.

theorem CliffordAlgebra.lie_bivector_bivector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (a b c d : M) : ⁅bivector Q a b, bivector Q c d⁆ = bivector Q (QuadraticMap.polar (⇑Q) b c • a - QuadraticMap.polar (⇑Q) a c • b) d + bivector Q c (QuadraticMap.polar (⇑Q) b d • a - QuadraticMap.polar (⇑Q) a d • b)

The bracket of two Clifford bivectors. Bracketing with bivector Q a b is a derivation which rotates a generator by x ↦ polar Q b x • a - polar Q a x • b, so it takes the Clifford bivector of (c, d) to the sum of the Clifford bivectors of the two rotated pairs. This is the closure property that makes the quadratic elements a Lie subalgebra.

noncomputable def CliffordAlgebra.quadraticLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : LieSubalgebra R (CliffordAlgebra Q)

The quadratic elements of a Clifford algebra, as a Lie subalgebra of CliffordAlgebra Q under the commutator bracket: the R-span of the Clifford bivectors CliffordAlgebra.bivector Q a b.

Unlike a transported bracket on ⋀[R]^2 M, this is a subobject of the Clifford algebra itself, so it needs no scoped instances beyond the local LieRing.ofAssociativeRing on an associative ring.

Equations

• CliffordAlgebra.quadraticLieSubalgebra Q = { toSubmodule := Submodule.span R (CliffordAlgebra.bivectorSet✝ Q), lie_mem' := ⋯ }

theorem CliffordAlgebra.quadraticLieSubalgebra_toSubmodule {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (quadraticLieSubalgebra Q).toSubmodule = Submodule.span R (Set.range fun (p : M × M) => bivector Q p.1 p.2)

The definitional pin: the quadratic elements are the span of the Clifford bivectors.

theorem CliffordAlgebra.bivector_mem_quadraticLieSubalgebra {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 ∈ quadraticLieSubalgebra Q

Every Clifford bivector is a quadratic element.

theorem CliffordAlgebra.quadraticLieSubalgebra_toSubmodule_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) : (quadraticLieSubalgebra Q).toSubmodule ≤ P

The universal property of the quadratic elements: any submodule containing every Clifford bivector contains them all. Every containment below is an instance of this.

theorem CliffordAlgebra.quadraticLieSubalgebra_le_evenOdd_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (quadraticLieSubalgebra Q).toSubmodule ≤ evenOdd Q 0

The quadratic elements are even.

theorem CliffordAlgebra.quadraticLieSubalgebra_le_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (quadraticLieSubalgebra Q).toSubmodule ≤ Subalgebra.toSubmodule (even Q)

The quadratic elements lie in the even subalgebra.

theorem CliffordAlgebra.quadraticLieSubalgebra_le_filtration_two {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (quadraticLieSubalgebra Q).toSubmodule ≤ filtration Q 2

The quadratic elements have filtration degree at most two.

@[simp]

theorem CliffordAlgebra.adjoin_quadraticLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Algebra.adjoin R ↑(quadraticLieSubalgebra Q) = even Q

The quadratic elements generate the even subalgebra. A product ι a * ι b of two generators is its Clifford bivector plus a scalar (CliffordAlgebra.ι_mul_ι_eq_bivector_add), and those products generate the even part.

@[simp]

theorem CliffordAlgebra.adjoin_coe_preimage_quadraticLieSubalgebra_eq_top {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : Algebra.adjoin R (Subtype.val ⁻¹' ↑(quadraticLieSubalgebra Q)) = ⊤

The quadratic elements generate the even subalgebra from within: regarded as elements of even Q, they generate all of it. This is the form in which a representation of the even subalgebra is determined by its values on the quadratic elements.

theorem CliffordAlgebra.quadraticLieSubalgebra_toSubmodule_eq_range {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : (quadraticLieSubalgebra Q).toSubmodule = (bivectorExterior Q).range

The quadratic elements are the image of the second exterior power. This is the sense in which the Lie subalgebra realizes ⋀[R]^2 M inside the Clifford algebra; the map itself is CliffordAlgebra.bivectorExterior.

@[simp]

theorem CliffordAlgebra.mem_quadraticLieSubalgebra_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : CliffordAlgebra Q} : x ∈ quadraticLieSubalgebra Q ↔ x ∈ (bivectorExterior Q).range

Membership in the quadratic elements: an element of the Clifford algebra is quadratic exactly when it is in the image of ⋀[R]^2 M under CliffordAlgebra.bivectorExterior.

theorem CliffordAlgebra.lie_ι_mem_range_ι_of_mem_quadraticLieSubalgebra {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : CliffordAlgebra Q} (hx : x ∈ quadraticLieSubalgebra Q) (m : M) : ⁅x, (ι Q) m⁆ ∈ (ι Q).range

Quadratic elements preserve the generators. Bracketing with a quadratic element sends ι Q m back into the image of ι Q; on the span of the generators it is therefore an endomorphism, which is what the comparison with the skew-adjoint endomorphisms of QuadraticMap.polarBilin Q is built from.