Map vector space to its double dual

Stream: maths

[David Loeffler]

If V is a topological vector space over a normed field 𝕜, how can I construct the canonical map from V to its double dual? That is, I'm looking for a construction of a map R : V →L[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜) such that R v e = e v for all (v : V) (e : V →L[𝕜] 𝕜).

If we forget the topologies and just ask for a plain linear map, this is docs#linear_map.applyₗ. If we put a normed-space structure (not just a topological-vector-space structure) on V, it's docs#continuous_linear_map.apply; but I don't want to force a choice of norm on V. It looks like mathlib does know how to topologize V →L[𝕜] 𝕜for any TVS, so the question makes sense, but I can't seem to find an answer to it in the library.

[Adam Topaz]

do we have something like docs#weak_dual.apply ?

[Adam Topaz]

well, it should be quite easy using docs#weak_dual.eval_continuous

[Adam Topaz]

Are you using the weak topology?

[Adam Topaz]

docs#top_dual_pairing also seems useful

[Eric Wieser]

It looks like mathlib does know how to topologize V →L[𝕜] 𝕜 for any TVS

I seem to remember that @Anatole Dedecker had made quite a lot of progress on this, but it either didn't make it to a PR, or the PR was diverted into a refactor elsewhere and then forgotten

[Eric Wieser]

(referred to here)

[Eric Wieser]

Aha, this is the thread I'm thinking of

[Anatole Dedecker]

I think we don't have the construction but it should be very easy, the key lemma being docs#uniform_on_fun.uniform_continuous_eval_of_mem. At some point it would be nice to go systematically through the basic operator norm files and generalize as much as possible, but this should probably wait for the port

[Kyle Miller]

David Loeffler said:

If we forget the topologies and just ask for a plain linear map, this is docs#linear_map.applyₗ.

Just so you know (or in case it's useful to anyone who finds this thread later), the pure algebra version is wrapped up as docs#module.dual.eval

[Anatole Dedecker]

Anatole Dedecker said:

I think we don't have the construction but it should be very easy, the key lemma being docs#uniform_on_fun.uniform_continuous_eval_of_mem. At some point it would be nice to go systematically through the basic operator norm files and generalize as much as possible, but this should probably wait for the port

Actually that's not quite right. What can easily be proved is that each evaluation is continuous (i.e we can get V →ₗ[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜)), but it is not clear at all that the last continuity is true in general (and Bourbaki seems to indicate otherwise, but I will have another look to be sure). Of course it is true for normed space and we could give topological conditions to make it work without invoking extra data (typically "bornological" or "barreled", but unfortunately we don't have these in mathlib yet).
Just to be clear, let me mention that this is all way easier if you work with weak topologies, but since you want to generalize the normed case I figured this is probably not what you want.

[David Loeffler]

Ah, so the reason I couldn't find the result I wanted in mathlib is because it's false, which is a pretty good reason. Thanks for enlightening me on that!

(Ironically, the case I want this for is actually when V is finite-dimensional. In this case the mathematical issues are all trivial, but the problem is getting mathlib to recognise that V →L[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜) and V →ₗ[𝕜] ((V →ₗ[𝕜] 𝕜) →ₗ[𝕜] 𝕜) are the same thing.)

[Jireh Loreaux]

Surely we have an equiv for that, right?

[Jireh Loreaux]

docs#linear_map.to_continuous_linear_map

[Jireh Loreaux]

You can probably use that to beef it up to the version needed here (I guess it's not super trivial though).

[David Loeffler]

Jireh Loreaux said:

You can probably use that to beef it up to the version needed here (I guess it's not super trivial though).

Unfortunately, it seems it is not only not super-trivial, but possibly even strictly sub-trivial. Using docs#linear_map.to_continuous_linear_map you can get a linear equivalence between V →L[𝕜] 𝕜 and V →ₗ[𝕜] 𝕜. But you can't get a continuous linear equivalence; indeed the latter space doesn't have a topology at all, as far as mathlib is concerned. So I don't see how to use the same trick a second time to get an isomorphism between the algebraic and topological double duals.

[Jireh Loreaux]

I don't think you were interpreting what I said the same way I intended it. You can get a linear equivalence between V →L[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜) and V →ₗ[𝕜] ((V →ₗ[𝕜] 𝕜) →ₗ[𝕜] 𝕜) by constructing the equivalence piece by piece using docs#linear_map.to_continuous_linear_map to upgrade with continuity, and using docs#linear_equiv.arrow_congr to paste things together. Like this:

import topology.algebra.module.finite_dimension
import topology.algebra.module.strong_topology

variables {𝕜 : Type*} [nontrivially_normed_field 𝕜] [complete_space 𝕜]
variables {V : Type*} [add_comm_group V] [module 𝕜 V] [topological_space V]
  [topological_add_group V] [has_continuous_smul 𝕜 V] [finite_dimensional 𝕜 V] [t2_space V]

example : (V →ₗ[𝕜] ((V →ₗ[𝕜] 𝕜) →ₗ[𝕜] 𝕜)) ≃ₗ[𝕜] V →L[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜) :=
((linear_equiv.refl 𝕜 V).arrow_congr $
  ((linear_map.to_continuous_linear_map : (V →ₗ[𝕜] 𝕜) ≃ₗ[𝕜] (V →L[𝕜] 𝕜)).arrow_congr
  (linear_equiv.refl 𝕜 𝕜)).trans
  linear_map.to_continuous_linear_map).trans
  linear_map.to_continuous_linear_map

In a calc-style block, this looks like:

(V →ₗ[𝕜] ((V →ₗ[𝕜] 𝕜) →ₗ[𝕜] 𝕜)) ≃ₗ[𝕜] (V →ₗ[𝕜] ((V →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜))
...                             ≃ₗ[𝕜] (V →ₗ[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜))
...                             ≃ₗ[𝕜] (V →L[𝕜] ((V →L[𝕜] 𝕜) →L[𝕜] 𝕜))

[David Loeffler]

Great, thank you very much for your help! I hadn't come across linear_map.arrow_congr before, I'll have to remember that one.

For my application, I eventually realised I could get away with something a little weaker: I only need an element of V →ₗ[𝕜] ((V →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) (with two →ₗs and one →L) and this can be constructed as (top_dual_pairing 𝕜 V).flip.