Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.Spin.Kernel

The kernel of the Spin action #

On a subsingleton quadratic space, the Spin action is a bijection between trivial groups, so its kernel is trivial. In particular, this describes the zero-dimensional case over a field. For a positive-dimensional finite nondegenerate quadratic space over a field where 2 is invertible, the kernel instead consists of the two scalar elements. The proof first shows that an even Clifford element commuting with every generating vector is scalar, using contraction and the exterior-algebra basis. Unitarity then restricts the scalar to 1 or -1.

Main results #

References #

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

Square roots of unity, and the scalar -1, in the Spin group #

source
theorem CliffordAlgebra.algebraMap_mem_spinGroup_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) (hvQ : IsUnit (Q v)) {ζ : R} (hζ : ζ ^ 2 = 1) :
(algebraMap R (CliffordAlgebra Q)) ζ ∈ spinGroup Q

A square root of unity belongs to the Spin group when the quadratic form is a unit on some vector: it is the product of the two invertible vectors ζ (Q v)⁻¹ • v and v.

source
theorem CliffordAlgebra.neg_one_mem_spinGroup_of_isUnit {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) (hvQ : IsUnit (Q v)) :
-1 ∈ spinGroup Q

The scalar -1 belongs to the Spin group when the quadratic form is a unit on some vector.

source
theorem CliffordAlgebra.neg_one_mem_spinGroup {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
-1 ∈ spinGroup Q

The scalar -1 belongs to the Spin group of a nonzero quadratic form over a field.

source
def CliffordAlgebra.spinGroup.negOne {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
↥(spinGroup Q)

The canonical scalar -1 in the Spin group of a nonzero quadratic form over a field.

Instances For
    source
    @[simp]
    theorem CliffordAlgebra.spinGroup.coe_negOne {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
    ↑(negOne Q hQ) = -1

    The underlying Clifford element of spinGroup.negOne is the scalar -1.

    source
    @[simp]
    theorem CliffordAlgebra.spinGroup.negOne_mul_self {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
    negOne Q hQ * negOne Q hQ = 1

    The canonical scalar -1 squares to the identity.

    source
    theorem CliffordAlgebra.spinGroup.negOne_ne_one {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) [Invertible 2] (hQ : Q ≠ 0) :
    negOne Q hQ ≠ 1

    The canonical scalar -1 in the Spin group is not the identity when 2 is invertible.

    source
    theorem CliffordAlgebra.mem_ker_spinToSpecialOrthogonal_of_coe_eq_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) {r : R} (h : ↑x = (algebraMap R (CliffordAlgebra Q)) r) :
    x ∈ (spinToSpecialOrthogonal Q).ker

    A Spin element whose Clifford value is a scalar lies in the kernel of the Spin action.

    source
    theorem CliffordAlgebra.mem_ker_spinToSpecialOrthogonal_of_coe_eq_neg_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) (h : ↑x = -1) :
    x ∈ (spinToSpecialOrthogonal Q).ker

    A Spin element whose Clifford value is -1 lies in the kernel of the Spin action.

    source
    theorem CliffordAlgebra.spinGroup.negOne_mem_ker_spinToSpecialOrthogonal {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
    negOne Q hQ ∈ (spinToSpecialOrthogonal Q).ker

    The scalar -1 lies in the kernel of the Spin action.

    source
    @[simp]
    theorem CliffordAlgebra.spinGroup.spinToSpecialOrthogonal_negOne {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
    (spinToSpecialOrthogonal Q) (negOne Q hQ) = 1

    The scalar -1 acts trivially on the quadratic space.

    source
    @[simp]
    theorem CliffordAlgebra.spinGroup.spinToOrthogonal_negOne {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : Q ≠ 0) :
    (spinToOrthogonal Q) (negOne Q hQ) = 1

    The scalar -1 acts trivially under the primary orthogonal Spin action.

    source
    @[simp]
    theorem QuadraticMap.Isometry.spinGroupMap_negOne {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {N : Type w} [AddCommGroup N] [Module K N] {Q : QuadraticForm K M} {P : QuadraticForm K N} (f : Q →qᵢ P) (hQ : Q ≠ 0) :
    f.spinGroupMap (CliffordAlgebra.spinGroup.negOne Q hQ) = CliffordAlgebra.spinGroup.negOne P ⋯

    A Spin-group map induced by a quadratic isometry preserves the canonical scalar -1.

    source
    theorem CliffordAlgebra.ker_spinToSpecialOrthogonal_eq_bot_of_subsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Subsingleton M] (Q : QuadraticForm R M) [Invertible 2] :
    (spinToSpecialOrthogonal Q).ker = ⊥

    The Spin action on a subsingleton quadratic space has trivial kernel.

    source
    theorem CliffordAlgebra.spinToSpecialOrthogonal_bijective_of_subsingleton {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Subsingleton M] (Q : QuadraticForm R M) [Invertible 2] :
    Function.Bijective ⇑(spinToSpecialOrthogonal Q)

    The Spin action on a subsingleton quadratic space is a bijection between trivial groups.

    source
    theorem CliffordAlgebra.mem_ker_spinToSpecialOrthogonal_iff {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) [Invertible 2] [Nontrivial M] (hQ : QuadraticMap.Nondegenerate) (x : ↥(spinGroup Q)) :
    x ∈ (spinToSpecialOrthogonal Q).ker ↔ x = 1 ∨ x = spinGroup.negOne Q ⋯

    A Spin element lies in the kernel of the special-orthogonal action exactly when it is the scalar 1 or the canonical scalar -1.

    source
    theorem CliffordAlgebra.eq_or_eq_negOne_mul_of_spinToSpecialOrthogonal_eq {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) [Invertible 2] [Nontrivial M] (hQ : QuadraticMap.Nondegenerate) (x z : ↥(spinGroup Q)) (h : (spinToSpecialOrthogonal Q) x = (spinToSpecialOrthogonal Q) z) :
    x = z ∨ x = spinGroup.negOne Q ⋯ * z

    Two Spin elements with the same special-orthogonal projection are equal or differ by the canonical scalar -1.

    source
    theorem CliffordAlgebra.mem_ker_spinToOrthogonal_iff {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (Q : QuadraticForm K M) [Invertible 2] [Nontrivial M] (hQ : QuadraticMap.Nondegenerate) (x : ↥(spinGroup Q)) :
    x ∈ (spinToOrthogonal Q).ker ↔ x = 1 ∨ x = spinGroup.negOne Q ⋯

    A Spin element lies in the kernel of the orthogonal action exactly when it is the scalar 1 or the canonical scalar -1.

    source
    theorem CliffordAlgebra.ker_spinToSpecialOrthogonal_eq_bot_of_finrank_eq_zero {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (hM : Module.finrank K M = 0) (Q : QuadraticForm K M) [Invertible 2] :
    (spinToSpecialOrthogonal Q).ker = ⊥

    The Spin action on a zero-dimensional quadratic space has trivial kernel.

    source
    theorem CliffordAlgebra.spinToSpecialOrthogonal_bijective_of_finrank_eq_zero {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (hM : Module.finrank K M = 0) (Q : QuadraticForm K M) [Invertible 2] :
    Function.Bijective ⇑(spinToSpecialOrthogonal Q)

    The Spin action on a zero-dimensional quadratic space is a bijection between trivial groups.

    source
    theorem CliffordAlgebra.card_ker_spinToSpecialOrthogonal {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] (hM : 0 < Module.finrank K M) (Q : QuadraticForm K M) [Invertible 2] (hQ : QuadraticMap.Nondegenerate) :
    Nat.card ↥(spinToSpecialOrthogonal Q).ker = 2

    The kernel of the Spin action on a positive-dimensional finite nondegenerate quadratic space over a field where 2 is invertible has cardinality two.

    source
    noncomputable def CliffordAlgebra.zmodTwoMulEquivKerSpinToSpecialOrthogonal {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) ≃* ↥(spinToSpecialOrthogonal Q).ker

    The kernel of the Spin 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.

    Instances For
      source
      @[simp]
      theorem CliffordAlgebra.zmodTwoMulEquivKerSpinToSpecialOrthogonal_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) :
      (zmodTwoMulEquivKerSpinToSpecialOrthogonal Q hQ) (Multiplicative.ofAdd 1) = ⟨spinGroup.negOne Q ⋯, ⋯⟩

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

      source
      @[simp]
      theorem CliffordAlgebra.zmodTwoMulEquivKerSpinToSpecialOrthogonal_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) :
      (zmodTwoMulEquivKerSpinToSpecialOrthogonal Q hQ).symm ⟨spinGroup.negOne Q ⋯, ⋯⟩ = Multiplicative.ofAdd 1

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