The group Spinᶜ(Q)

For a nonzero real quadratic form Q, the group Spinᶜ(Q) is the quotient (Spin(Q) × U(1)) / {1, (-1, -1)} of the product of the Spin group with the unit circle by the central subgroup generated by (-1, -1). We write [s, z] for the class of (s, z). It is the structure group of a Spinᶜ structure: for Q v = -‖v‖² on an oriented four-space, its half-spin representations [s, z] ↦ z ρ^±(s) are the fibres of the spinor bundles W^± of a Spinᶜ four-manifold.

The group comes with two homomorphisms: the determinant character [s, z] ↦ z² to U(1), and the rotation homomorphism [s, z] ↦ π(s) to SO(Q) through the Spin action π : Spin(Q) → SO(Q). For a Spinᶜ structure, the determinant line L is the line bundle associated to its principal Spinᶜ bundle through the determinant character, and the frame bundle is obtained from that principal bundle through the rotation homomorphism. Both homomorphisms are well defined because (-1)² = 1 and π(-1) = 1. For a finite-dimensional nondegenerate Q in positive dimension, the kernel of their product Spinᶜ(Q) → SO(Q) × U(1) is the subgroup {1, [1, -1]} of order two, and the product is onto whenever the Spin action is. So Spinᶜ(Q) is a double cover of SO(Q) × U(1) whenever Spin(Q) is a double cover of SO(Q).

Main definitions

• CliffordAlgebra.spinCKernel Q hQ: the central subgroup of spinGroup Q × Circle generated by (-1, -1).
• CliffordAlgebra.spinCGroup Q hQ: the quotient group Spinᶜ(Q).
• CliffordAlgebra.spinCGroup.mk Q hQ: the quotient map (s, z) ↦ [s, z], and CliffordAlgebra.spinCGroup.lift: the descent of homomorphisms trivial on (-1, -1).
• CliffordAlgebra.spinCGroup.ofSpin Q hQ and CliffordAlgebra.spinCGroup.ofCircle Q hQ: the injective homomorphisms s ↦ [s, 1] and z ↦ [1, z].
• CliffordAlgebra.spinCGroup.det Q hQ: the determinant character [s, z] ↦ z².
• CliffordAlgebra.spinCGroup.toSpecialOrthogonal Q hQ: the rotation homomorphism [s, z] ↦ π(s).
• QuadraticMap.Isometry.spinCGroupMap f hQ hP: the homomorphism [s, z] ↦ [f s, z] induced by a quadratic isometry f.

Main results

• CliffordAlgebra.mem_spinCKernel_iff: the subgroup spinCKernel Q hQ is {1, (-1, -1)}.
• CliffordAlgebra.coe_spinCKernel: the underlying set of that subgroup is the diagonal pair.
• CliffordAlgebra.finite_spinCKernel: the diagonal kernel is finite.
• CliffordAlgebra.spinCGroup.mk_eq_mk_iff: [s, z] = [s', z'] exactly when (s', z') = (s, z) or (s', z') = (-s, -z).
• CliffordAlgebra.spinCGroup.mem_ker_toSpecialOrthogonal_prod_det_iff: the kernel of Spinᶜ(Q) → SO(Q) × U(1) is {1, [1, -1]}.
• CliffordAlgebra.spinCGroup.coe_ker_toSpecialOrthogonal_prod_det: the underlying set of that kernel is the pair {1, [1, -1]}.
• CliffordAlgebra.spinCGroup.finite_ker_toSpecialOrthogonal_prod_det: that kernel is finite.
• CliffordAlgebra.spinCGroup.toSpecialOrthogonal_prod_det_surjective: this map is onto when the Spin action is onto SO(Q).
• CliffordAlgebra.spinCGroup.circle_hom_ext: a homomorphism from the circle to Spinᶜ(Q) is determined by its composite with Spinᶜ(Q) → SO(Q) × U(1).
• QuadraticMap.Isometry.det_spinCGroupMap and QuadraticMap.Isometry.toSpecialOrthogonal_spinCGroupMap_apply: the induced map preserves the determinant character, and its rotations extend the rotations of the source along f.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Appendix D.
• J. W. Morgan, The Seiberg–Witten equations and applications to the topology of smooth four-manifolds, Mathematical Notes 44, Princeton University Press, 1996, §3.1.

noncomputable def CliffordAlgebra.spinCKernel {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Subgroup (↥(spinGroup Q) × Circle)

The central subgroup of spinGroup Q × Circle generated by (-1, -1). The group Spinᶜ(Q) is the quotient by it.

theorem CliffordAlgebra.mem_spinCKernel_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) {p : ↥(spinGroup Q) × Circle} : p ∈ spinCKernel Q hQ ↔ p = 1 ∨ p = (spinGroup.negOne Q hQ, -1)

The subgroup spinCKernel Q hQ consists of 1 and (-1, -1).

theorem CliffordAlgebra.coe_spinCKernel {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : ↑(spinCKernel Q hQ) = {1, (spinGroup.negOne Q hQ, -1)}

The underlying set of spinCKernel Q hQ is the diagonal pair {1, (-1, -1)}.

theorem CliffordAlgebra.finite_spinCKernel {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (↑(spinCKernel Q hQ)).Finite

The diagonal order-two kernel defining Spinᶜ(Q) is finite.

theorem CliffordAlgebra.negOne_neg_one_mem_spinCKernel {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (spinGroup.negOne Q hQ, -1) ∈ spinCKernel Q hQ

(-1, -1) lies in spinCKernel Q hQ.

theorem CliffordAlgebra.spinCKernel_le_center {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : spinCKernel Q hQ ≤ Subgroup.center (↥(spinGroup Q) × Circle)

The subgroup spinCKernel Q hQ is central.

instance CliffordAlgebra.instNormalProdSubtypeRealMemSubmonoidSpinGroupCircleSpinCKernel {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (spinCKernel Q hQ).Normal

@[reducible, inline]

abbrev CliffordAlgebra.spinCGroup {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Type u_1

The group Spinᶜ(Q): the quotient (Spin(Q) × U(1)) / {1, (-1, -1)}. For Q v = -‖v‖² on a real inner product space of dimension n, this is Spinᶜ(n), the structure group of a Spinᶜ structure.

noncomputable def CliffordAlgebra.spinCGroup.mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : ↥(spinGroup Q) × Circle →* spinCGroup Q hQ

The quotient map Spin(Q) × U(1) → Spinᶜ(Q), (s, z) ↦ [s, z].

theorem CliffordAlgebra.spinCGroup.mk_apply {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (p : ↥(spinGroup Q) × Circle) : (mk Q hQ) p = ↑p

mk is the quotient map.

theorem CliffordAlgebra.spinCGroup.coe_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : ⇑(mk Q hQ) = QuotientGroup.mk

The underlying function of mk is the quotient projection. This is not a simp lemma: simplifying partially applied mk would prevent representative lemmas from matching.

theorem CliffordAlgebra.spinCGroup.mk_surjective {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Function.Surjective ⇑(mk Q hQ)

Every element of Spinᶜ(Q) is a class [s, z].

@[simp]

theorem CliffordAlgebra.spinCGroup.ker_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (mk Q hQ).ker = spinCKernel Q hQ

The kernel of the quotient map is {1, (-1, -1)}.

theorem CliffordAlgebra.spinCGroup.card_fiber_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (x : spinCGroup Q hQ) : Nat.card ↑(⇑(mk Q hQ) ⁻¹' {x}) = 2

Every fibre of Spin(Q) × Circle → Spinᶜ(Q) has exactly two elements.

@[simp]

theorem CliffordAlgebra.spinCGroup.mk_negOne_neg_one {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (mk Q hQ) (spinGroup.negOne Q hQ, -1) = 1

[-1, -1] = 1 in Spinᶜ(Q).

theorem CliffordAlgebra.spinCGroup.mk_eq_mk_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) {p p' : ↥(spinGroup Q) × Circle} : (mk Q hQ) p = (mk Q hQ) p' ↔ p' = p ∨ p' = (spinGroup.negOne Q hQ, -1) * p

[s, z] = [s', z'] exactly when (s', z') = (s, z) or (s', z') = (-s, -z).

noncomputable def CliffordAlgebra.spinCGroup.lift {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) {G : Type u_2} [Monoid G] (f : ↥(spinGroup Q) × Circle →* G) (hf : f (spinGroup.negOne Q hQ, -1) = 1) : spinCGroup Q hQ →* G

The universal property of Spinᶜ(Q): a homomorphism out of Spin(Q) × U(1) that is trivial on (-1, -1) descends to Spinᶜ(Q).

@[simp]

theorem CliffordAlgebra.spinCGroup.lift_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) {G : Type u_2} [Monoid G] (f : ↥(spinGroup Q) × Circle →* G) (hf : f (spinGroup.negOne Q hQ, -1) = 1) (p : ↥(spinGroup Q) × Circle) : (lift Q hQ f hf) ((mk Q hQ) p) = f p

@[simp]

theorem CliffordAlgebra.spinCGroup.lift_comp_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) {G : Type u_2} [Monoid G] (f : ↥(spinGroup Q) × Circle →* G) (hf : f (spinGroup.negOne Q hQ, -1) = 1) : (lift Q hQ f hf).comp (mk Q hQ) = f

The composite of lift f with the quotient map is f.

noncomputable def CliffordAlgebra.spinCGroup.ofSpin {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : ↥(spinGroup Q) →* spinCGroup Q hQ

The inclusion Spin(Q) → Spinᶜ(Q), s ↦ [s, 1].

noncomputable def CliffordAlgebra.spinCGroup.ofCircle {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Circle →* spinCGroup Q hQ

The inclusion U(1) → Spinᶜ(Q), z ↦ [1, z].

theorem CliffordAlgebra.spinCGroup.ofSpin_apply {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (s : ↥(spinGroup Q)) : (ofSpin Q hQ) s = (mk Q hQ) (s, 1)

theorem CliffordAlgebra.spinCGroup.ofCircle_apply {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (z : Circle) : (ofCircle Q hQ) z = (mk Q hQ) (1, z)

theorem CliffordAlgebra.spinCGroup.ofSpin_mul_ofCircle {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (s : ↥(spinGroup Q)) (z : Circle) : (ofSpin Q hQ) s * (ofCircle Q hQ) z = (mk Q hQ) (s, z)

The class [s, z] is the product [s, 1] [1, z].

theorem CliffordAlgebra.spinCGroup.ofCircle_mem_center {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (z : Circle) : (ofCircle Q hQ) z ∈ Subgroup.center (spinCGroup Q hQ)

The circle factor is central in Spinᶜ(Q).

theorem CliffordAlgebra.spinCGroup.ofSpin_negOne {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : (ofSpin Q hQ) (spinGroup.negOne Q hQ) = (ofCircle Q hQ) (-1)

The two inclusions agree on -1: [-1, 1] = [1, -1].

theorem CliffordAlgebra.spinCGroup.ofSpin_injective {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Function.Injective ⇑(ofSpin Q hQ)

Spin(Q) is a subgroup of Spinᶜ(Q).

theorem CliffordAlgebra.spinCGroup.ofCircle_injective {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : Function.Injective ⇑(ofCircle Q hQ)

U(1) is a subgroup of Spinᶜ(Q).

The determinant character

noncomputable def CliffordAlgebra.spinCGroup.det {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : spinCGroup Q hQ →* Circle

The determinant character Spinᶜ(Q) → U(1), [s, z] ↦ z², well defined because (-1)² = 1. The determinant line of a Spinᶜ structure is the line bundle associated to its principal Spinᶜ bundle through this character.

@[simp]

theorem CliffordAlgebra.spinCGroup.det_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (p : ↥(spinGroup Q) × Circle) : (det Q hQ) ((mk Q hQ) p) = p.2 ^ 2

@[simp]

theorem CliffordAlgebra.spinCGroup.det_ofSpin {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (s : ↥(spinGroup Q)) : (det Q hQ) ((ofSpin Q hQ) s) = 1

@[simp]

theorem CliffordAlgebra.spinCGroup.det_ofCircle {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (z : Circle) : (det Q hQ) ((ofCircle Q hQ) z) = z ^ 2

The rotation homomorphism

noncomputable def CliffordAlgebra.spinCGroup.toSpecialOrthogonal {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) : spinCGroup Q hQ →* ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

The rotation homomorphism Spinᶜ(Q) → SO(Q), [s, z] ↦ π(s), through the Spin action π; it is well defined because π(-1) = 1.

@[simp]

theorem CliffordAlgebra.spinCGroup.toSpecialOrthogonal_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (p : ↥(spinGroup Q) × Circle) : (toSpecialOrthogonal Q hQ) ((mk Q hQ) p) = (spinToSpecialOrthogonal Q) p.1

@[simp]

theorem CliffordAlgebra.spinCGroup.toSpecialOrthogonal_ofSpin {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (s : ↥(spinGroup Q)) : (toSpecialOrthogonal Q hQ) ((ofSpin Q hQ) s) = (spinToSpecialOrthogonal Q) s

@[simp]

theorem CliffordAlgebra.spinCGroup.toSpecialOrthogonal_ofCircle {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (z : Circle) : (toSpecialOrthogonal Q hQ) ((ofCircle Q hQ) z) = 1

Spinᶜ(Q) as a double cover of SO(Q) × U(1)

theorem CliffordAlgebra.spinCGroup.mem_ker_toSpecialOrthogonal_prod_det_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) [FiniteDimensional ℝ M] (hQn : QuadraticMap.Nondegenerate) (x : spinCGroup Q hQ) : x ∈ ((toSpecialOrthogonal Q hQ).prod (det Q hQ)).ker ↔ x = 1 ∨ x = (ofCircle Q hQ) (-1)

The kernel of Spinᶜ(Q) → SO(Q) × U(1), [s, z] ↦ (π(s), z²), is {1, [1, -1]} for a finite-dimensional nondegenerate quadratic form in positive dimension.

theorem CliffordAlgebra.spinCGroup.coe_ker_toSpecialOrthogonal_prod_det {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) [FiniteDimensional ℝ M] (hQn : QuadraticMap.Nondegenerate) : ↑((toSpecialOrthogonal Q hQ).prod (det Q hQ)).ker = {1, (ofCircle Q hQ) (-1)}

The underlying set of the frame-and-determinant kernel is {1, [1, -1]} for a finite-dimensional nondegenerate form in positive dimension.

theorem CliffordAlgebra.spinCGroup.finite_ker_toSpecialOrthogonal_prod_det {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) [FiniteDimensional ℝ M] (hQn : QuadraticMap.Nondegenerate) : (↑((toSpecialOrthogonal Q hQ).prod (det Q hQ)).ker).Finite

The frame-and-determinant kernel is finite for a nondegenerate form in positive finite dimension.

theorem CliffordAlgebra.spinCGroup.toSpecialOrthogonal_prod_det_surjective {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) (h : Function.Surjective ⇑(spinToSpecialOrthogonal Q)) : Function.Surjective ⇑((toSpecialOrthogonal Q hQ).prod (det Q hQ))

Spinᶜ(Q) → SO(Q) × U(1) is onto whenever the Spin action is onto SO(Q): every unit complex number has a square root on the circle.

theorem CliffordAlgebra.spinCGroup.card_fiber_toSpecialOrthogonal_prod_det {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) [FiniteDimensional ℝ M] (hQn : QuadraticMap.Nondegenerate) (hsurj : Function.Surjective ⇑((toSpecialOrthogonal Q hQ).prod (det Q hQ))) (y : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) × Circle) : Nat.card ↑(⇑((toSpecialOrthogonal Q hQ).prod (det Q hQ)) ⁻¹' {y}) = 2

Every fibre of the frame-and-determinant map has two elements when it is surjective and the form is nondegenerate in positive finite dimension.

Homomorphisms from the circle

theorem CliffordAlgebra.spinCGroup.circle_hom_ext {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (hQ : Q ≠ 0) [FiniteDimensional ℝ M] (hQn : QuadraticMap.Nondegenerate) {φ ψ : Circle →* spinCGroup Q hQ} (h : ((toSpecialOrthogonal Q hQ).prod (det Q hQ)).comp φ = ((toSpecialOrthogonal Q hQ).prod (det Q hQ)).comp ψ) : φ = ψ

A homomorphism from the circle to Spinᶜ(Q) is determined by its composite with Spinᶜ(Q) → SO(Q) × U(1), for a finite-dimensional nondegenerate form. Two such homomorphisms differ by a homomorphism into the central kernel {1, [1, -1]}, and this is trivial because every point of the circle is a square while the kernel has exponent two.

Functoriality

noncomputable def QuadraticMap.Isometry.spinCGroupMap {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) : CliffordAlgebra.spinCGroup Q hQ →* CliffordAlgebra.spinCGroup P hP

The homomorphism of Spinᶜ groups induced by a quadratic isometry f, [s, z] ↦ [f s, z], where f s is the image of s under the induced homomorphism QuadraticMap.Isometry.spinGroupMap of Spin groups. It is well defined because f preserves the scalar -1. For the inclusion of an orthogonal summand, such as the stabilization V → ℝ × V by an extra line, it extends the structure group of a Spinᶜ structure on V to that of ℝ × V.

@[simp]

theorem QuadraticMap.Isometry.spinCGroupMap_mk {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (p : ↥(spinGroup Q) × Circle) : (f.spinCGroupMap hQ hP) ((CliffordAlgebra.spinCGroup.mk Q hQ) p) = (CliffordAlgebra.spinCGroup.mk P hP) (f.spinGroupMap p.1, p.2)

The induced map sends [s, z] to [f s, z].

@[simp]

theorem QuadraticMap.Isometry.spinCGroupMap_ofSpin {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (s : ↥(spinGroup Q)) : (f.spinCGroupMap hQ hP) ((CliffordAlgebra.spinCGroup.ofSpin Q hQ) s) = (CliffordAlgebra.spinCGroup.ofSpin P hP) (f.spinGroupMap s)

@[simp]

theorem QuadraticMap.Isometry.spinCGroupMap_ofCircle {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (z : Circle) : (f.spinCGroupMap hQ hP) ((CliffordAlgebra.spinCGroup.ofCircle Q hQ) z) = (CliffordAlgebra.spinCGroup.ofCircle P hP) z

@[simp]

theorem QuadraticMap.Isometry.spinCGroupMap_id {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (hQ : Q ≠ 0) : (id Q).spinCGroupMap hQ hQ = MonoidHom.id (CliffordAlgebra.spinCGroup Q hQ)

The identity isometry induces the identity of Spinᶜ(Q).

@[simp]

theorem QuadraticMap.Isometry.spinCGroupMap_comp {M : Type u_1} {N : Type u_2} {L : Type u_3} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] [AddCommGroup L] [Module ℝ L] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} {R : QuadraticForm ℝ L} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (g : P →qᵢ R) (hR : R ≠ 0) : (g.spinCGroupMap hP hR).comp (f.spinCGroupMap hQ hP) = (g.comp f).spinCGroupMap hQ hR

The maps induced by quadratic isometries respect composition.

@[simp]

theorem QuadraticMap.Isometry.det_spinCGroupMap {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (x : CliffordAlgebra.spinCGroup Q hQ) : (CliffordAlgebra.spinCGroup.det P hP) ((f.spinCGroupMap hQ hP) x) = (CliffordAlgebra.spinCGroup.det Q hQ) x

The induced map preserves the determinant character.

@[simp]

theorem QuadraticMap.Isometry.toSpecialOrthogonal_spinCGroupMap_apply {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℝ M] [AddCommGroup N] [Module ℝ N] {Q : QuadraticForm ℝ M} {P : QuadraticForm ℝ N} (f : Q →qᵢ P) (hQ : Q ≠ 0) (hP : P ≠ 0) (x : CliffordAlgebra.spinCGroup Q hQ) (m : M) : ↑((CliffordAlgebra.spinCGroup.toSpecialOrthogonal P hP) ((f.spinCGroupMap hQ hP) x)) (f m) = f (↑((CliffordAlgebra.spinCGroup.toSpecialOrthogonal Q hQ) x) m)

The rotation of an induced element extends the rotation of the source along f: on the image of f, the rotation π([f s, z]) acts as f ∘ π([s, z]).