mathlib3 documentation

linear_algebra.clifford_algebra.even_equiv

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 #

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

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

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

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