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 ofCliffordAlgebra.toEvenon the "Clifford conjugate", that isCliffordAlgebra.reversecomposed withCliffordAlgebra.involute.
Constructions needed for CliffordAlgebra.equivEven #
@[reducible, inline]
abbrev
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.
Equations
- CliffordAlgebra.EquivEven.Q' Q = Q.prod (-QuadraticForm.sq)
Instances For
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.1 - m.2 * m.2
def
CliffordAlgebra.EquivEven.e0
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
The unit vector in the new dimension
Equations
Instances For
def
CliffordAlgebra.EquivEven.v
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
The embedding from the existing vector space
Equations
Instances For
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)
:
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)
:
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)
:
@[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)
:
@[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)
:
The embedding from the smaller algebra into the new larger one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
The embedding from the even subalgebra with an extra dimension into the original algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((CliffordAlgebra.ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
theorem
CliffordAlgebra.toEven_comp_ofEven
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
:
(CliffordAlgebra.toEven Q).comp (CliffordAlgebra.ofEven Q) = AlgHom.id R ↥(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)
:
(CliffordAlgebra.ofEven Q).comp (CliffordAlgebra.toEven Q) = AlgHom.id R (CliffordAlgebra Q)
def
CliffordAlgebra.equivEven
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R 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
Instances For
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)
:
↥(CliffordAlgebra.even Q) →ₐ[R] ↥(CliffordAlgebra.even Q')
One direction of CliffordAlgebra.evenEquivEvenNeg
Equations
- CliffordAlgebra.evenToNeg Q Q' h = (CliffordAlgebra.even.lift Q) { bilin := -(CliffordAlgebra.even.ι Q').bilin, contract := ⋯, contract_mid := ⋯ }
Instances For
@[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')
:
(CliffordAlgebra.evenToNeg Q' Q h').comp (CliffordAlgebra.evenToNeg Q Q' h) = AlgHom.id R ↥(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 : ↥(CliffordAlgebra.even (-Q)))
:
(CliffordAlgebra.evenEquivEvenNeg Q).symm a = (CliffordAlgebra.evenToNeg (-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 : ↥(CliffordAlgebra.even Q))
:
(CliffordAlgebra.evenEquivEvenNeg Q) a = (CliffordAlgebra.evenToNeg 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)
:
↥(CliffordAlgebra.even Q) ≃ₐ[R] ↥(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.
Equations
- CliffordAlgebra.evenEquivEvenNeg Q = AlgEquiv.ofAlgHom (CliffordAlgebra.evenToNeg Q (-Q) ⋯) (CliffordAlgebra.evenToNeg (-Q) Q ⋯) ⋯ ⋯