Special orthogonal groups in rank at most one

A determinant-one automorphism of a finite free module of rank at most one over a commutative ring is the identity. Thus its special orthogonal group is trivial, even for a degenerate quadratic form and in characteristic two. This supplies the low-dimensional boundary of spinor-norm image calculations.

@[simp]

theorem QuadraticMap.specialOrthogonalGroup_eq_bot_of_finrank_le_one {R : Type u_1} {V : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R V N) (hV : Module.finrank R V ≤ 1) : TauCeti.QuadraticMap.specialOrthogonalGroup Q = ⊥

The special orthogonal group of a quadratic map on a finite free module of rank at most one is trivial. No nondegeneracy or characteristic assumption is needed.