Normed space structure on the completion of a normed space #
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
.
@[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] :
@[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] :
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_add := _, smul_zero := _}, add_smul := _, zero_smul := _}, norm_smul_le := _}
def
uniform_space.completion.to_complₗᵢ
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 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' := _}
@[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] :
noncomputable
def
uniform_space.completion.to_complL
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[normed_add_comm_group E]
[normed_space 𝕜 E] :
Embedding of a normed space to its completion as a continuous linear map.
@[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] :
@[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] :
@[protected, instance]
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 := _}
@[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] :
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 := _}