Orthogonal groups in dimension one

On a free module of rank one over an integral domain every linear endomorphism is a scalar c, and c preserves a nonzero quadratic map valued in a torsion-free module exactly when c * c = 1, that is when c = 1 or c = -1. So the orthogonal group of such a quadratic map on a line is {1, -1}, of order two when 2 ≠ 0, and the reflection in any vector of invertible norm is -1.

Together with the triviality of the special orthogonal group in rank at most one (QuadraticMap.specialOrthogonalGroup_eq_bot_of_finrank_le_one), this is the dimension-one boundary case of the orthogonal-group calculations: for Q x = a x² with a ≠ 0 over a field, the group O(Q) is {±1}, SO(Q) is trivial, and -1 is the reflection in every nonzero vector. The last fact is what computes the spinor norm of -1 as the square class of a (CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_smul_sq).

Main results

• TauCeti.QuadraticMap.mem_orthogonalGroup_iff_of_finrank_eq_one: in rank one, the isometries of a nonzero quadratic map valued in a torsion-free module are exactly 1 and -1.
• TauCeti.QuadraticMap.eq_one_or_eq_negOrthogonal_of_finrank_eq_one: the same dichotomy for elements of the orthogonal group.
• TauCeti.QuadraticMap.card_orthogonalGroup_of_finrank_eq_one: if moreover 2 ≠ 0, the orthogonal group has exactly two elements.
• QuadraticMap.reflection_eq_neg_of_finrank_eq_one and QuadraticMap.reflectionOrthogonal_eq_negOrthogonal_of_finrank_eq_one: in rank one, the reflection in any vector of invertible norm is -1.

theorem TauCeti.QuadraticMap.mem_orthogonalGroup_iff_of_finrank_eq_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [Module.IsTorsionFree R N] {Q : QuadraticMap R M N} (hQ : Q ≠ 0) (hM : Module.finrank R M = 1) {f : M ≃ₗ[R] M} : f ∈ orthogonalGroup Q ↔ f = 1 ∨ f = LinearEquiv.neg R

The orthogonal group of a line. On a free module of rank one over a domain, the isometries of a nonzero quadratic map valued in a torsion-free module are exactly 1 and -1.

theorem TauCeti.QuadraticMap.eq_one_or_eq_negOrthogonal_of_finrank_eq_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [Module.IsTorsionFree R N] {Q : QuadraticMap R M N} (hQ : Q ≠ 0) (hM : Module.finrank R M = 1) (g : ↥(orthogonalGroup Q)) : g = 1 ∨ g = Q.negOrthogonal

In rank one, every isometry of a nonzero quadratic map is 1 or Q.negOrthogonal.

theorem QuadraticMap.negOrthogonal_ne_one_of_finrank_eq_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [NeZero 2] (Q : QuadraticMap R M N) (hM : Module.finrank R M = 1) : Q.negOrthogonal ≠ 1

When 2 ≠ 0, negation is a nontrivial isometry of a module of rank one.

theorem TauCeti.QuadraticMap.card_orthogonalGroup_of_finrank_eq_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [AddCommGroup N] [Module R N] [NeZero 2] [Module.IsTorsionFree R N] {Q : QuadraticMap R M N} (hQ : Q ≠ 0) (hM : Module.finrank R M = 1) : Nat.card ↥(orthogonalGroup Q) = 2

The orthogonal group of a line has order two. On a free module of rank one over a domain in which 2 ≠ 0, a nonzero quadratic map valued in a torsion-free module has exactly the two isometries 1 and -1.

theorem QuadraticMap.reflection_eq_neg_of_finrank_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] (hM : Module.finrank R M = 1) : TauCeti.QuadraticMap.reflection Q v = LinearEquiv.neg R

In rank one, every reflection is -1. The reflection in a vector of invertible norm on a free module of rank one over a domain is negation.

theorem QuadraticMap.reflectionOrthogonal_eq_negOrthogonal_of_finrank_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] (hM : Module.finrank R M = 1) : TauCeti.QuadraticMap.reflectionOrthogonal Q v = negOrthogonal Q

In rank one, the bundled reflection in a vector of invertible norm is Q.negOrthogonal.