Documentation

TauCeti.Topology.Algebra.OrthogonalGroup

Closedness and path components of matrix orthogonal groups #

The matrix orthogonal and special orthogonal groups are closed in the entrywise matrix topology. The orthogonal group is cut out by the transpose-inverse equations, and the special orthogonal group adds the determinant-one equation. Mathlib defines these groups as the unitary and special unitary groups for the trivial scalar star operation, so their closedness follows from the corresponding unitary results.

Over ℝ the special orthogonal group is path-connected, so two orthogonal matrices lie in the same path component exactly when they have the same determinant; for a nonempty index type the orthogonal group therefore has exactly two path components, cut out by the sign of the determinant. The special orthogonal group is generated by products r_u r_w of two reflections (TauCeti.closure_reflection_mul_eq_matrixSpecialOrthogonalGroup), and such a product is joined to r_u r_u = 1 by moving w to u: along the segment from w to u when it avoids the origin, and directly otherwise, since then w is a multiple of u and r_w = r_u. The products joined to the identity form a submonoid, which therefore contains every special orthogonal matrix.

Read through the action of orthogonal matrices on Euclidean space, two linear isometries of EuclideanSpace ℝ ι with the same determinant are joined by a path of linear isometries, continuous in the operator-norm topology.

Main results #

The closedness statements identify the topological input supplied by these carriers for later constructions of Lie-group structures and continuity arguments on the corresponding subgroups.

source
theorem TauCeti.Matrix.instContinuousStar {R : Type u_3} [CommSemiring R] [TopologicalSpace R] :
ContinuousStar R
source
theorem TauCeti.Matrix.isClosed_orthogonalGroup {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] :
IsClosed ↑(Matrix.orthogonalGroup n R)

The matrix orthogonal group is closed in the entrywise matrix topology.

source
theorem TauCeti.Matrix.isClosed_specialOrthogonalGroup {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T1Space R] :
IsClosed ↑(Matrix.specialOrthogonalGroup n R)

The matrix special orthogonal group is closed in the entrywise matrix topology.

Path components of the real orthogonal group #

source
theorem TauCeti.Matrix.continuousOn_reflectionMatrix {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
ContinuousOn (fun (u : ι → ℝ) => reflectionMatrix u (2 / u ⬝ᵥ u)) {u : ι → ℝ | u ≠ 0}

The reflection matrix u ↦ 1 - (2 / (u ⬝ᵥ u)) • vecMulVec u u in the hyperplane orthogonal to u depends continuously on the nonzero vector u.

source
instance TauCeti.Matrix.instPathConnectedSpaceSpecialOrthogonalGroup {ι : Type u_1} [Fintype ι] [DecidableEq ι] :
PathConnectedSpace ↥(Matrix.specialOrthogonalGroup ι ℝ)

The real special orthogonal group is path-connected.

source
theorem TauCeti.Matrix.joined_orthogonalGroup_iff_det_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A B : ↥(Matrix.orthogonalGroup ι ℝ)} :
Joined A B ↔ (↑A).det = (↑B).det

The path components of the real orthogonal group. Two orthogonal matrices are joined by a path of orthogonal matrices exactly when they have the same determinant.

Rotations taking one unit vector to another #

source
noncomputable def TauCeti.sphereRotation {N : ℕ} (b y : ↑(Metric.sphere 0 1)) :
↥(Matrix.specialOrthogonalGroup (Fin N) ℝ)

The rotation taking a unit vector b to a unit vector y ≠ -b: the reflection in b followed by the reflection in b + y. For y = -b it is defined to be the identity, which does not take b to -b.

Instances For
    source
    @[simp]
    theorem TauCeti.sphereRotation_neg_self {N : ℕ} (b : ↑(Metric.sphere 0 1)) :
    sphereRotation b (-b) = 1

    At the antipode -b, sphereRotation b (-b) is defined to be the identity as a fallback; it does not take b to -b.

    source
    theorem TauCeti.coe_sphereRotation_of_ne {N : ℕ} {b y : ↑(Metric.sphere 0 1)} (h : y ≠ -b) :
    ↑(sphereRotation b y) = reflectionMatrix (↑b + ↑y).ofLp (2 / (↑b + ↑y).ofLp ⬝ᵥ (↑b + ↑y).ofLp) * reflectionMatrix (↑b).ofLp 2

    Away from the antipode of b, sphereRotation b y is the product of the reflections in b + y and in b.

    source
    theorem TauCeti.sphereRotation_mulVec {N : ℕ} {b y : ↑(Metric.sphere 0 1)} (h : y ≠ -b) :
    (↑(sphereRotation b y)).mulVec (↑b).ofLp = (↑y).ofLp

    The rotation sphereRotation b y takes b to y when y ≠ -b.

    source
    theorem TauCeti.continuousOn_sphereRotation {N : ℕ} (b : ↑(Metric.sphere 0 1)) :
    ContinuousOn (sphereRotation b) {-b}ᶜ

    The rotation sphereRotation b y depends continuously on y away from -b.

    Paths of linear isometries #

    source
    theorem TauCeti.exists_path_linearIsometryEquiv_of_det_eq {ι : Type u_1} [Fintype ι] {g g' : EuclideanSpace ℝ ι ≃ₗᵢ[ℝ] EuclideanSpace ℝ ι} (h : LinearMap.det ↑g.toLinearEquiv = LinearMap.det ↑g'.toLinearEquiv) :
    ∃ (γ : ↑unitInterval → EuclideanSpace ℝ ι ≃ₗᵢ[ℝ] EuclideanSpace ℝ ι), (Continuous fun (t : ↑unitInterval) => ↑↑(γ t)) ∧ γ 0 = g ∧ γ 1 = g'

    Linear isometries of Euclidean space with the same determinant are joined by a path. Two linear isometries g and g' of EuclideanSpace ℝ ι with the same determinant are joined by a path of linear isometries, continuous in the operator-norm topology.