The span of a single vector

The equivalence of 𝕜 and 𝕜 • x for x ≠ 0 are defined as continuous linear equivalence and isometry.

Main definitions

• ContinuousLinearEquiv.toSpanNonzeroSingleton: The continuous linear equivalence between 𝕜 and 𝕜 • x for x ≠ 0.
• LinearIsometryEquiv.toSpanUnitSingleton: For ‖x‖ = 1 the continuous linear equivalence is a linear isometry equivalence.

theorem LinearMap.toSpanSingleton_homothety (𝕜 : Type u_1) {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (c : 𝕜) : ‖(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

theorem LinearEquiv.toSpanNonzeroSingleton_homothety (𝕜 : Type u_1) {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜) : ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖

noncomputable def ContinuousLinearEquiv.toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] ↥(Submodule.span 𝕜 {x})

Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear equivalence from E₁ to the span of x.

Equations

• ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h = ContinuousLinearEquiv.ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ ⋯ ⋯

noncomputable def ContinuousLinearEquiv.coord (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) : ↥(Submodule.span 𝕜 {x}) →L[𝕜] 𝕜

Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear map from the span of x to 𝕜.

Equations

• ContinuousLinearEquiv.coord 𝕜 x h = ↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h))

@[simp]

theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) : ⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h)) = ⇑(ContinuousLinearEquiv.coord 𝕜 x h)

@[simp]

theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) (c : 𝕜) : (ContinuousLinearEquiv.coord 𝕜 x h) ((ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) c) = c

@[simp]

theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) (y : ↥(Submodule.span 𝕜 {x})) : (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) ((ContinuousLinearEquiv.coord 𝕜 x h) y) = y

@[simp]

theorem ContinuousLinearEquiv.coord_self (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) : (ContinuousLinearEquiv.coord 𝕜 x h) { val := x, property := ⋯ } = 1

noncomputable def LinearIsometryEquiv.toSpanUnitSingleton {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (hx : ‖x‖ = 1) : 𝕜 ≃ₗᵢ[𝕜] ↥(Submodule.span 𝕜 {x})

Given a unit element x of a normed space E over a field 𝕜, the natural linear isometry equivalence from E to the span of x.

Equations

• LinearIsometryEquiv.toSpanUnitSingleton x hx = { toLinearEquiv := LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯, norm_map' := ⋯ }

@[simp]

theorem LinearIsometryEquiv.toSpanUnitSingleton_apply {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (hx : ‖x‖ = 1) (r : 𝕜) : (LinearIsometryEquiv.toSpanUnitSingleton x hx) r = { val := r • x, property := ⋯ }