Completion.map of linear map is linear

Stream: Is there code for X?

[Gregory Wickham]

Is there a way to easily construct a linear function from (Completion A) to (Completion A) from a linear function from A to A? UniformSpace.Completion.map doesn't preserve linearity.

Here is an abstracted minimum example of what I'm trying to do:

import Mathlib.Algebra.Module.LinearMap.Defs
import Mathlib.Data.Complex.Basic
import Mathlib.Topology.UniformSpace.Completion
-- Setup
variable {A : Type*} [AddCommMonoid A] [Module ℂ A] [UniformSpace A]
def H := UniformSpace.Completion (A)
instance : AddCommMonoid (H (A := A)) := sorry
instance : Module ℂ (H (A := A)) := sorry
def Tlin : A →ₗ[ℂ] A := sorry
-- Questions
noncomputable
def T : (H (A := A)) →ₗ[ℂ] (H (A := A)) where
  toFun := UniformSpace.Completion.map (Tlin) (α := A) (β := A)
  map_add' := sorry -- is there a way to conicesly prove this
  map_smul' := sorry -- and this?

noncomputable
def T' : (H (A := A)) →ₗ[ℂ] (H (A := A)) := sorry -- Is there something I could put here?

In my actual project, I am doing a Completion on an inner product space to get a Hilbert space, so if there's a way to use that fact to get a linear extension to the completion by respecting the existing vector space structure and linear map/homomorphism, that would probably also be sufficient.

[Kenny Lau]

you need the function to be continuous right

[Kenny Lau]

I don't know where to find it so I'll let other people answer

[Aaron Liu]

you need to have some way of relating the module structure and the topology

[Moritz Doll]

It is not quite what you are asking for but I assume you want docs#ContinuousLinearMap.extend and you take the map that maps A to the completion. Can you please say what is exactly your setup? Is the completion known (usually it is L^2 or something similar), what is the operator?

[Moritz Doll]

There is also #31074 which is more how mathematicians would state that result

[Kenny Lau]

I think it would make sense to extend the Completion API using the lemma you cited