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 #
-
clifford_algebra.equiv_even: Every Clifford algebra is isomorphic as an algebra to the even subalgebra of a Clifford algebra with one more dimension.clifford_algebra.even_equiv.Q': The quadratic form used by this "one-up" algebra.clifford_algebra.to_even: The simp-normal form of the forward direction of this isomorphism.clifford_algebra.of_even: The simp-normal form of the reverse direction of this isomorphism.
-
clifford_algebra.even_equiv_even_neg: Every even subalgebra is isomorphic to the even subalgebra of the Clifford algebra with negated quadratic form.clifford_algebra.even_to_neg: The simp-normal form of each direction of this isomorphism.
Main results #
clifford_algebra.coe_to_even_reverse_involute: the behavior ofclifford_algebra.to_evenon the "Clifford conjugate", that isclifford_algebra.reversecomposed withclifford_algebra.involute.
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) :
quadratic_form R (M × R)
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) :
def
clifford_algebra.equiv_even.e0
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The unit vector in the new dimension
Equations
def
clifford_algebra.equiv_even.v
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The embedding from the existing vector space
Equations
theorem
clifford_algebra.equiv_even.ι_eq_v_add_smul_e0
{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 : R) :
⇑(clifford_algebra.ι (clifford_algebra.equiv_even.Q' Q)) (m, r) = ⇑(clifford_algebra.equiv_even.v Q) m + r • clifford_algebra.equiv_even.e0 Q
theorem
clifford_algebra.equiv_even.e0_mul_e0
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
theorem
clifford_algebra.equiv_even.v_sq_scalar
{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) :
⇑(clifford_algebra.equiv_even.v Q) m * ⇑(clifford_algebra.equiv_even.v Q) m = ⇑(algebra_map R (clifford_algebra (clifford_algebra.equiv_even.Q' Q))) (⇑Q m)
theorem
clifford_algebra.equiv_even.neg_e0_mul_v
{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) :
theorem
clifford_algebra.equiv_even.neg_v_mul_e0
{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) :
@[simp]
theorem
clifford_algebra.equiv_even.e0_mul_v_mul_e0
{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) :
@[simp]
theorem
clifford_algebra.equiv_even.reverse_v
{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) :
@[simp]
theorem
clifford_algebra.equiv_even.involute_v
{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) :
@[simp]
theorem
clifford_algebra.equiv_even.reverse_e0
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[simp]
theorem
clifford_algebra.equiv_even.involute_e0
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
def
clifford_algebra.to_even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The embedding from the smaller algebra into the new larger one.
Equations
@[simp]
theorem
clifford_algebra.to_even_ι
{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) :
↑(⇑(clifford_algebra.to_even Q) (⇑(clifford_algebra.ι Q) m)) = clifford_algebra.equiv_even.e0 Q * ⇑(clifford_algebra.equiv_even.v Q) m
def
clifford_algebra.of_even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The embedding from the even subalgebra with an extra dimension into the original algebra.
Equations
- clifford_algebra.of_even Q = let f : M × R →ₗ[R] M × R →ₗ[R] clifford_algebra Q := ((algebra.lmul R (clifford_algebra Q)).to_linear_map.comp ((clifford_algebra.ι Q).comp (linear_map.fst R M R) + (algebra.linear_map R (clifford_algebra Q)).comp (linear_map.snd R M R))).compl₂ ((clifford_algebra.ι Q).comp (linear_map.fst R M R) - (algebra.linear_map R (clifford_algebra Q)).comp (linear_map.snd R M R)) in ⇑(clifford_algebra.even.lift (clifford_algebra.equiv_even.Q' Q)) {bilin := f, contract := _, contract_mid := _}
theorem
clifford_algebra.of_even_ι
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(x y : M × R) :
⇑(clifford_algebra.of_even Q) (⇑(⇑((clifford_algebra.even.ι (clifford_algebra.equiv_even.Q' Q)).bilin) x) y) = (⇑(clifford_algebra.ι Q) x.fst + ⇑(algebra_map R (clifford_algebra Q)) x.snd) * (⇑(clifford_algebra.ι Q) y.fst - ⇑(algebra_map R (clifford_algebra Q)) y.snd)
theorem
clifford_algebra.to_even_comp_of_even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
theorem
clifford_algebra.of_even_comp_to_even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
def
clifford_algebra.equiv_even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form 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
@[simp]
theorem
clifford_algebra.equiv_even_symm_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.even (clifford_algebra.equiv_even.Q' Q))) :
⇑((clifford_algebra.equiv_even Q).symm) ᾰ = ⇑(clifford_algebra.of_even Q) ᾰ
@[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) :
⇑(clifford_algebra.equiv_even Q) ᾰ = ⇑(clifford_algebra.to_even Q) ᾰ
theorem
clifford_algebra.coe_to_even_reverse_involute
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(x : 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 #
def
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) :
↥(clifford_algebra.even Q) →ₐ[R] ↥(clifford_algebra.even Q')
One direction of clifford_algebra.even_equiv_even_neg
Equations
- clifford_algebra.even_to_neg Q Q' h = ⇑(clifford_algebra.even.lift Q) {bilin := -(clifford_algebra.even.ι Q').bilin, contract := _, contract_mid := _}
@[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) :
⇑(clifford_algebra.even_to_neg Q Q' h) (⇑(⇑((clifford_algebra.even.ι Q).bilin) m₁) m₂) = -⇑(⇑((clifford_algebra.even.ι Q').bilin) 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') :
(clifford_algebra.even_to_neg Q' Q h').comp (clifford_algebra.even_to_neg Q Q' h) = alg_hom.id R ↥(clifford_algebra.even Q)
@[simp]
theorem
clifford_algebra.even_equiv_even_neg_symm_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.even (-Q))) :
⇑((clifford_algebra.even_equiv_even_neg Q).symm) ᾰ = ⇑(clifford_algebra.even_to_neg (-Q) Q _) ᾰ
@[simp]
theorem
clifford_algebra.even_equiv_even_neg_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.even Q)) :
⇑(clifford_algebra.even_equiv_even_neg Q) ᾰ = ⇑(clifford_algebra.even_to_neg Q (-Q) _) ᾰ
def
clifford_algebra.even_equiv_even_neg
{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.even Q) ≃ₐ[R] ↥(clifford_algebra.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
- clifford_algebra.even_equiv_even_neg Q = alg_equiv.of_alg_hom (clifford_algebra.even_to_neg Q (-Q) _) (clifford_algebra.even_to_neg (-Q) Q _) _ _