The even unitary carrier of a Clifford algebra

The even Clifford algebra carries the canonical reversal involution. On even elements this is Mathlib's star, so the unitary equation star x * x = 1 is the reverse-unitary equation used in the low-dimensional descriptions of Spin groups. This file packages the even unitary elements as a subgroup of Clifford units, transports that subgroup along quadratic isometries, and compares it with Mathlib's Lipschitz-defined spinGroup.

The carrier is intentionally larger than spinGroup: the latter also requires membership in the Lipschitz closure. The range theorem records that distinction exactly, so subsequent low-rank arguments can prove when the two carriers coincide rather than building a second Spin definition.

The equivalence CliffordAlgebra.evenUnitaryGroupEquivUnitaryOfAlgEquiv transports this carrier along any algebra equivalence from the even Clifford algebra that carries reversal to the target star. Its coercion equations expose the forward and inverse maps without unfolding the construction.

The construction follows the Clifford-group conventions of H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2, and uses Mathlib's SpinGroup and Tau Ceti's Clifford functoriality API.

Main results

• CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one characterizes the carrier by the reverse-norm equation.
• CliffordAlgebra.evenUnitaryGroup.reverse_mul_self and CliffordAlgebra.evenUnitaryGroup.self_mul_reverse give its two norm equations.
• CliffordAlgebra.evenUnitaryGroup.reverse_eq_inv identifies reversal with the unit inverse.
• CliffordAlgebra.rightIotaEven_spinGroup_smul transports the Spin action after right multiplication by a vector of quadratic value -1.

def CliffordAlgebra.evenUnitaryGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Subgroup (CliffordAlgebra Q)ˣ

Units whose Clifford values are even and unitary for the canonical star involution.

Equations

• CliffordAlgebra.evenUnitaryGroup Q = { carrier := {x : (CliffordAlgebra Q)ˣ | ↑x ∈ CliffordAlgebra.even Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem CliffordAlgebra.evenUnitaryGroup.mem_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : (CliffordAlgebra Q)ˣ} : x ∈ evenUnitaryGroup Q ↔ ↑x ∈ even Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)

Membership in evenUnitaryGroup is exactly evenness together with the unitary equation.

theorem CliffordAlgebra.evenUnitaryGroup.mem_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ evenUnitaryGroup Q) : ↑x ∈ even Q

theorem CliffordAlgebra.evenUnitaryGroup.mem_unitary {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ evenUnitaryGroup Q) : ↑x ∈ unitary (CliffordAlgebra Q)

theorem CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : (CliffordAlgebra Q)ˣ} : x ∈ evenUnitaryGroup Q ↔ ↑x ∈ even Q ∧ reverse ↑x * ↑x = 1

An even Clifford unit lies in evenUnitaryGroup exactly when its reverse norm is one.

theorem CliffordAlgebra.evenUnitaryGroup.reverse_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : reverse ↑↑x * ↑↑x = 1

The reverse norm of an even unitary Clifford element is one.

theorem CliffordAlgebra.evenUnitaryGroup.self_mul_reverse {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : ↑↑x * reverse ↑↑x = 1

The right-handed reverse norm of an even unitary Clifford element is one.

@[simp]

theorem CliffordAlgebra.evenUnitaryGroup.reverse_eq_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : reverse ↑↑x = ↑(↑x)⁻¹

Reversal of an even unitary Clifford element is its unit inverse after coercion.

def QuadraticMap.Isometry.evenUnitaryGroupMap {R : Type u} [CommRing R] {M₁ : Type v'} {M₂ : Type w'} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) : ↥(CliffordAlgebra.evenUnitaryGroup Q₁) →* ↥(CliffordAlgebra.evenUnitaryGroup Q₂)

The Clifford-algebra map of a quadratic isometry restricts to the even unitary carriers.

Equations

• f.evenUnitaryGroupMap = { toFun := fun (x : ↥(CliffordAlgebra.evenUnitaryGroup Q₁)) => ⟨(Units.map ↑(CliffordAlgebra.map f).toRingHom) ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem QuadraticMap.Isometry.coe_evenUnitaryGroupMap_apply {R : Type u} [CommRing R] {M₁ : Type v'} {M₂ : Type w'} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : ↥(CliffordAlgebra.evenUnitaryGroup Q₁)) : ↑(f.evenUnitaryGroupMap x) = (Units.map ↑(CliffordAlgebra.map f).toRingHom) ↑x

After coercion, the induced map is the Units.map of the Clifford-algebra map.

@[simp]

theorem QuadraticMap.Isometry.evenUnitaryGroupMap_id {R : Type u} [CommRing R] {M₁ : Type v'} [AddCommGroup M₁] [Module R M₁] (Q : QuadraticForm R M₁) : (id Q).evenUnitaryGroupMap = MonoidHom.id ↥(CliffordAlgebra.evenUnitaryGroup Q)

The identity quadratic isometry induces the identity even-unitary-group homomorphism.

@[simp]

theorem QuadraticMap.Isometry.evenUnitaryGroupMap_comp {R : Type u} [CommRing R] {M₁ : Type v'} {M₂ : Type w'} {M₃ : Type z'} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) : f.evenUnitaryGroupMap.comp g.evenUnitaryGroupMap = (f.comp g).evenUnitaryGroupMap

Even-unitary-group homomorphisms respect composition of quadratic isometries.

def CliffordAlgebra.evenUnitaryGroupEvenPart {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↥(evenUnitaryGroup Q) →* ↥(even Q)

Forget an even unitary Clifford unit to its value in the even Clifford subalgebra.

Equations

• CliffordAlgebra.evenUnitaryGroupEvenPart Q = { toFun := fun (x : ↥(CliffordAlgebra.evenUnitaryGroup Q)) => ⟨↑↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupEvenPart {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : ↑((evenUnitaryGroupEvenPart Q) x) = ↑↑x

Coercing the even part of an even unitary element recovers its Clifford value.

theorem CliffordAlgebra.reverseEven_evenUnitaryGroupEvenPart_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : (reverseEven Q) ((evenUnitaryGroupEvenPart Q) x) * (evenUnitaryGroupEvenPart Q) x = 1

The left reverse norm of the even part of an even unitary element is one.

theorem CliffordAlgebra.evenUnitaryGroupEvenPart_mul_reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(evenUnitaryGroup Q)) : (evenUnitaryGroupEvenPart Q) x * (reverseEven Q) ((evenUnitaryGroupEvenPart Q) x) = 1

The right reverse norm of the even part of an even unitary element is one.

theorem CliffordAlgebra.map_evenUnitaryGroupEvenPart_mem_unitary {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] [StarMul A] (e : ↥(even Q) ≃ₐ[R] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) (x : ↥(evenUnitaryGroup Q)) : e ((evenUnitaryGroupEvenPart Q) x) ∈ unitary A

A reversal-preserving algebra equivalence sends the even part of an even unitary Clifford element to a unitary element of the target algebra.

noncomputable def CliffordAlgebra.evenUnitaryGroupEquivUnitaryOfAlgEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] [StarMul A] (e : ↥(even Q) ≃ₐ[R] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) : ↥(evenUnitaryGroup Q) ≃* ↥(unitary A)

A reversal-preserving equivalence from the even Clifford algebra transports its even unitary carrier to the unitary group of the target algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupEquivUnitaryOfAlgEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] [StarMul A] (e : ↥(even Q) ≃ₐ[R] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) (x : ↥(evenUnitaryGroup Q)) : ↑((evenUnitaryGroupEquivUnitaryOfAlgEquiv Q e he) x) = e ((evenUnitaryGroupEvenPart Q) x)

The forward unitary transport applies the algebra equivalence to the even Clifford value.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupEquivUnitaryOfAlgEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] [StarMul A] (e : ↥(even Q) ≃ₐ[R] A) (he : ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)) (q : ↥(unitary A)) : ↑↑((evenUnitaryGroupEquivUnitaryOfAlgEquiv Q e he).symm q) = ↑(e.symm ↑q)

The inverse unitary transport has Clifford value obtained by applying the inverse algebra equivalence.

noncomputable def CliffordAlgebra.evenUnitaryGroupEquivOfAlgEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] {G : Type u_1} [Group G] (e : ↥(even Q) ≃ₐ[R] A) (P : A → Prop) (val : G →* A) (hval : Function.Injective ⇑val) (ofVal : (a : A) → P a → G) (val_ofVal : ∀ (a : A) (ha : P a), val (ofVal a ha) = a) (val_mem : ∀ (g : G), P (val g)) (hP : ∀ (x : ↥(even Q)), (reverseEven Q) x * x = 1 ↔ P (e x)) : ↥(evenUnitaryGroup Q) ≃* G

Transport the even unitary Clifford group through an algebra equivalence when a target group is exactly the subtype cut out by the transported reverse-norm-one predicate.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.coe_evenUnitaryGroupEquivOfAlgEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] {G : Type u_1} [Group G] (e : ↥(even Q) ≃ₐ[R] A) (P : A → Prop) (val : G →* A) (hval : Function.Injective ⇑val) (ofVal : (a : A) → P a → G) (val_ofVal : ∀ (a : A) (ha : P a), val (ofVal a ha) = a) (val_mem : ∀ (g : G), P (val g)) (hP : ∀ (x : ↥(even Q)), (reverseEven Q) x * x = 1 ↔ P (e x)) (x : ↥(evenUnitaryGroup Q)) : val ((evenUnitaryGroupEquivOfAlgEquiv Q e P val hval ofVal val_ofVal val_mem hP) x) = e ((evenUnitaryGroupEvenPart Q) x)

The forward generic transport applies the algebra equivalence to the even Clifford value.

@[simp]

theorem CliffordAlgebra.evenUnitaryGroupEquivOfAlgEquiv_symm_apply_evenPart {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type w} [Semiring A] [Algebra R A] {G : Type u_1} [Group G] (e : ↥(even Q) ≃ₐ[R] A) (P : A → Prop) (val : G →* A) (hval : Function.Injective ⇑val) (ofVal : (a : A) → P a → G) (val_ofVal : ∀ (a : A) (ha : P a), val (ofVal a ha) = a) (val_mem : ∀ (g : G), P (val g)) (hP : ∀ (x : ↥(even Q)), (reverseEven Q) x * x = 1 ↔ P (e x)) (g : G) : (evenUnitaryGroupEvenPart Q) ((evenUnitaryGroupEquivOfAlgEquiv Q e P val hval ofVal val_ofVal val_mem hP).symm g) = e.symm (val g)

The inverse generic transport is obtained by applying the inverse algebra equivalence.

def CliffordAlgebra.spinGroupToEvenUnitary {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↥(spinGroup Q) →* ↥(evenUnitaryGroup Q)

Forget a Spin element to the same Clifford unit in the even unitary carrier.

Equations

• CliffordAlgebra.spinGroupToEvenUnitary Q = spinGroup.toUnits.codRestrict (CliffordAlgebra.evenUnitaryGroup Q) ⋯

@[simp]

theorem CliffordAlgebra.coe_spinGroupToEvenUnitary_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(spinGroup Q)) : ↑((spinGroupToEvenUnitary Q) x) = spinGroup.toUnits x

The canonical map from Spin to the even unitary carrier does not change the underlying Clifford unit.

theorem CliffordAlgebra.spinGroupToEvenUnitary_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Function.Injective ⇑(spinGroupToEvenUnitary Q)

The canonical map from Spin to the even unitary carrier is injective.

@[simp]

theorem CliffordAlgebra.spinGroupToEvenUnitary_inj {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x y : ↥(spinGroup Q)) : (spinGroupToEvenUnitary Q) x = (spinGroupToEvenUnitary Q) y ↔ x = y

Two Spin elements have the same image in the even unitary carrier exactly when they are equal.

@[simp]

theorem CliffordAlgebra.range_spinGroup_toUnits {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : spinGroup.toUnits.range = lipschitzGroup Q ⊓ evenUnitaryGroup Q

The Spin units are precisely the Lipschitz units that lie in the even unitary carrier.

Spin action after right multiplication by a negative vector

theorem CliffordAlgebra.rightIotaEven_spinGroup_smul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (e : M) (he : Q e = -1) (s : ↥(spinGroup Q)) (m : M) : (rightIotaEven Q e) (s • m) = (evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s) * (rightIotaEven Q e) m * (conjugateNegativeIotaEven Q e he) ((reverseEven Q) ((evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s)))

Multiplication by a negative generating vector transports the Spin action into multiplication in the even Clifford algebra.

theorem CliffordAlgebra.neg_rightIotaEven_spinGroup_smul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (e : M) (he : Q e = -1) (s : ↥(spinGroup Q)) (m : M) : (-rightIotaEven Q e) (s • m) = (evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s) * (-rightIotaEven Q e) m * (conjugateNegativeIotaEven Q e he) ((reverseEven Q) ((evenUnitaryGroupEvenPart Q) ((spinGroupToEvenUnitary Q) s)))

The negated right-vector embedding satisfies the same Spin transport identity.