Normed space structure on the completion of a normed space

If E is a normed space over 𝕜, then so is UniformSpace.Completion E. In this file we provide necessary instances and define UniformSpace.Completion.toComplₗᵢ - coercion E → UniformSpace.Completion E as a bundled linear isometry.

We also show that if A is a normed algebra over 𝕜, then so is UniformSpace.Completion A.

TODO: Generalise the results here from the concrete completion to any AbstractCompletion.

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instNormedSpace (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : NormedSpace 𝕜 (Completion E)

Equations

• UniformSpace.Completion.instNormedSpace 𝕜 E = { toModule := UniformSpace.Completion.instModule, norm_smul_le := ⋯ }

def UniformSpace.Completion.toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] : E →ₗᵢ[𝕜] Completion E

Embedding of a normed space to its completion as a linear isometry.

Equations

• UniformSpace.Completion.toComplₗᵢ = { toFun := UniformSpace.Completion.coe', map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem UniformSpace.Completion.coe_toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] : ⇑toComplₗᵢ = coe'

noncomputable def UniformSpace.Completion.toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] : E →L[𝕜] Completion E

Embedding of a normed space to its completion as a continuous linear map.

Equations

• UniformSpace.Completion.toComplL = UniformSpace.Completion.toComplₗᵢ.toContinuousLinearMap

@[simp]

theorem UniformSpace.Completion.coe_toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] : ⇑toComplL = coe'

@[simp]

theorem UniformSpace.Completion.norm_toComplL {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] : ‖toComplL‖ = 1

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instNormedRing (A : Type u_3) [SeminormedRing A] : NormedRing (Completion A)

Equations

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

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instNormedCommRing (A : Type u_3) [SeminormedCommRing A] : NormedCommRing (Completion A)

Equations

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

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instNormedAlgebra (𝕜 : Type u_1) (A : Type u_3) [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] : NormedAlgebra 𝕜 (Completion A)

Equations

• UniformSpace.Completion.instNormedAlgebra 𝕜 A = { toAlgebra := UniformSpace.Completion.algebra A 𝕜, norm_smul_le := ⋯ }

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instNormedFieldOfCompletableTopField (A : Type u_3) [NormedField A] [CompletableTopField A] : NormedField (Completion A)

Equations

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