Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.Pin.Kernel

The kernel of the Pin action #

For a positive-dimensional finite nondegenerate quadratic space over a field where 2 is invertible, the kernel of the Pin action is canonically the cyclic group of order two. The proof identifies a Pin element acting trivially with an even element, then reuses the Spin-kernel classification.

Main results #

References #

This completes the Pin-kernel part of Layer 2 in TauCetiRoadmap/RepresentationTheory/SpinRepresentations/README.md. See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

source
noncomputable def CliffordAlgebra.zmodTwoMulEquivKerPinToOrthogonal {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [Nontrivial M] (Q : QuadraticForm K M) [Invertible 2] (hQ : QuadraticMap.Nondegenerate) :
Multiplicative (ZMod 2) ≃* ↥(pinToOrthogonal Q).ker

The kernel of the Pin action on a positive-dimensional nondegenerate quadratic space over a field in which 2 is invertible is canonically the cyclic group of order two, with its generator sent to the scalar -1.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CliffordAlgebra.zmodTwoMulEquivKerPinToOrthogonal_apply_ofAdd_one {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [Nontrivial M] (Q : QuadraticForm K M) [Invertible 2] (hQ : QuadraticMap.Nondegenerate) :
    (zmodTwoMulEquivKerPinToOrthogonal Q hQ) (Multiplicative.ofAdd 1) = ⟨(spinToPin Q) (spinGroup.negOne Q ⋯), ⋯⟩

    The chosen generator of Multiplicative (ZMod 2) maps to the scalar -1 in the Pin kernel.

    source
    @[simp]
    theorem CliffordAlgebra.zmodTwoMulEquivKerPinToOrthogonal_symm_apply_negOne {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] [Nontrivial M] (Q : QuadraticForm K M) [Invertible 2] (hQ : QuadraticMap.Nondegenerate) :
    (zmodTwoMulEquivKerPinToOrthogonal Q hQ).symm ⟨(spinToPin Q) (spinGroup.negOne Q ⋯), ⋯⟩ = Multiplicative.ofAdd 1

    The inverse kernel equivalence sends the scalar -1 to the chosen generator of Multiplicative (ZMod 2).