Clifford algebras of a direct sum of two vector spaces

We show that the Clifford algebra of a direct sum is the graded tensor product of the Clifford algebras, as CliffordAlgebra.equivProd.

Main definitions:

• CliffordAlgebra.equivProd : CliffordAlgebra (Q₁.prod Q₂) ≃ₐ[R] (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)

TODO

Introduce morphisms and equivalences of graded algebas, and upgrade CliffordAlgebra.equivProd to a graded algebra equivalence.

theorem CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ) (f₂ : Q₂ →qᵢ Qₙ) (hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ i₂ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ i₁) (hm₂ : m₂ ∈ evenOdd Q₂ i₂) : (map f₁) m₁ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁)

If m₁ and m₂ are both homogeneous, and the quadratic spaces Q₁ and Q₂ map into orthogonal subspaces of Qₙ (for instance, when Qₙ = Q₁.prod Q₂), then the product of the embedding in CliffordAlgebra Q commutes up to a sign factor.

theorem CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ) (f₂ : Q₂ →qᵢ Qₙ) (hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₂ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ 0) (hm₂ : m₂ ∈ evenOdd Q₂ i₂) : Commute ((map f₁) m₁) ((map f₂) m₂)

theorem CliffordAlgebra.commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ) (f₂ : Q₂ →qᵢ Qₙ) (hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ i₁) (hm₂ : m₂ ∈ evenOdd Q₂ 0) : Commute ((map f₁) m₁) ((map f₂) m₂)

theorem CliffordAlgebra.map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ) (f₂ : Q₂ →qᵢ Qₙ) (hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) (hm₁ : m₁ ∈ evenOdd Q₁ 1) (hm₂ : m₂ ∈ evenOdd Q₂ 1) : (map f₁) m₁ * (map f₂) m₂ = -(map f₂) m₂ * (map f₁) m₁

noncomputable def CliffordAlgebra.ofProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂) →ₐ[R] GradedTensorProduct R (evenOdd Q₁) (evenOdd Q₂)

The forward direction of CliffordAlgebra.prodEquiv.

Equations

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

@[simp]

theorem CliffordAlgebra.ofProd_ι_mk {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : (ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) = (ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m₂

noncomputable def CliffordAlgebra.toProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : GradedTensorProduct R (evenOdd Q₁) (evenOdd Q₂) →ₐ[R] CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)

The reverse direction of CliffordAlgebra.prodEquiv.

Equations

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

@[simp]

theorem CliffordAlgebra.toProd_ι_tmul_one {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) : (toProd Q₁ Q₂) ((ι Q₁) m₁ ᵍ⊗ₜ[R] 1) = (ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)

@[simp]

theorem CliffordAlgebra.toProd_one_tmul_ι {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (m₂ : M₂) : (toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (ι Q₂) m₂) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)

theorem CliffordAlgebra.toProd_comp_ofProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))

theorem CliffordAlgebra.ofProd_comp_toProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : (ofProd Q₁ Q₂).comp (toProd Q₁ Q₂) = AlgHom.id R (GradedTensorProduct R (evenOdd Q₁) (evenOdd Q₂))

noncomputable def CliffordAlgebra.prodEquiv {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂) ≃ₐ[R] GradedTensorProduct R (evenOdd Q₁) (evenOdd Q₂)

The Clifford algebra over an orthogonal direct sum of quadratic vector spaces is isomorphic as an algebra to the graded tensor product of the Clifford algebras of each space.

This is CliffordAlgebra.toProd and CliffordAlgebra.ofProd as an equivalence.

Equations

• CliffordAlgebra.prodEquiv Q₁ Q₂ = AlgEquiv.ofAlgHom (CliffordAlgebra.ofProd Q₁ Q₂) (CliffordAlgebra.toProd Q₁ Q₂) ⋯ ⋯

@[simp]

theorem CliffordAlgebra.prodEquiv_symm_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (a : GradedTensorProduct R (evenOdd Q₁) (evenOdd Q₂)) : (prodEquiv Q₁ Q₂).symm a = (toProd Q₁ Q₂) a

@[simp]

theorem CliffordAlgebra.prodEquiv_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)) : (prodEquiv Q₁ Q₂) a = (ofProd Q₁ Q₂) a