Functoriality of Clifford algebras

This file records structural properties of the algebra map induced by a quadratic isometry. Such maps commute with Clifford conjugation and preserve the even subalgebra. For an orthogonal product, the map induced by the left-summand inclusion is injective when the left Clifford algebra is flat and scalar action on the right Clifford algebra is faithful.

Main results

• CliffordAlgebra.map_involute proves naturality of the grade involution.
• CliffordAlgebra.map_reverse proves naturality of Clifford reversal.
• CliffordAlgebra.map_star proves naturality of Clifford conjugation.
• CliffordAlgebra.map_mem_even proves preservation of the even subalgebra.
• CliffordAlgebra.evenEquivOfIsometry restricts an isometry-induced equivalence to the even subalgebras, with coercion and generator-level transport equations.
• CliffordAlgebra.map_inl_injective proves injectivity for a left orthogonal summand.

@[simp]

theorem CliffordAlgebra.map_involute {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : CliffordAlgebra Q₁) : (map f) (involute x) = involute ((map f) x)

The grade involution commutes with the algebra map induced by a quadratic isometry.

@[simp]

theorem CliffordAlgebra.map_reverse {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : CliffordAlgebra Q₁) : (map f) (reverse x) = reverse ((map f) x)

Clifford reversal commutes with the algebra map induced by a quadratic isometry.

@[simp]

theorem CliffordAlgebra.map_star {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : CliffordAlgebra Q₁) : (map f) (star x) = star ((map f) x)

Clifford conjugation commutes with the algebra map induced by a quadratic isometry.

theorem CliffordAlgebra.map_mem_even {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) {x : CliffordAlgebra Q₁} (hx : x ∈ even Q₁) : (map f) x ∈ even Q₂

A quadratic isometry sends the even Clifford subalgebra into the even Clifford subalgebra.

theorem CliffordAlgebra.map_equivOfIsometry_even {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : Subalgebra.map (↑(equivOfIsometry e)) (even Q₁) = even Q₂

An isometry equivalence maps the even Clifford subalgebra onto the even Clifford subalgebra.

noncomputable def CliffordAlgebra.evenEquivOfIsometry {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : ↥(even Q₁) ≃ₐ[R] ↥(even Q₂)

The Clifford-algebra equivalence induced by a quadratic isometry equivalence, restricted to the even subalgebras.

Equations

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

@[simp]

theorem CliffordAlgebra.coe_evenEquivOfIsometry_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (x : ↥(even Q₁)) : ↑((evenEquivOfIsometry e) x) = (equivOfIsometry e) ↑x

After coercion, evenEquivOfIsometry agrees with the full Clifford-algebra equivalence.

@[simp]

theorem CliffordAlgebra.evenEquivOfIsometry_ι {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (m n : M₁) : (evenEquivOfIsometry e) (((even.ι Q₁).bilin m) n) = ((even.ι Q₂).bilin (e m)) (e n)

On a bilinear generator, the restricted equivalence applies the isometry to both vectors.

@[simp]

theorem CliffordAlgebra.evenEquivOfIsometry_symm {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) : (evenEquivOfIsometry e).symm = evenEquivOfIsometry e.symm

The inverse of an isometry-induced even Clifford equivalence is induced by the inverse isometry.

@[simp]

theorem CliffordAlgebra.evenEquivOfIsometry_trans {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {M₃ : Type u_1} [AddCommGroup M₃] [Module R M₃] {Q₃ : QuadraticForm R M₃} (e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂) (e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃) : (evenEquivOfIsometry e₁₂).trans (evenEquivOfIsometry e₂₃) = evenEquivOfIsometry (e₁₂.trans e₂₃)

Restriction to even Clifford algebras respects composition of isometry equivalences.

@[simp]

theorem CliffordAlgebra.evenEquivOfIsometry_refl {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {Q₁ : QuadraticForm R M₁} : evenEquivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

The identity isometry induces the identity on the even Clifford algebra.

@[simp]

theorem CliffordAlgebra.equivEven_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (Q : QuadraticForm R M₁) (x : CliffordAlgebra Q) : (equivEven Q) x = (toEven Q) x

The standard dimension-shift equivalence applies its defining algebra homomorphism.

@[simp]

theorem CliffordAlgebra.equivEven_symm_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (Q : QuadraticForm R M₁) (x : ↥(even (EquivEven.Q' Q))) : (equivEven Q).symm x = (ofEven Q) x

The inverse standard dimension-shift equivalence applies its defining algebra homomorphism.

theorem CliffordAlgebra.map_inl_injective {K : Type u} [CommRing K] {N₁ : Type v} [AddCommGroup N₁] [Module K N₁] {N₂ : Type w} [AddCommGroup N₂] [Module K N₂] (P₁ : QuadraticForm K N₁) (P₂ : QuadraticForm K N₂) [Module.Flat K (CliffordAlgebra P₁)] [FaithfulSMul K (CliffordAlgebra P₂)] : Function.Injective ⇑(map (QuadraticMap.Isometry.inl P₁ P₂))

The Clifford-algebra map induced by the inclusion of the left summand of an orthogonal product is injective when the left Clifford algebra is flat and scalar action on the right Clifford algebra is faithful.