Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Prod

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: #

TODO: #

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

source
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₁.Isometry Qₙ) (f₂ : Q₂.Isometry Qₙ) (hf : ∀ (x : M₁) (y : M₂), Qₙ.IsOrtho (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ : ZMod 2} {i₂ : ZMod 2} (hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁) (hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂) :
(CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁)

If m₁ and m₂ are both homogenous, 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.

source
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₁.Isometry Qₙ) (f₂ : Q₂.Isometry Qₙ) (hf : ∀ (x : M₁) (y : M₂), Qₙ.IsOrtho (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₂ : ZMod 2} (hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ 0) (hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂) :
Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
source
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₁.Isometry Qₙ) (f₂ : Q₂.Isometry Qₙ) (hf : ∀ (x : M₁) (y : M₂), Qₙ.IsOrtho (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ : ZMod 2} (hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁) (hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ 0) :
Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
source
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₁.Isometry Qₙ) (f₂ : Q₂.Isometry Qₙ) (hf : ∀ (x : M₁) (y : M₂), Qₙ.IsOrtho (f₁ x) (f₂ y)) (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) (hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ 1) (hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ 1) :
(CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = -(CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁
source
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 (Q₁.prod Q₂) →ₐ[R] GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)

The forward direction of CliffordAlgebra.prodEquiv.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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₂) :
    (CliffordAlgebra.ofProd Q₁ Q₂) ((CliffordAlgebra.ι (Q₁.prod Q₂)) (m₁, m₂)) = (CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂
    source
    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 (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂) →ₐ[R] CliffordAlgebra (Q₁.prod Q₂)

    The reverse direction of CliffordAlgebra.prodEquiv.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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₁) :
      (CliffordAlgebra.toProd Q₁ Q₂) ((CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1) = (CliffordAlgebra.ι (Q₁.prod Q₂)) (m₁, 0)
      source
      @[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₂) :
      (CliffordAlgebra.toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂) = (CliffordAlgebra.ι (Q₁.prod Q₂)) (0, m₂)
      source
      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₂) :
      (CliffordAlgebra.toProd Q₁ Q₂).comp (CliffordAlgebra.ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (Q₁.prod Q₂))
      source
      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₂) :
      (CliffordAlgebra.ofProd Q₁ Q₂).comp (CliffordAlgebra.toProd Q₁ Q₂) = AlgHom.id R (GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂))
      source
      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 (Q₁.prod Q₂) ≃ₐ[R] GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.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
      Instances For
        source
        @[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 (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)) :
        (CliffordAlgebra.prodEquiv Q₁ Q₂).symm a = (CliffordAlgebra.toProd Q₁ Q₂) a
        source
        @[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 (Q₁.prod Q₂)) :
        (CliffordAlgebra.prodEquiv Q₁ Q₂) a = (CliffordAlgebra.ofProd Q₁ Q₂) a