Basic Spin-group carrier facts

This file records the carrier-level criterion that a product of two Clifford vectors with unit product of norms belongs to the Spin group, identifies membership in the range of spinGroup.toUnits with membership of the underlying Clifford value, and proves that the Spin group of the zero module is trivial. The action and its orthogonal comparison are defined in Spin.Action and Pin.Action.

@[simp]

theorem CliffordAlgebra.mem_spinGroup_toUnits_range_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (u : (CliffordAlgebra Q)ˣ) : u ∈ spinGroup.toUnits.range ↔ ↑u ∈ spinGroup Q

A Clifford unit belongs to the range of the canonical map from the Spin group exactly when its Clifford value belongs to the Spin group.

theorem CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x y : M) (hxy : Q x * Q y = 1) : (ι Q) x * (ι Q) y ∈ spinGroup Q

The product of two Clifford generators belongs to Spin when their norms multiply to one.

instance CliffordAlgebra.instSubsingletonSpinGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Subsingleton M] : Subsingleton ↥(spinGroup Q)

The Spin group of a quadratic form on the zero module is trivial, because the Lipschitz group containing it is (lipschitzGroup_eq_bot).