Topology on special orthogonal groups in coordinates

For a quadratic map Q on a finite coordinate space n → R, this file induces the standard coordinate topology from the faithful map of specialOrthogonalGroup Q into GL(n, R) defined in TauCeti.LinearAlgebra.QuadraticForm.OrthogonalGroup.Basic. Over a topological ring the resulting special orthogonal group is a topological group, and it is Hausdorff when R is Hausdorff.

The construction applies to an arbitrary quadratic map on the coordinate space. It does not use a Clifford algebra or a Spin group.

Main results

• TauCeti.QuadraticMap.isEmbedding_specialOrthogonalToGeneralLinear records that it is a topological embedding.
• TauCeti.QuadraticMap.continuous_coe_specialOrthogonalGroup_pi: the inclusion into the linear automorphism group is continuous for the coordinate topology.

@[instance_reducible]

noncomputable instance TauCeti.QuadraticMap.instTopologicalSpaceSpecialOrthogonalGroupPi {n : Type u} [Fintype n] {R : Type v} [CommRing R] [TopologicalSpace R] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : TopologicalSpace ↥(specialOrthogonalGroup Q)

The canonical topology on a special orthogonal group in coordinates is induced by its faithful representation in GL(n, R).

theorem TauCeti.QuadraticMap.isEmbedding_specialOrthogonalToGeneralLinear {n : Type u} [Fintype n] {R : Type v} [CommRing R] [TopologicalSpace R] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : Topology.IsEmbedding ⇑Q.specialOrthogonalToGeneralLinear

The coordinate inclusion of a special orthogonal group is a topological embedding.

instance TauCeti.QuadraticMap.instIsTopologicalGroupSpecialOrthogonalGroupPi {n : Type u} [Fintype n] {R : Type v} [CommRing R] [TopologicalSpace R] {N : Type w} [AddCommMonoid N] [Module R N] [IsTopologicalRing R] (Q : QuadraticMap R (n → R) N) : IsTopologicalGroup ↥(specialOrthogonalGroup Q)

A special orthogonal group in coordinates over a topological ring is a topological group.

instance TauCeti.QuadraticMap.instT2SpaceSpecialOrthogonalGroupPi {n : Type u} [Fintype n] {R : Type v} [CommRing R] [TopologicalSpace R] {N : Type w} [AddCommMonoid N] [Module R N] [T2Space R] (Q : QuadraticMap R (n → R) N) : T2Space ↥(specialOrthogonalGroup Q)

A special orthogonal group in Hausdorff coordinates is Hausdorff.

theorem TauCeti.QuadraticMap.continuous_coe_specialOrthogonalGroup_pi {n : Type u} [Fintype n] {R : Type v} [CommRing R] [TopologicalSpace R] {N : Type w} [AddCommMonoid N] [Module R N] [IsTopologicalRing R] (Q : QuadraticMap R (n → R) N) : Continuous Subtype.val

The inclusion of a special orthogonal group in coordinates into the linear automorphism group is continuous for the coordinate topology. So every subset of SO(Q) that is open for its subspace topology in the linear automorphism group is also open for the coordinate topology.