Linear isometries of the unit sphere

A linear isometry equivalence preserves norms, so it restricts to an equivalence of unit spheres. This file develops that restriction independently of the manifold structure on spheres.

Main definitions

• LinearIsometry.unitSphereMap: the map of unit spheres obtained by restricting a linear isometry.
• LinearIsometryEquiv.unitSphereEquiv: the equivalence of unit spheres obtained by restricting a linear isometry equivalence.
• LinearIsometryEquiv.unitSphereIsometryEquiv: the isometry equivalence of unit spheres obtained by restricting a linear isometry equivalence.
• LinearIsometryEquiv.instMulActionUnitSphere: the action of the linear isometry group of E on the unit sphere of E, which is by isometries.
• LinearIsometryEquiv.isPretransitive_unitSphere: for a real inner product space this action is transitive.

Main results

• LinearIsometry.isometry_unitSphereMap, LinearIsometry.isEmbedding_unitSphereMap: the restriction of a linear isometry is an isometry, hence (for a normed source) a topological embedding.
• LinearIsometryEquiv.isometry_unitSphereEquiv: the restriction is an isometry.
• TauCeti.LinearMap.eq_of_eqOn_unitSphere: a real linear map is determined by its values on the unit sphere.

Implementation notes

The declarations extending LinearIsometry and LinearIsometryEquiv live in the root-level LinearIsometry and LinearIsometryEquiv namespaces, so receiver notation elaborates. The separate linear-map lemma remains in TauCeti.LinearMap; it has no explicit LinearMap receiver for dot notation.

def LinearIsometry.unitSphereMap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) (x : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1)

A linear isometry restricts to a map of the corresponding unit spheres.

Equations

• f.unitSphereMap x = ⟨f ↑x, ⋯⟩

@[simp]

theorem LinearIsometry.coe_unitSphereMap_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) (x : ↑(Metric.sphere 0 1)) : ↑(f.unitSphereMap x) = f ↑x

theorem LinearIsometry.isometry_unitSphereMap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) : Isometry f.unitSphereMap

The restriction of a linear isometry to the unit spheres is an isometry.

theorem LinearIsometry.continuous_unitSphereMap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) : Continuous f.unitSphereMap

The restriction of a linear isometry to the unit spheres is continuous.

@[simp]

theorem LinearIsometry.unitSphereMap_neg {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) (x : ↑(Metric.sphere 0 1)) : f.unitSphereMap (-x) = -f.unitSphereMap x

The restriction of a linear isometry to the unit spheres commutes with the antipodal map.

theorem LinearIsometry.isEmbedding_unitSphereMap {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [NormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (f : E →ₗᵢ[R] F) : Topology.IsEmbedding f.unitSphereMap

The restriction of a linear isometry to the unit spheres is a topological embedding.

theorem LinearIsometryEquiv.map_mem_unitSphere_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) (x : E) : e x ∈ Metric.sphere 0 1 ↔ x ∈ Metric.sphere 0 1

A linear isometry equivalence preserves the unit sphere: it maps unit vectors to unit vectors, and nothing else to unit vectors.

def LinearIsometryEquiv.unitSphereEquiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) : ↑(Metric.sphere 0 1) ≃ ↑(Metric.sphere 0 1)

A linear isometry equivalence restricts to an equivalence of the corresponding unit spheres.

Equations

• e.unitSphereEquiv = e.toEquiv.subtypeEquiv ⋯

@[simp]

theorem LinearIsometryEquiv.coe_unitSphereEquiv_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) (x : ↑(Metric.sphere 0 1)) : ↑(e.unitSphereEquiv x) = e ↑x

@[simp]

theorem LinearIsometryEquiv.unitSphereEquiv_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) : e.unitSphereEquiv.symm = e.symm.unitSphereEquiv

@[simp]

theorem LinearIsometryEquiv.unitSphereEquiv_refl {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : (refl R E).unitSphereEquiv = Equiv.refl ↑(Metric.sphere 0 1)

@[simp]

theorem LinearIsometryEquiv.unitSphereEquiv_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [Module R E] [Module R F] [Module R G] (e : E ≃ₗᵢ[R] F) (e' : F ≃ₗᵢ[R] G) : (e.trans e').unitSphereEquiv = e.unitSphereEquiv.trans e'.unitSphereEquiv

theorem LinearIsometryEquiv.isometry_unitSphereEquiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) : Isometry ⇑e.unitSphereEquiv

The restriction of a linear isometry equivalence to the unit sphere is an isometry for the distance the sphere inherits from E: the action of O(n + 1) on Sⁿ is by isometries of the round sphere.

def LinearIsometryEquiv.unitSphereIsometryEquiv {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) : ↑(Metric.sphere 0 1) ≃ᵢ ↑(Metric.sphere 0 1)

A linear isometry equivalence restricts to an isometry equivalence of the corresponding unit spheres.

Equations

• e.unitSphereIsometryEquiv = { toEquiv := e.unitSphereEquiv, isometry_toFun := ⋯ }

@[simp]

theorem LinearIsometryEquiv.coe_unitSphereIsometryEquiv_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) (x : ↑(Metric.sphere 0 1)) : ↑(e.unitSphereIsometryEquiv x) = e ↑x

@[simp]

theorem LinearIsometryEquiv.unitSphereIsometryEquiv_symm {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module R E] [Module R F] (e : E ≃ₗᵢ[R] F) : e.unitSphereIsometryEquiv.symm = e.symm.unitSphereIsometryEquiv

@[simp]

theorem LinearIsometryEquiv.unitSphereIsometryEquiv_refl {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : (refl R E).unitSphereIsometryEquiv = IsometryEquiv.refl ↑(Metric.sphere 0 1)

@[simp]

theorem LinearIsometryEquiv.unitSphereIsometryEquiv_trans {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [Module R E] [Module R F] [Module R G] (e : E ≃ₗᵢ[R] F) (e' : F ≃ₗᵢ[R] G) : (e.trans e').unitSphereIsometryEquiv = e.unitSphereIsometryEquiv.trans e'.unitSphereIsometryEquiv

@[instance_reducible]

instance LinearIsometryEquiv.instSMulUnitSphere {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : SMul (E ≃ₗᵢ[R] E) ↑(Metric.sphere 0 1)

A linear isometry equivalence of E acts on the unit sphere of E by restriction.

Equations

• LinearIsometryEquiv.instSMulUnitSphere = { smul := fun (e : E ≃ₗᵢ[R] E) => ⇑e.unitSphereEquiv }

@[simp]

theorem LinearIsometryEquiv.coe_smul_unitSphere {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] (e : E ≃ₗᵢ[R] E) (x : ↑(Metric.sphere 0 1)) : ↑(e • x) = e ↑x

@[instance_reducible]

instance LinearIsometryEquiv.instMulActionUnitSphere {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : MulAction (E ≃ₗᵢ[R] E) ↑(Metric.sphere 0 1)

The group of linear isometry equivalences of E acts on the unit sphere of E by restriction.

Equations

• LinearIsometryEquiv.instMulActionUnitSphere = { toSMul := LinearIsometryEquiv.instSMulUnitSphere, mul_smul := ⋯, one_smul := ⋯ }

instance LinearIsometryEquiv.instIsIsometricSMulIdElemSphereOfNatReal_tauCeti {R : Type u_1} {E : Type u_2} [Semiring R] [SeminormedAddCommGroup E] [Module R E] : IsIsometricSMul (E ≃ₗᵢ[R] E) ↑(Metric.sphere 0 1)

The linear isometry group of E acts on the unit sphere by isometries.

instance LinearIsometryEquiv.isPretransitive_unitSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : MulAction.IsPretransitive (E ≃ₗᵢ[ℝ] E) ↑(Metric.sphere 0 1)

The linear isometry group of a real inner product space acts transitively on its unit sphere: the reflection in the hyperplane orthogonal to x - y exchanges x and y.

theorem TauCeti.LinearMap.eq_of_eqOn_unitSphere {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommMonoid F] [Module ℝ F] {f g : E →ₗ[ℝ] F} (h : Set.EqOn (⇑f) (⇑g) (Metric.sphere 0 1)) : f = g

A real linear map is determined by its values on the unit sphere, since every nonzero vector is a positive multiple of a unit vector.