Completion of continuous (semi-)linear maps:

This file has a declaration that enables a continuous (semi-)linear map between modules to be lifted to a continuous semilinear map between the completions of those modules.

Main declarations

• ContinuousLinearMap.completion: promotes a continuous semilinear map from α to β to a continuous semilinear map from Completion α to Completion β.
• ContinuousLinearMap.fromCompletion: promotes a continuous semilinear map from α to β to a continuous semilinear map from Completion α to β.

noncomputable def ContinuousLinearMap.completion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} (f : α →SL[σ] β) : UniformSpace.Completion α →SL[σ] UniformSpace.Completion β

Lift a continuous semilinear map to a continuous semilinear map between the UniformSpace.Completions of the spaces. This is UniformSpace.Completion.map bundled as a continuous linear map when the input is itself a continuous linear map.

Equations

• f.completion = { toFun := (↑((↑f).toAddMonoidHom.completion ⋯)).toFun, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.toAddMonoidHom_completion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} (f : α →SL[σ] β) : (↑f.completion).toAddMonoidHom = (↑f).toAddMonoidHom.completion ⋯

theorem ContinuousLinearMap.coe_completion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} (f : α →SL[σ] β) : ⇑f.completion = UniformSpace.Completion.map ⇑f

@[simp]

theorem ContinuousLinearMap.completion_apply_coe {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} (f : α →SL[σ] β) (a : α) : f.completion ↑a = ↑(f a)

noncomputable def ContinuousLinearMap.fromCompletion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) : UniformSpace.Completion α →SL[σ] β

Extension of a linear function to a linear function over the completion. This is the continuous linear version of UniformSpace.Completion.extension.

Equations

• f.fromCompletion = { toFun := (↑((↑f).toAddMonoidHom.extension ⋯)).toFun, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.toAddMonoidHom_fromCompletion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) : (↑f.fromCompletion).toAddMonoidHom = (↑f).toAddMonoidHom.extension ⋯

theorem ContinuousLinearMap.coe_fromCompletion {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) : ⇑f.fromCompletion = UniformSpace.Completion.extension ⇑f

@[simp]

theorem ContinuousLinearMap.fromCompletion_apply_coe {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) (e : α) : f.fromCompletion ↑e = f e

theorem ContinuousLinearMap.fromCompletion_unique {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) (g : UniformSpace.Completion α →SL[σ] β) (h : ∀ (e : α), f e = g ↑e) : f.fromCompletion = g

def UniformSpace.Completion.toComplL {α : Type u_1} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] : α →L[S] Completion α

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

Equations

• UniformSpace.Completion.toComplL = { toFun := (↑UniformSpace.Completion.toCompl).toFun, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem UniformSpace.Completion.coe_toComplL {α : Type u_1} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] : ⇑toComplL = coe'

@[simp]

theorem UniformSpace.Completion.toAddMonoidHom_toComplL {α : Type u_1} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] : ↑toComplL = toCompl

@[simp]

theorem ContinuousLinearMap.extend_completionToComplL {α : Type u_1} {β : Type u_2} {R : Type u_3} {S : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring S] [Module S α] [UniformContinuousConstSMul S α] [Semiring R] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R β] [UniformContinuousConstSMul R β] {σ : S →+* R} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) : f.extend UniformSpace.Completion.toComplL = f.fromCompletion