# mathlibdocumentation

linear_algebra.clifford_algebra.even_equiv

# Isomorphisms with the even subalgebra of a Clifford algebra #

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

## Main definitions #

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

• clifford_algebra.even_equiv.Q': The quadratic form used by this "one-up" algebra.
• clifford_algebra.to_even: The simp-normal form of the forward direction of this isomorphism.
• clifford_algebra.of_even: The simp-normal form of the reverse direction of this isomorphism.
• clifford_algebra.even_equiv_even_neg: Every even subalgebra is isomorphic to the even subalgebra of the Clifford algebra with negated quadratic form.

• clifford_algebra.even_to_neg: The simp-normal form of each direction of this isomorphism.

## Main results #

• clifford_algebra.coe_to_even_reverse_involute: the behavior of clifford_algebra.to_even on the "Clifford conjugate", that is clifford_algebra.reverse composed with clifford_algebra.involute.

### Constructions needed for clifford_algebra.equiv_even#

@[reducible]
def clifford_algebra.equiv_even.Q' {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
(M × R)

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

Equations
theorem clifford_algebra.equiv_even.Q'_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M × R) :
= Q m.fst - m.snd * m.snd
def clifford_algebra.equiv_even.e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

The unit vector in the new dimension

Equations
def clifford_algebra.equiv_even.v {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

The embedding from the existing vector space

Equations
theorem clifford_algebra.equiv_even.ι_eq_v_add_smul_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) (r : R) :
theorem clifford_algebra.equiv_even.e0_mul_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
theorem clifford_algebra.equiv_even.v_sq_scalar {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
= (Q m)
theorem clifford_algebra.equiv_even.neg_e0_mul_v {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
theorem clifford_algebra.equiv_even.neg_v_mul_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
@[simp]
theorem clifford_algebra.equiv_even.e0_mul_v_mul_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
@[simp]
theorem clifford_algebra.equiv_even.reverse_v {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
@[simp]
theorem clifford_algebra.equiv_even.involute_v {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
@[simp]
theorem clifford_algebra.equiv_even.reverse_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
@[simp]
theorem clifford_algebra.equiv_even.involute_e0 {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
def clifford_algebra.to_even {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

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

Equations
@[simp]
theorem clifford_algebra.to_even_ι {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
def clifford_algebra.of_even {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

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

Equations
theorem clifford_algebra.of_even_ι {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (x y : M × R) :
theorem clifford_algebra.to_even_comp_of_even {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
theorem clifford_algebra.of_even_comp_to_even {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
def clifford_algebra.equiv_even {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

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
@[simp]
theorem clifford_algebra.equiv_even_symm_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M)  :
=
@[simp]
theorem clifford_algebra.equiv_even_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (ᾰ : clifford_algebra Q) :
theorem clifford_algebra.coe_to_even_reverse_involute {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (x : clifford_algebra Q) :

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 clifford_algebra.even_equiv_even_neg#

def clifford_algebra.even_to_neg {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q Q' : M) (h : Q' = -Q) :

One direction of clifford_algebra.even_equiv_even_neg

Equations
@[simp]
theorem clifford_algebra.even_to_neg_ι {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q Q' : M) (h : Q' = -Q) (m₁ m₂ : M) :
h) ((.bilin) m₁) m₂) = -(.bilin) m₁) m₂
theorem clifford_algebra.even_to_neg_comp_even_to_neg {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q Q' : M) (h : Q' = -Q) (h' : Q = -Q') :
h').comp h) =
@[simp]
theorem clifford_algebra.even_equiv_even_neg_symm_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (ᾰ : ) :
= _)
@[simp]
theorem clifford_algebra.even_equiv_even_neg_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (ᾰ : ) :
= _)
def clifford_algebra.even_equiv_even_neg {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

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