The special orthogonal group inside the orthogonal group

The orthogonal group O(Q) and the special orthogonal group SO(Q) both carry the subspace topology from the linear automorphism group, whose topology records an automorphism and its inverse. In this topology the determinant O(Q) →* Rˣ is continuous, so its kernel SO(Q) is closed in O(Q) over a T1 ring, and the inclusion SO(Q) →* O(Q) is a closed embedding.

When the polar form is left-separating on a finite free module over a domain, every orthogonal determinant squares to one, so the determinant takes only finitely many values and SO(Q) has finite index in O(Q). Being closed of finite index, it is then also open, and the inclusion is an open embedding. In particular, for a nondegenerate form over ℝ or ℚ_p, a compact or open subgroup of O(Q) pulls back to a compact or open subgroup of SO(Q).

Over a Hausdorff topological field with 2 invertible, SO(Q) is moreover closed in the linear automorphism group of a finite-dimensional space, hence locally compact when the field is.

Main results

• QuadraticMap.continuous_orthogonalDet: the determinant on O(Q) is continuous.
• QuadraticMap.isClosed_specialOrthogonalWithin and QuadraticMap.isClosedEmbedding_specialOrthogonalToOrthogonal: SO(Q) is closed in O(Q).
• QuadraticMap.isOpen_specialOrthogonalWithin and QuadraticMap.isOpenEmbedding_specialOrthogonalToOrthogonal: SO(Q) is open in O(Q) when the polar form is left-separating.
• TauCeti.QuadraticMap.isClosed_specialOrthogonalGroup: SO(Q) is closed in the linear automorphism group.
• TauCeti.QuadraticMap.instLocallyCompactSpaceSpecialOrthogonalGroup: SO(Q) is locally compact over a locally compact field.

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

The determinant O(Q) →* Rˣ is continuous.

theorem QuadraticMap.isClosed_specialOrthogonalWithin {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) [T1Space R] : IsClosed ↑Q.specialOrthogonalWithin

The determinant kernel SO(Q) is closed in O(Q).

theorem QuadraticMap.isClosedEmbedding_specialOrthogonalToOrthogonal {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) [T1Space R] : Topology.IsClosedEmbedding ⇑Q.specialOrthogonalToOrthogonal

The inclusion SO(Q) →* O(Q) is a closed embedding.

theorem QuadraticMap.isOpen_specialOrthogonalWithin {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {Q : QuadraticForm R M} (hQ : LinearMap.SeparatingLeft (polarBilin Q)) : IsOpen ↑(specialOrthogonalWithin Q)

If the polar form is left-separating on a finite free module over a domain, then SO(Q) is open in O(Q), being a closed subgroup of finite index.

theorem QuadraticMap.isOpenEmbedding_specialOrthogonalToOrthogonal {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {Q : QuadraticForm R M} (hQ : LinearMap.SeparatingLeft (polarBilin Q)) : Topology.IsOpenEmbedding ⇑(specialOrthogonalToOrthogonal Q)

If the polar form is left-separating on a finite free module over a domain, then the inclusion SO(Q) →* O(Q) is an open embedding.

theorem TauCeti.QuadraticMap.isClosed_specialOrthogonalGroup {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 ↑(specialOrthogonalGroup Q)

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

instance TauCeti.QuadraticMap.instLocallyCompactSpaceSpecialOrthogonalGroup {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 ↥(specialOrthogonalGroup Q)

The special orthogonal group of a finite-dimensional quadratic space over a Hausdorff locally compact topological field is locally compact.