Orthogonal matrices as linear isometries

This file relates Mathlib's matrix orthogonal group to the linear isometry group of the corresponding Euclidean space.

Main definitions

• TauCeti.orthogonalGroupToLinearIsometryEquiv: the group homomorphism from orthogonal matrices to linear isometry equivalences of Euclidean space.

Main results

• TauCeti.continuous_orthogonalGroupToLinearIsometryEquiv: the resulting linear maps depend continuously on the matrix, for the operator-norm topology.

noncomputable def TauCeti.orthogonalGroupToLinearIsometryEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ↥(Matrix.orthogonalGroup ι ℝ) →* EuclideanSpace ℝ ι ≃ₗᵢ[ℝ] EuclideanSpace ℝ ι

An orthogonal matrix acts on Euclidean space as a linear isometry equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.orthogonalGroupToLinearIsometryEquiv_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : ↥(Matrix.orthogonalGroup ι ℝ)) (x : EuclideanSpace ℝ ι) : (orthogonalGroupToLinearIsometryEquiv A) x = WithLp.toLp 2 ((↑A).mulVec x.ofLp)

The linear isometry equivalence associated to an orthogonal matrix acts by matrix-vector multiplication in Euclidean coordinates.

theorem TauCeti.orthogonalGroupToLinearIsometryEquiv_injective {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Function.Injective ⇑orthogonalGroupToLinearIsometryEquiv

The conversion from orthogonal matrices to linear isometry equivalences is injective.

theorem TauCeti.continuous_orthogonalGroupToLinearIsometryEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Continuous fun (A : ↥(Matrix.orthogonalGroup ι ℝ)) => ↑↑(orthogonalGroupToLinearIsometryEquiv A)

The linear map of an orthogonal matrix depends continuously on the matrix: the conversion to continuous linear endomorphisms of Euclidean space is continuous for the subspace topology on the orthogonal group and the operator-norm topology.