Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.Spin.SpinorNorm.Isometry

Spinor norms under isometries #

An isometry of quadratic spaces carries reflections to reflections with the same quadratic value. Since reflections generate the orthogonal group, it preserves the orthogonal spinor norm and its restriction to the special orthogonal group. This lets spinor-norm computations be transported across a change of quadratic coordinates. The induced equivalence of spinor-norm kernels also intertwines the corresponding Spin homomorphisms.

References #

source
@[simp]
theorem QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) :
(CliffordAlgebra.orthogonalSpinorNorm Q' ⋯) (e.orthogonalGroupCongr g) = (CliffordAlgebra.orthogonalSpinorNorm Q hQ) g

An isometric equivalence preserves the orthogonal spinor norm.

source
theorem QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) :
(CliffordAlgebra.spinorNorm Q' ⋯) (e.specialOrthogonalGroupCongr g) = (CliffordAlgebra.spinorNorm Q hQ) g

An isometric equivalence preserves the spinor norm on the special orthogonal group.

source
theorem QuadraticMap.IsometryEquiv.map_ker_spinorNorm {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) :
Subgroup.map (↑e.specialOrthogonalGroupCongr) (CliffordAlgebra.spinorNorm Q hQ).ker = (CliffordAlgebra.spinorNorm Q' ⋯).ker

Special-orthogonal transport maps the kernel of the spinor norm onto the kernel for the isometric quadratic form.

source
noncomputable def QuadraticMap.IsometryEquiv.spinorNormKernelCongr {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) :
↥(CliffordAlgebra.spinorNorm Q hQ).ker ≃* ↥(CliffordAlgebra.spinorNorm Q' ⋯).ker

An isometric equivalence restricts to an equivalence of spinor-norm kernels.

Instances For
    source
    @[simp]
    theorem QuadraticMap.IsometryEquiv.coe_spinorNormKernelCongr_apply {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) (g : ↥(CliffordAlgebra.spinorNorm Q hQ).ker) :
    ↑((e.spinorNormKernelCongr hQ) g) = e.specialOrthogonalGroupCongr ↑g

    The underlying special-orthogonal element of spinorNormKernelCongr is obtained by special-orthogonal transport.

    source
    @[simp]
    theorem QuadraticMap.IsometryEquiv.coe_spinorNormKernelCongr_symm_apply {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) (g : ↥(CliffordAlgebra.spinorNorm Q' ⋯).ker) :
    ↑((e.spinorNormKernelCongr hQ).symm g) = e.specialOrthogonalGroupCongr.symm ↑g

    The inverse of spinorNormKernelCongr acts through inverse special-orthogonal transport.

    source
    @[simp]
    theorem QuadraticMap.IsometryEquiv.spinorNormKernelCongr_spinToSpinorNormKernel {K : Type u} [Field K] [Invertible 2] {V : Type v} {W : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {Q' : QuadraticForm K W} (e : IsometryEquiv Q Q') (hQ : Nondegenerate) (x : ↥(spinGroup Q)) :
    (e.spinorNormKernelCongr hQ) ((CliffordAlgebra.spinToSpinorNormKernel Q hQ) x) = (CliffordAlgebra.spinToSpinorNormKernel Q' ⋯) (e.spinGroupEquiv x)

    Transporting the Spin homomorphism to the spinor-norm kernel agrees with first transporting the Spin element.