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] [NormSMulClass 𝕜 E] (x : E) (c : 𝕜) : ‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

theorem LinearEquiv.toSpanNonzeroSingleton_homothety (𝕜 : Type u_1) {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜) : ‖(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 𝕜 to the span of x.

Equations

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

@[simp]

theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) (a✝ : 𝕜) : ↑((toSpanNonzeroSingleton 𝕜 x h) a✝) = a✝ • x

@[simp]

theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) (a✝ : ↥(Submodule.span 𝕜 {x})) : (toSpanNonzeroSingleton 𝕜 x h).symm a✝ = (LinearEquiv.ofInjective (LinearMap.toSpanSingleton 𝕜 E x) ⋯).symm ((LinearEquiv.ofEq (Submodule.span 𝕜 {x}) (LinearMap.range (LinearMap.toSpanSingleton 𝕜 E x)) ⋯) a✝)

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

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.toSpanNonzeroSingleton 𝕜 x h).symm

@[simp]

theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm (𝕜 : Type u_1) {E : Type u_2} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) : ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = ⇑(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 : 𝕜) : (coord 𝕜 x h) ((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})) : (toSpanNonzeroSingleton 𝕜 x h) ((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) : (coord 𝕜 x h) ⟨x, ⋯⟩ = 1

noncomputable def LinearIsometryEquiv.toSpanUnitSingleton {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 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 𝕜 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] [NormSMulClass 𝕜 E] (x : E) (hx : ‖x‖ = 1) (r : 𝕜) : (toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩