Closedness and local compactness of the orthogonal group

For a quadratic form with separating polar form on a finite free module over a domain, every endomorphism preserving the form is automatically invertible. Thus the orthogonal group, viewed in the space of linear endomorphisms, is the common zero set of the equations Q (f x) = Q x. When the form is continuous, this image is closed. This description is useful when passing from the topology of linear endomorphisms to local orthogonal point groups.

The result holds over a Hausdorff commutative domain with module topologies and a finite free module, provided the form is continuous. A topological ring structure on the scalars supplies continuity; the theorem takes continuity directly. Local compactness is not needed for closedness, but separation is: over a semiring with the indiscrete topology the module topology on the endomorphisms is indiscrete, and the orthogonal group of any form on a nontrivial module is a nonempty proper subset of it, since it omits 0. So it is never closed there, already for Q x = x ^ 2 on a field K in dimension one, where it is {1, -1}.

Over a Hausdorff topological field, the orthogonal group of a finite-dimensional quadratic space is also closed in the linear automorphism group with its canonical topology, the one recording an automorphism and its inverse: it is the preimage of the closed set of form-preserving endomorphisms under the continuous forgetful map. When the field is moreover locally compact, the automorphism group is locally compact, so the orthogonal group is a locally compact Hausdorff topological group. This is the topology in which the orthogonal point groups over ℝ and ℚ_p are studied.

Main results

• TauCeti.QuadraticMap.isClosed_range_orthogonalGroup_toLinearMap: the orthogonal group is closed in the endomorphism space, through its underlying linear maps.
• QuadraticMap.not_isClosed_range_orthogonalGroup_toLinearMap_of_indiscreteTopology: over scalars with the indiscrete topology this fails for every quadratic map on a nontrivial module, so the T2Space hypothesis cannot be dropped.
• TauCeti.QuadraticMap.isClosed_orthogonalGroup: the orthogonal group is closed in the linear automorphism group.
• TauCeti.QuadraticMap.instLocallyCompactSpaceOrthogonalGroup: the orthogonal group is locally compact over a locally compact field.
• QuadraticMap.continuous_equivFun_orthogonalGroup_apply_basis: the coordinates of the image of a basis vector under an orthogonal transformation depend continuously on it.
• QuadraticMap.continuous_specialOrthogonalToOrthogonal: the inclusion of the special orthogonal group into the orthogonal group is continuous.

theorem TauCeti.QuadraticMap.isClosed_range_orthogonalGroup_toLinearMap {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [T2Space R] [AddCommGroup M] [Module R M] [Module.Finite R M] [TopologicalSpace M] [IsModuleTopology R M] [TopologicalSpace (Module.End R M)] [IsModuleTopology R (Module.End R M)] [IsDomain R] [Module.Free R M] (Q : QuadraticForm R M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.polarBilin Q)) (hcont : Continuous ⇑Q) : IsClosed (Set.range fun (g : ↥(orthogonalGroup Q)) => ↑↑g)

The orthogonal group of a continuous quadratic form with separating polar form on a finite free module is closed in the endomorphism space, through its underlying linear maps.

theorem QuadraticMap.not_isClosed_range_orthogonalGroup_toLinearMap_of_indiscreteTopology {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [TopologicalSpace R] [IndiscreteTopology R] [AddCommMonoid M] [Module R M] [Nontrivial M] [AddCommMonoid N] [Module R N] [TopologicalSpace (Module.End R M)] [IsModuleTopology R (Module.End R M)] (Q : QuadraticMap R M N) : ¬IsClosed (Set.range fun (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) => ↑↑g)

Over a semiring with the indiscrete topology, the orthogonal group of any quadratic map on a nontrivial module is not closed in the endomorphism space: that space is indiscrete, and the orthogonal group is nonempty and does not contain 0. Thus the separation hypothesis of isClosed_range_orthogonalGroup_toLinearMap cannot be dropped.

theorem TauCeti.QuadraticMap.isClosed_orthogonalGroup {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : IsClosed ↑(orthogonalGroup Q)

The orthogonal group of a finite-dimensional quadratic space over a Hausdorff topological field is closed in the linear automorphism group with its canonical topology. No topology on the space itself is assumed.

instance TauCeti.QuadraticMap.instLocallyCompactSpaceOrthogonalGroup {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) [LocallyCompactSpace K] : LocallyCompactSpace ↥(orthogonalGroup Q)

The orthogonal group of a finite-dimensional quadratic space over a Hausdorff locally compact topological field is locally compact, being closed in the locally compact linear automorphism group.

theorem QuadraticMap.continuous_specialOrthogonalToOrthogonal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Continuous ⇑Q.specialOrthogonalToOrthogonal

The inclusion SO(Q) →* O(Q) is continuous, both groups carrying the subspace topology from the linear automorphism group.

theorem QuadraticMap.continuous_equivFun_orthogonalGroup_apply_basis {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [AddCommGroup V] [Module K V] [Finite ι] (Q : QuadraticForm K V) (b : Module.Basis ι K V) (i : ι) : Continuous fun (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) => b.equivFun (↑g (b i))

The coordinates of the image of a basis vector under an orthogonal transformation depend continuously on the transformation.