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 G to H to a continuous semilinear map from Completion G to Completion H.

noncomputable def ContinuousLinearMap.completion {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* 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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂} (f : α →SL[σ] β) : (↑f.completion).toAddMonoidHom = (↑f).toAddMonoidHom.completion ⋯

theorem ContinuousLinearMap.coe_completion {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* 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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂} (f : α →SL[σ] β) (a : α) : f.completion ↑a = ↑(f a)