Linear isometries of the closed unit ball

A linear isometry preserves norms, so it maps the closed unit ball into the closed unit ball and the unit sphere into the unit sphere. This file records the restriction to the closed unit ball, independently of any manifold structure: it is a topological embedding, and it meets the unit sphere exactly in the image of the unit sphere. These are the point-set facts behind the smooth embedding of closed balls induced by a linear isometry, the flat disc that a great circle bounds.

Main definitions

• LinearIsometry.unitClosedBallMap: the restriction of a linear isometry to the closed unit balls.

Main results

• LinearIsometry.isometry_unitClosedBallMap, LinearIsometry.isEmbedding_unitClosedBallMap: the restriction is an isometry, hence (for a normed source) a topological embedding.

def LinearIsometry.unitClosedBallMap {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.closedBall 0 1)) : ↑(Metric.closedBall 0 1)

The restriction of a linear isometry to the closed unit balls.

Equations

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

@[simp]

theorem LinearIsometry.coe_unitClosedBallMap_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.closedBall 0 1)) : ↑(f.unitClosedBallMap x) = f ↑x

theorem LinearIsometry.isometry_unitClosedBallMap {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.unitClosedBallMap

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

theorem LinearIsometry.continuous_unitClosedBallMap {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.unitClosedBallMap

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

theorem LinearIsometry.isEmbedding_unitClosedBallMap {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.unitClosedBallMap

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