mathlib3 documentation


Isomorphisms with the even subalgebra of a Clifford algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Main results #

Constructions needed for clifford_algebra.equiv_even #

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.

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

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.


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 #

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

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.