Every orthogonal matrix of the plane has a Pin⁺ lift

Over a field F of characteristic not two in which every sum of two squares is a square, every orthogonal matrix P ∈ O₂(F) has a Pin⁺ lift in the Clifford model M₂(F) of the plane (TauCeti.exists_isPinLift_of_forall_isSquare); this applies to a separably closed field (TauCeti.exists_isPinLift). By the Cartan–Dieudonné theorem, in the matrix form TauCeti.closure_reflection_mul_eq_matrixSpecialOrthogonalGroup, a special orthogonal P is a product of pairs of reflections in anisotropic vectors v. Since F contains a square root s of v ⬝ᵥ v, the reflection in v is the reflection in the unit vector s⁻¹ v, which lifts its own reflection (TauCeti.isPinLift_pinVec). An orthogonal P of determinant −1 is P diag(−1, 1) · diag(−1, 1), and diag(−1, 1) is lifted by e₁.

Together with TauCeti.IsPinLift.eq_or_eq_neg this says that over such a field the lift exists and is unique up to sign: it is the input that lets a cocycle valued in O₂ be compared with one valued in the Pin⁺ model, as in Serre's computation of the Evens norm of a Kummer class.

Main results

• TauCeti.exists_isPinLift_of_forall_isSquare: every orthogonal 2 × 2 matrix over a field of characteristic not two in which sums of two squares are squares has a Pin⁺ lift.
• TauCeti.exists_isPinLift: the case of a separably closed field.

References

• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, §1.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.

theorem TauCeti.exists_isPinLift_of_forall_isSquare {F : Type u_1} [Field F] [NeZero 2] (hF : ∀ (a b : F), IsSquare (a * a + b * b)) {P : Matrix (Fin 2) (Fin 2) F} (hP : P ∈ Matrix.orthogonalGroup (Fin 2) F) : ∃ (x : Matrix (Fin 2) (Fin 2) F), IsPinLift x P

Every orthogonal matrix of the plane has a Pin⁺ lift over a field of characteristic not two in which every sum of two squares is a square, such as ℝ or a separably closed field. The lift is unique up to sign (TauCeti.IsPinLift.eq_or_eq_neg).

theorem TauCeti.exists_isPinLift {F : Type u_1} [Field F] [IsSepClosed F] [NeZero 2] {P : Matrix (Fin 2) (Fin 2) F} (hP : P ∈ Matrix.orthogonalGroup (Fin 2) F) : ∃ (x : Matrix (Fin 2) (Fin 2) F), IsPinLift x P

Every orthogonal matrix of the plane has a Pin⁺ lift over a separably closed field of characteristic not two. The lift is unique up to sign (TauCeti.IsPinLift.eq_or_eq_neg).