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} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : QuadraticForm R (M × R)

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

theorem CliffordAlgebra.EquivEven.Q'_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M × R) : ↑(CliffordAlgebra.EquivEven.Q' Q) m = ↑Q m.fst - m.snd * m.snd

def CliffordAlgebra.EquivEven.e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q)

The unit vector in the new dimension

def CliffordAlgebra.EquivEven.v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : M →ₗ[R] CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q)

The embedding from the existing vector space

theorem CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) (r : R) : ↑(CliffordAlgebra.ι (CliffordAlgebra.EquivEven.Q' Q)) (m, r) = ↑(CliffordAlgebra.EquivEven.v Q) m + r • CliffordAlgebra.EquivEven.e0 Q

theorem CliffordAlgebra.EquivEven.e0_mul_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : CliffordAlgebra.EquivEven.e0 Q * CliffordAlgebra.EquivEven.e0 Q = -1

theorem CliffordAlgebra.EquivEven.v_sq_scalar {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : ↑(CliffordAlgebra.EquivEven.v Q) m * ↑(CliffordAlgebra.EquivEven.v Q) m = ↑(algebraMap R (CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q))) (↑Q m)

theorem CliffordAlgebra.EquivEven.neg_e0_mul_v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : -(CliffordAlgebra.EquivEven.e0 Q * ↑(CliffordAlgebra.EquivEven.v Q) m) = ↑(CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q

theorem CliffordAlgebra.EquivEven.neg_v_mul_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : -(↑(CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q) = CliffordAlgebra.EquivEven.e0 Q * ↑(CliffordAlgebra.EquivEven.v Q) m

@[simp]

theorem CliffordAlgebra.EquivEven.e0_mul_v_mul_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : CliffordAlgebra.EquivEven.e0 Q * ↑(CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q = ↑(CliffordAlgebra.EquivEven.v Q) m

@[simp]

theorem CliffordAlgebra.EquivEven.reverse_v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : ↑CliffordAlgebra.reverse (↑(CliffordAlgebra.EquivEven.v Q) m) = ↑(CliffordAlgebra.EquivEven.v Q) m

@[simp]

theorem CliffordAlgebra.EquivEven.involute_v {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : ↑CliffordAlgebra.involute (↑(CliffordAlgebra.EquivEven.v Q) m) = -↑(CliffordAlgebra.EquivEven.v Q) m

@[simp]

theorem CliffordAlgebra.EquivEven.reverse_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↑CliffordAlgebra.reverse (CliffordAlgebra.EquivEven.e0 Q) = CliffordAlgebra.EquivEven.e0 Q

@[simp]

theorem CliffordAlgebra.EquivEven.involute_e0 {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↑CliffordAlgebra.involute (CliffordAlgebra.EquivEven.e0 Q) = -CliffordAlgebra.EquivEven.e0 Q

def CliffordAlgebra.toEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : CliffordAlgebra Q →ₐ[R] { x // x ∈ CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q) }

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

@[simp]

theorem CliffordAlgebra.toEven_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : ↑(↑(CliffordAlgebra.toEven Q) (↑(CliffordAlgebra.ι Q) m)) = CliffordAlgebra.EquivEven.e0 Q * ↑(CliffordAlgebra.EquivEven.v Q) m

def CliffordAlgebra.ofEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : { x // x ∈ CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q) } →ₐ[R] CliffordAlgebra Q

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

theorem CliffordAlgebra.ofEven_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : M × R) (y : M × R) : ↑(CliffordAlgebra.ofEven Q) (↑(↑(CliffordAlgebra.even.ι (CliffordAlgebra.EquivEven.Q' Q)).bilin x) y) = (↑(CliffordAlgebra.ι Q) x.fst + ↑(algebraMap R (CliffordAlgebra Q)) x.snd) * (↑(CliffordAlgebra.ι Q) y.fst - ↑(algebraMap R (CliffordAlgebra Q)) y.snd)

theorem CliffordAlgebra.toEven_comp_ofEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : AlgHom.comp (CliffordAlgebra.toEven Q) (CliffordAlgebra.ofEven Q) = AlgHom.id R { x // x ∈ CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q) }

theorem CliffordAlgebra.ofEven_comp_toEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : AlgHom.comp (CliffordAlgebra.ofEven Q) (CliffordAlgebra.toEven Q) = AlgHom.id R (CliffordAlgebra Q)

@[simp]

theorem CliffordAlgebra.equivEven_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : CliffordAlgebra Q) : ↑(CliffordAlgebra.equivEven Q) a = ↑(CliffordAlgebra.toEven Q) a

@[simp]

theorem CliffordAlgebra.equivEven_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : { x // x ∈ CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q) }) : ↑(AlgEquiv.symm (CliffordAlgebra.equivEven Q)) a = ↑(CliffordAlgebra.ofEven Q) a

def CliffordAlgebra.equivEven {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : CliffordAlgebra Q ≃ₐ[R] { x // x ∈ CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q) }

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.

theorem CliffordAlgebra.coe_toEven_reverse_involute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : ↑(↑(CliffordAlgebra.toEven Q) (↑CliffordAlgebra.reverse (↑CliffordAlgebra.involute x))) = ↑CliffordAlgebra.reverse ↑(↑(CliffordAlgebra.toEven Q) 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} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) : { x // x ∈ CliffordAlgebra.even Q } →ₐ[R] { x // x ∈ CliffordAlgebra.even Q' }

One direction of CliffordAlgebra.evenEquivEvenNeg

@[simp]

theorem CliffordAlgebra.evenToNeg_ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) (m₁ : M) (m₂ : M) : ↑(CliffordAlgebra.evenToNeg Q Q' h) (↑(↑(CliffordAlgebra.even.ι Q).bilin m₁) m₂) = -↑(↑(CliffordAlgebra.even.ι Q').bilin m₁) m₂

theorem CliffordAlgebra.evenToNeg_comp_evenToNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (Q' : QuadraticForm R M) (h : Q' = -Q) (h' : Q = -Q') : AlgHom.comp (CliffordAlgebra.evenToNeg Q' Q h') (CliffordAlgebra.evenToNeg Q Q' h) = AlgHom.id R { x // x ∈ CliffordAlgebra.even Q }

@[simp]

theorem CliffordAlgebra.evenEquivEvenNeg_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : { x // x ∈ CliffordAlgebra.even (-Q) }) : ↑(AlgEquiv.symm (CliffordAlgebra.evenEquivEvenNeg Q)) a = ↑(CliffordAlgebra.evenToNeg (-Q) Q (_ : Q = - -Q)) a

@[simp]

theorem CliffordAlgebra.evenEquivEvenNeg_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : { x // x ∈ CliffordAlgebra.even Q }) : ↑(CliffordAlgebra.evenEquivEvenNeg Q) a = ↑(CliffordAlgebra.evenToNeg Q (-Q) (_ : -Q = -Q)) a

def CliffordAlgebra.evenEquivEvenNeg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : { x // x ∈ CliffordAlgebra.even Q } ≃ₐ[R] { x // x ∈ CliffordAlgebra.even (-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.