Determinant square classes of orthogonal transformations

The determinant of an orthogonal transformation of a finite-dimensional space is a unit. Reducing that unit modulo squares gives a homomorphism from the orthogonal group to the square-class group. This construction only uses the orthogonal group and does not require a characteristic assumption.

Main definitions and results

• QuadraticMap.orthogonalDetSquareClass: the determinant modulo squares on O(Q).
• QuadraticMap.orthogonalDetSquareClass_apply: its value on an orthogonal transformation.

noncomputable def QuadraticMap.orthogonalDetSquareClass {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {N : Type w} [AddCommMonoid N] [Module K N] [FiniteDimensional K V] (Q : QuadraticMap K V N) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q) →* Multiplicative (TauCeti.SquareClassGroup K)

The determinant of an orthogonal transformation, reduced modulo squares.

Equations

• Q.orthogonalDetSquareClass = TauCeti.squareClassHom.comp (LinearEquiv.det.comp (TauCeti.QuadraticMap.orthogonalGroup Q).subtype)

@[simp]

theorem QuadraticMap.orthogonalDetSquareClass_apply {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] {N : Type w} [AddCommMonoid N] [Module K N] [FiniteDimensional K V] (Q : QuadraticMap K V N) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) : Q.orthogonalDetSquareClass g = TauCeti.squareClassHom (LinearEquiv.det ↑g)

The determinant square-class map evaluates by taking the determinant modulo squares.