# Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

# 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]
def 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.

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

The unit vector in the new dimension

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

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 : ) :
→ₐ[R] { x // }

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

Instances For
@[simp]
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 : ) :
{ x // } →ₐ[R]

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

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.fst + ↑() x.snd) * (↑() y.fst - ↑() y.snd)
theorem CliffordAlgebra.toEven_comp_ofEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
= AlgHom.id R { x // }
theorem CliffordAlgebra.ofEven_comp_toEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
@[simp]
theorem CliffordAlgebra.equivEven_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : ) :
= ↑() a
@[simp]
theorem CliffordAlgebra.equivEven_symm_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : { x // }) :
= ↑() a
def CliffordAlgebra.equivEven {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
≃ₐ[R] { x // }

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.

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 ↑(↑() x)

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) :
{ x // } →ₐ[R] { x // }

One direction of CliffordAlgebra.evenEquivEvenNeg

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') :
AlgHom.comp () () = AlgHom.id R { x // }
@[simp]
theorem CliffordAlgebra.evenEquivEvenNeg_symm_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : { x // }) :
= ↑(CliffordAlgebra.evenToNeg (-Q) Q (_ : Q = - -Q)) a
@[simp]
theorem CliffordAlgebra.evenEquivEvenNeg_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (a : { x // }) :
= ↑(CliffordAlgebra.evenToNeg Q (-Q) (_ : -Q = -Q)) a
def CliffordAlgebra.evenEquivEvenNeg {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
{ x // } ≃ₐ[R] { x // }

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.

Instances For