Normed space structure on the completion of a normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

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

source

@[protected, instance]

def uniform_space.completion.normed_space.to_has_uniform_continuous_const_smul (𝕜 : Type u_1) (E : Type u_2) [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

has_uniform_continuous_const_smul 𝕜 E

source

@[protected, instance]

noncomputable def uniform_space.completion.normed_space (𝕜 : Type u_1) (E : Type u_2) [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

normed_space 𝕜 (uniform_space.completion E)

Equations

uniform_space.completion.normed_space 𝕜 E = {to_module := {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul (uniform_space.completion.has_smul 𝕜 E)}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}, norm_smul_le := _}

source

def uniform_space.completion.to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

E →ₗᵢ[𝕜] uniform_space.completion E

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

Equations

uniform_space.completion.to_complₗᵢ = {to_linear_map := {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}, norm_map' := _}

source

@[simp]

theorem uniform_space.completion.coe_to_complₗᵢ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

⇑uniform_space.completion.to_complₗᵢ = coe

source

noncomputable def uniform_space.completion.to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

E →L[𝕜] uniform_space.completion E

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

Equations

uniform_space.completion.to_complL = uniform_space.completion.to_complₗᵢ.to_continuous_linear_map

source

@[simp]

theorem uniform_space.completion.coe_to_complL {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] :

⇑uniform_space.completion.to_complL = coe

source

@[simp]

theorem uniform_space.completion.norm_to_complL {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] :

‖uniform_space.completion.to_complL ‖ = 1

source

@[protected, instance]

noncomputable def uniform_space.completion.normed_ring (A : Type u_3) [semi_normed_ring A] :

normed_ring (uniform_space.completion A)

Equations

uniform_space.completion.normed_ring A = {to_has_norm := uniform_space.completion.has_norm A semi_normed_ring.to_has_norm, to_ring := {add := ring.add uniform_space.completion.ring, add_assoc := _, zero := ring.zero uniform_space.completion.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul uniform_space.completion.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg uniform_space.completion.ring, sub := ring.sub uniform_space.completion.ring, sub_eq_add_neg := _, zsmul := ring.zsmul uniform_space.completion.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast uniform_space.completion.ring, nat_cast := ring.nat_cast uniform_space.completion.ring, one := ring.one uniform_space.completion.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul uniform_space.completion.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow uniform_space.completion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space uniform_space.completion.metric_space, eq_of_dist_eq_zero := _}, dist_eq := _, norm_mul := _}

source

@[protected, instance]

noncomputable def uniform_space.completion.normed_algebra (𝕜 : Type u_1) [normed_field 𝕜] (A : Type u_3) [semi_normed_comm_ring A] [normed_algebra 𝕜 A] [has_uniform_continuous_const_smul 𝕜 A] :

normed_algebra 𝕜 (uniform_space.completion A)

Equations

uniform_space.completion.normed_algebra 𝕜 A = {to_algebra := {to_has_smul := algebra.to_has_smul (uniform_space.completion.algebra A 𝕜), to_ring_hom := algebra.to_ring_hom (uniform_space.completion.algebra A 𝕜), commutes' := _, smul_def' := _}, norm_smul_le := _}