Continuity of isometric transport of orthogonal groups

An isometric equivalence e : Q₁ ≃ Q₂ of quadratic maps identifies O(Q₁) with O(Q₂), and SO(Q₁) with SO(Q₂), by conjugation. Both groups carry the subspace topology from the forward-and-inverse topology on linear automorphisms, in which conjugation by a linear equivalence is continuous (LinearEquiv.continuous_autCongr). So the transport is continuous, and, its inverse being transport along e.symm, it is a homeomorphism. In particular it carries compact and open subgroups of one orthogonal group onto compact and open subgroups of the other, which is what lets compact-open reference subgroups be moved along an isometry of local quadratic spaces.

Main results

• QuadraticMap.IsometryEquiv.continuous_orthogonalGroupCongr: transport of orthogonal groups along an isometry is continuous.
• QuadraticMap.IsometryEquiv.continuous_specialOrthogonalGroupCongr: the same for special orthogonal groups.

theorem QuadraticMap.IsometryEquiv.continuous_orthogonalGroupCongr {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommSemiring R] [TopologicalSpace R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : Continuous ⇑e.orthogonalGroupCongr

Transport of orthogonal groups along an isometric equivalence is continuous.

theorem QuadraticMap.IsometryEquiv.continuous_specialOrthogonalGroupCongr {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [TopologicalSpace R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : Continuous ⇑e.specialOrthogonalGroupCongr

Transport of special orthogonal groups along an isometric equivalence is continuous.