Functoriality of Spin groups

A linear isometry of quadratic spaces induces an algebra homomorphism of their Clifford algebras. Using the induced Lipschitz-group homomorphism, this file proves that the Clifford homomorphism preserves the Spin group and packages its restriction as a group homomorphism. Isometry equivalences induce group equivalences, and these maps commute with the vector actions. The fixed-complement result specializes this naturality to an orthogonal summand.

Main results

• QuadraticMap.Isometry.spinGroupMap is the homomorphism of Spin groups induced by a quadratic isometry.
• QuadraticMap.IsometryEquiv.spinGroupEquiv is the group equivalence induced by a quadratic isometry equivalence.
• QuadraticMap.Isometry.spinGroupMap_injective_of_leftInverse proves injectivity when the isometry has an isometric left inverse.
• QuadraticMap.Isometry.spinGroupMap_spinVectorAction proves naturality of the Spin vector action.
• QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_spinToSpecialOrthogonal proves naturality of the Spin homomorphism to the special orthogonal group.
• TauCeti.QuadraticMap.spinToOrthogonal_spinGroupEquiv proves naturality of the Spin homomorphism to the orthogonal group.
• QuadraticMap.IsometryEquiv.spinGroupMap_fixed_of_prod proves that the Spin group of one summand fixes the other summand.
• QuadraticMap.IsometryEquiv.spinGroupMap_spinVectorAction_prod combines these facts into the full action formula on an orthogonal product.

theorem QuadraticMap.Isometry.map_mem_spinGroup {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : ↥(spinGroup Q₁)) : (CliffordAlgebra.map f) ↑x ∈ spinGroup Q₂

The Clifford map induced by a quadratic isometry sends Spin elements to Spin elements.

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

The homomorphism of Spin groups induced by a quadratic isometry.

Equations

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

@[simp]

theorem QuadraticMap.Isometry.coe_spinGroupMap_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : ↥(spinGroup Q₁)) : ↑(f.spinGroupMap x) = (CliffordAlgebra.map f) ↑x

The Spin-group map is induced by the corresponding Clifford-algebra map.

@[simp]

theorem QuadraticMap.Isometry.spinGroupMap_id {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (Q₁ : QuadraticForm R M₁) : (id Q₁).spinGroupMap = MonoidHom.id ↥(spinGroup Q₁)

The identity isometry induces the identity homomorphism of a Spin group.

@[simp]

theorem QuadraticMap.Isometry.spinGroupMap_comp {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {N : Type x} [AddCommGroup N] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q : QuadraticForm R N} (f : Q₂ →qᵢ Q) (g : Q₁ →qᵢ Q₂) : f.spinGroupMap.comp g.spinGroupMap = (f.comp g).spinGroupMap

Spin-group maps respect composition of quadratic isometries.

def QuadraticMap.IsometryEquiv.spinGroupEquiv {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) : ↥(spinGroup Q₁) ≃* ↥(spinGroup Q₂)

The equivalence of Spin groups induced by a quadratic isometry equivalence.

Equations

• e.spinGroupEquiv = e.toIsometry.spinGroupMap.toMulEquiv e.symm.toIsometry.spinGroupMap ⋯ ⋯

@[simp]

theorem QuadraticMap.IsometryEquiv.spinGroupEquiv_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) (x : ↥(spinGroup Q₁)) : e.spinGroupEquiv x = e.toIsometry.spinGroupMap x

The equivalence induced on Spin groups agrees with the forward isometry map.

@[simp]

theorem QuadraticMap.IsometryEquiv.spinGroupEquiv_symm {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) : e.spinGroupEquiv.symm = e.symm.spinGroupEquiv

The inverse of the induced Spin equivalence is induced by the inverse quadratic isometry.

theorem QuadraticMap.Isometry.spinGroupMap_injective {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (hf : Function.Injective ⇑(CliffordAlgebra.map f)) : Function.Injective ⇑f.spinGroupMap

A Spin-group map is injective if its underlying Clifford-algebra map is injective.

theorem QuadraticMap.Isometry.spinGroupMap_injective_of_leftInverse {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁) (h : Function.LeftInverse ⇑g ⇑f) : Function.Injective ⇑f.spinGroupMap

A quadratic isometry with an isometric left inverse induces an injective Spin-group map.

@[simp]

theorem QuadraticMap.Isometry.spinGroupMap_spinVectorAction {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Invertible 2] (f : Q₁ →qᵢ Q₂) (x : ↥(spinGroup Q₁)) (m : M₁) : (CliffordAlgebra.spinVectorAction Q₂ (f.spinGroupMap x)) (f m) = f ((CliffordAlgebra.spinVectorAction Q₁ x) m)

Spin-group maps commute with the vector actions induced by quadratic isometries.

@[simp]

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_spinToSpecialOrthogonal {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Invertible 2] (e : IsometryEquiv Q₁ Q₂) (x : ↥(spinGroup Q₁)) : e.specialOrthogonalGroupCongr ((CliffordAlgebra.spinToSpecialOrthogonal Q₁) x) = (CliffordAlgebra.spinToSpecialOrthogonal Q₂) (e.spinGroupEquiv x)

The homomorphism from the Spin group to the special orthogonal group is natural under isometric equivalences of quadratic forms.

theorem QuadraticMap.IsometryEquiv.spinGroupMap_fixed_of_prod {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {N : Type x} [AddCommGroup N] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q : QuadraticForm R N} (e : IsometryEquiv Q (QuadraticMap.prod Q₁ Q₂)) [Invertible 2] (x : ↥(spinGroup Q₁)) (m₂ : M₂) : (CliffordAlgebra.spinVectorAction Q ((e.symm.toIsometry.comp (Isometry.inl Q₁ Q₂)).spinGroupMap x)) ((e.symm.toIsometry.comp (Isometry.inr Q₁ Q₂)) m₂) = (e.symm.toIsometry.comp (Isometry.inr Q₁ Q₂)) m₂

Under an orthogonal-product isometry, the image of the Spin group of the first summand fixes every vector in the second summand.

@[simp]

theorem QuadraticMap.IsometryEquiv.spinGroupMap_spinVectorAction_prod {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {N : Type x} [AddCommGroup N] [Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q : QuadraticForm R N} (e : IsometryEquiv Q (QuadraticMap.prod Q₁ Q₂)) [Invertible 2] (x : ↥(spinGroup Q₁)) (m₁ : M₁) (m₂ : M₂) : (CliffordAlgebra.spinVectorAction Q ((e.symm.toIsometry.comp (Isometry.inl Q₁ Q₂)).spinGroupMap x)) (e.symm (m₁, m₂)) = e.symm ((CliffordAlgebra.spinVectorAction Q₁ x) m₁, m₂)

Under an orthogonal-product isometry, the image of a Spin element acts on the first summand by the original Spin action and fixes the second summand.

@[simp]

theorem TauCeti.QuadraticMap.spinToOrthogonal_spinGroupEquiv {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Invertible 2] (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (x : ↥(spinGroup Q₁)) : (CliffordAlgebra.spinToOrthogonal Q₂) (e.spinGroupEquiv x) = e.orthogonalGroupCongr ((CliffordAlgebra.spinToOrthogonal Q₁) x)

The Spin projection to the orthogonal group commutes with isometric equivalences of quadratic forms.