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} {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)

noncomputable def ContinuousLinearMap.fromCompletion {α : 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₂} [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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* 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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* 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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* 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} {R₂ : Type u_4} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R₁] [Module R₁ α] [UniformContinuousConstSMul R₁ α] [Semiring R₂] [UniformSpace β] [AddCommGroup β] [IsUniformAddGroup β] [Module R₂ β] [UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂} [T0Space β] [CompleteSpace β] (f : α →SL[σ] β) (g : UniformSpace.Completion α →SL[σ] β) (h : ∀ (e : α), f e = g ↑e) : f.fromCompletion = g