Mathlib.Analysis.Normed.Module.Completion

Module docstring

{"# 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. "}

UniformSpace.Completion.instNormedSpace instance

[NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : NormedSpace 𝕜 (Completion E)

Full source

instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
    NormedSpace 𝕜 (Completion E) where
  norm_smul_le := norm_smul_le

Normed Space Structure on the Completion of a Normed Space

Informal description

For any normed field $\mathbb{K}$ and normed space $E$ over $\mathbb{K}$, the completion $\overline{E}$ of $E$ is also a normed space over $\mathbb{K}$. This instance provides the normed space structure on the completion, extending the normed space structure of $E$.

UniformSpace.Completion.toComplₗᵢ definition

: E →ₗᵢ[𝕜] Completion E

Full source

/-- Embedding of a normed space to its completion as a linear isometry. -/
def toComplₗᵢ : E →ₗᵢ[𝕜] Completion E :=
  { toCompl with
    toFun := (↑)
    map_smul' := coe_smul
    norm_map' := norm_coe }

Linear isometric embedding into normed space completion

Informal description

The linear isometric embedding from a normed space $E$ over a normed field $\mathbb{K}$ to its completion $\overline{E}$, which maps each element $x \in E$ to its image in the completion while preserving the norm: $\|x\| = \|\overline{x}\|$. This map is linear and preserves scalar multiplication.

UniformSpace.Completion.coe_toComplₗᵢ theorem

: ⇑(toComplₗᵢ : E →ₗᵢ[𝕜] Completion E) = ((↑) : E → Completion E)

Full source

@[simp]
theorem coe_toComplₗᵢ : ⇑(toComplₗᵢ : E →ₗᵢ[𝕜] Completion E) = ((↑) : E → Completion E) :=
  rfl

Coincidence of Linear Isometric Embedding and Canonical Embedding in Normed Space Completion

Informal description

The underlying function of the linear isometric embedding `toComplₗᵢ` from a normed space $E$ over $\mathbb{K}$ to its completion $\overline{E}$ coincides with the canonical embedding map $E \to \overline{E}$.

UniformSpace.Completion.toComplL definition

: E →L[𝕜] Completion E

Full source

/-- Embedding of a normed space to its completion as a continuous linear map. -/
def toComplL : E →L[𝕜] Completion E :=
  toComplₗᵢ.toContinuousLinearMap

Continuous linear embedding into normed space completion

Informal description

The continuous linear map embedding a normed space $ E $ over the field $ \mathbb{K} $ into its completion $ \overline{E} $, obtained by converting the linear isometric embedding $ \text{toComplₗᵢ} $ into a continuous linear map. This map preserves the norm and is linear with respect to the field $ \mathbb{K} $.

UniformSpace.Completion.coe_toComplL theorem

: ⇑(toComplL : E →L[𝕜] Completion E) = ((↑) : E → Completion E)

Full source

@[simp]
theorem coe_toComplL : ⇑(toComplL : E →L[𝕜] Completion E) = ((↑) : E → Completion E) :=
  rfl

Coincidence of Continuous Linear Embedding and Canonical Embedding in Normed Space Completion

Informal description

The underlying function of the continuous linear map $\text{toComplL} : E \to_{\mathbb{K}} \overline{E}$ coincides with the canonical embedding map $E \to \overline{E}$, where $\overline{E}$ is the completion of the normed space $E$ over the field $\mathbb{K}$.

UniformSpace.Completion.norm_toComplL theorem

 {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :
  ‖(toComplL : E →L[𝕜] Completion E)‖ = 1

Full source

@[simp]
theorem norm_toComplL {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] [Nontrivial E] : ‖(toComplL : E →L[𝕜] Completion E)‖ = 1 :=
  (toComplₗᵢ : E →ₗᵢ[𝕜] Completion E).norm_toContinuousLinearMap

Operator Norm of Completion Embedding is One

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $E$ a nontrivial normed space over $\mathbb{K}$. The operator norm of the continuous linear embedding $\text{toComplL} \colon E \to \overline{E}$ from $E$ to its completion $\overline{E}$ is equal to $1$.

UniformSpace.Completion.instNormedRing instance

[SeminormedRing A] : NormedRing (Completion A)

Full source

instance [SeminormedRing A] : NormedRing (Completion A) where
  __ : NormedAddCommGroup (Completion A) := inferInstance
  __ : Ring (Completion A) := inferInstance
  norm_mul_le x y := by
    induction x, y using induction_on₂ with
    | hp => apply isClosed_le <;> fun_prop
    | ih x y => simpa only [← coe_mul, norm_coe] using norm_mul_le x y

Completion of a Seminormed Ring is a Normed Ring

Informal description

For any seminormed ring $A$, the completion of $A$ as a uniform space is a normed ring.

UniformSpace.Completion.instNormedCommRing instance

[SeminormedCommRing A] : NormedCommRing (Completion A)

Full source

instance [SeminormedCommRing A] : NormedCommRing (Completion A) where
  __ : CommRing (Completion A) := inferInstance
  __ : NormedRing (Completion A) := inferInstance

Completion of a Seminormed Commutative Ring is a Normed Commutative Ring

Informal description

For any seminormed commutative ring $A$, the Hausdorff completion of $A$ as a uniform space is a normed commutative ring.

UniformSpace.Completion.instNormedAlgebra instance

[NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] : NormedAlgebra 𝕜 (Completion A)

Full source

instance [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] :
    NormedAlgebra 𝕜 (Completion A) where
  norm_smul_le := norm_smul_le

Completion of a Normed Algebra is a Normed Algebra

Informal description

For any normed field $\mathbb{K}$ and seminormed commutative ring $A$ that is a normed algebra over $\mathbb{K}$, the completion of $A$ as a uniform space is also a normed algebra over $\mathbb{K}$.

UniformSpace.Completion.instNormedFieldOfCompletableTopField instance

[NormedField A] [CompletableTopField A] : NormedField (UniformSpace.Completion A)

Full source

instance [NormedField A] [CompletableTopField A] :
    NormedField (UniformSpace.Completion A) where
  __ : NormedCommRing (Completion A) := inferInstance
  __ : Field (Completion A) := inferInstance
  norm_mul x y := induction_on₂ x y (isClosed_eq (by fun_prop) (by fun_prop)) (by simp [← coe_mul])

Completion of a Normed Completable Topological Field is a Normed Field

Informal description

For any normed field $A$ that is also a completable topological field, the completion $\hat{A}$ of $A$ as a uniform space is a normed field.