Eval as a linear map from CLM to codomain

Stream: Is there code for X?

[Moritz Doll]

Does the following definition exist somewhere? I would be shocked if not, but I could not find it

variable (𝕜 E : Type*) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]

@[simps]
def evalLM (a : E) : (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜 where
  toFun v := v a
  map_add' := fun _ _ ↦ rfl
  map_smul' := fun _ _ ↦ rfl

[Jireh Loreaux]

How does docs#ContinuousLinearMap.apply' work for you?

[Jireh Loreaux]

If the hypotheses of that are too strong, then I'm betting we don't have the version you want.

[Moritz Doll]

I don't want to assume that E is a normed space

[Jireh Loreaux]

We also have docs#LinearMap.applyₗ'

[Jireh Loreaux]

You could compose that with a forgetful morphism.

[Moritz Doll]

Yes, that sounds very reasonable. The context is that I want to prove continuity of the evaluation for the pointwise convergence topology:

theorem PointwiseConvergenceCLM.eval_continuous (a : E) :
    Continuous (fun (v : E →Lₛ[𝕜] 𝕜) ↦ v a) := by sorry

and the proof uses that the map is linear (to reduce everything to 0 nhds). Also I want to bundle this definition (and the corresponding one for the weak dual)

[Moritz Doll]

Ah crap, I think I have to define my own docs#ContinuousLinearMap.coeLM variant

[Antoine Chambert-Loir]

Yes, that would be nice to refactor this stuff so that they hold for arbitrary topological vector spaces.