mathlib documentation

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 #

Main results #

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] [add_comm_group M] [module R M] (Q : quadratic_form R M) :

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] [add_comm_group M] [module R M] (Q : quadratic_form R M) (m : M × R) :

The unit vector in the new dimension

Equations

The embedding from the existing vector space

Equations

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_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (ᾰ : 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 #

@[simp]
theorem clifford_algebra.even_to_neg_ι {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q Q' : quadratic_form R M) (h : Q' = -Q) (m₁ m₂ : M) :
theorem clifford_algebra.even_to_neg_comp_even_to_neg {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q Q' : quadratic_form R M) (h : Q' = -Q) (h' : Q = -Q') :

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