# Isomorphisms with the even subalgebra of a Clifford algebra #

This file provides some notable isomorphisms regarding the even subalgebra, CliffordAlgebra.even.

## Main definitions #

• CliffordAlgebra.equivEven: Every Clifford algebra is isomorphic as an algebra to the even subalgebra of a Clifford algebra with one more dimension.

• CliffordAlgebra.EquivEven.Q': The quadratic form used by this "one-up" algebra.
• CliffordAlgebra.toEven: The simp-normal form of the forward direction of this isomorphism.
• CliffordAlgebra.ofEven: The simp-normal form of the reverse direction of this isomorphism.
• CliffordAlgebra.evenEquivEvenNeg: Every even subalgebra is isomorphic to the even subalgebra of the Clifford algebra with negated quadratic form.

• CliffordAlgebra.evenToNeg: The simp-normal form of each direction of this isomorphism.

## Main results #

• CliffordAlgebra.coe_toEven_reverse_involute: the behavior of CliffordAlgebra.toEven on the "Clifford conjugate", that is CliffordAlgebra.reverse composed with CliffordAlgebra.involute.

### Constructions needed for CliffordAlgebra.equivEven#

@[reducible, inline]
abbrev CliffordAlgebra.EquivEven.Q' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

The quadratic form on the augmented vector space M × R sending v + r•e0 to Q v - r^2.

Equations
Instances For
theorem CliffordAlgebra.EquivEven.Q'_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M × R) :
= Q m.1 - m.2 * m.2
def CliffordAlgebra.EquivEven.e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

The unit vector in the new dimension

Equations
Instances For
def CliffordAlgebra.EquivEven.v {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

The embedding from the existing vector space

Equations
Instances For
theorem CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) (r : R) :
(m, r) =
theorem CliffordAlgebra.EquivEven.e0_mul_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
theorem CliffordAlgebra.EquivEven.v_sq_scalar {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
= (Q m)
theorem CliffordAlgebra.EquivEven.neg_e0_mul_v {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
theorem CliffordAlgebra.EquivEven.neg_v_mul_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
@[simp]
theorem CliffordAlgebra.EquivEven.e0_mul_v_mul_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
@[simp]
theorem CliffordAlgebra.EquivEven.reverse_v {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
CliffordAlgebra.reverse () =
@[simp]
theorem CliffordAlgebra.EquivEven.involute_v {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
CliffordAlgebra.involute () =
@[simp]
theorem CliffordAlgebra.EquivEven.reverse_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
CliffordAlgebra.reverse =
@[simp]
theorem CliffordAlgebra.EquivEven.involute_e0 {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
CliffordAlgebra.involute =
def CliffordAlgebra.toEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

The embedding from the smaller algebra into the new larger one.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CliffordAlgebra.toEven_ι {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
( ( m)) =
def CliffordAlgebra.ofEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

The embedding from the even subalgebra with an extra dimension into the original algebra.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CliffordAlgebra.ofEven_ι {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (x : M × R) (y : M × R) :
((.bilin x) y) = ( x.1 + () x.2) * ( y.1 - () y.2)
theorem CliffordAlgebra.toEven_comp_ofEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
theorem CliffordAlgebra.ofEven_comp_toEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
.comp =
def CliffordAlgebra.equivEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

Any clifford algebra is isomorphic to the even subalgebra of a clifford algebra with an extra dimension (that is, with vector space M × R), with a quadratic form evaluating to -1 on that new basis vector.

Equations
Instances For
theorem CliffordAlgebra.coe_toEven_reverse_involute {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (x : ) :
( (CliffordAlgebra.reverse (CliffordAlgebra.involute x))) = CliffordAlgebra.reverse ()

The representation of the clifford conjugate (i.e. the reverse of the involute) in the even subalgebra is just the reverse of the representation.

### Constructions needed for CliffordAlgebra.evenEquivEvenNeg#

def CliffordAlgebra.evenToNeg {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (Q' : ) (h : Q' = -Q) :
→ₐ[R] ()

One direction of CliffordAlgebra.evenEquivEvenNeg

Equations
• = { bilin := -.bilin, contract := , contract_mid := }
Instances For
@[simp]
theorem CliffordAlgebra.evenToNeg_ι {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (Q' : ) (h : Q' = -Q) (m₁ : M) (m₂ : M) :
() ((.bilin m₁) m₂) = -(.bilin m₁) m₂
theorem CliffordAlgebra.evenToNeg_comp_evenToNeg {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (Q' : ) (h : Q' = -Q) (h' : Q = -Q') :
().comp () =
@[simp]
theorem CliffordAlgebra.evenEquivEvenNeg_symm_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : ()) :
.symm a = () a
@[simp]
theorem CliffordAlgebra.evenEquivEvenNeg_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : ) :
= () a
def CliffordAlgebra.evenEquivEvenNeg {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
≃ₐ[R] ()

The even subalgebras of the algebras with quadratic form Q and -Q are isomorphic.

Stated another way, 𝒞ℓ⁺(p,q,r) and 𝒞ℓ⁺(q,p,r) are isomorphic.

Equations
Instances For