Topology on continuous_maps without a norm

Stream: maths

[Eric Wieser]

We currently don't have the topology on continuous maps when only a topology is available on the (co)domains; If we had this, we could relax a lot of typeclasses.

[Eric Wieser]

(cc @Jason KY. who had some thoughts on discord about that)

[Jason KY.]

Eric Wieser said:

(cc Jason KY. who had some thoughts on discord about that)

I'll copy what I wrote on discord here (the question is how to generalize the topology on the space of bounded linear operators between normed spaces to TVS. No promise what I've written is at all correct):

Since the space of operators is also a topological vector space it suffices to give a basis of open sets at 0. I think since this basis for the topology induced by the norm is given by $B_\epsilon(0) = \{T(B_1) \le \epsilon B_1\}$ we can do the similar for the not norm case. So since bounded is defined in general for all TVS (Yael pointed out this is the von Nuemann boundedness which we have), maybe a compatible basis at 0 is all sets of the form $\{T(U) \le V\}$ for bounded open neighborhood $U, V$ of 0 in $X$ and $Y$ resp.

[Kevin Buzzard]

If we attempt to put a topology on Hom(X,Y) when only one of X and Y has a topology, then this will almost surely be the wrong topology in the case where both X and Y have a topology (for example, one often wants to take the compact-open topology, or the weak or strong dual topology for a space of linear maps to the ground field etc etc). Is this not an issue?

[Jason KY.]

I'm not sure if I understand. My suggestion requires both X and Y to be topological vector spaces so it won't work if only one of X and Y has a topology

[Jireh Loreaux]

I think Kevin's point still stands. There's a lot of operator topologies. I guess the point is just that you want to weaken the type class assumptions on continuous_linear_map?

[Kevin Buzzard]

You can't even talk about continuous linear maps if you don't have a topology on both sides. I'm not sure I understand what is being proposed here.

[Jireh Loreaux]

Kevin there's a topology on both spaces.

[Jireh Loreaux]

The question is about the topology on the space of linear maps between them.

[Oliver Nash]

In finite dimensions, for t2 TVSs over a complete field, all linear maps are continuous and so the space of linear maps is a subset of the space of continuous maps. So if we take the compact-open topology on continuous maps we get a topology on the subset of linear maps. I expect when both domain+codomain are finite-dimensional all topologies are equal.

[Jireh Loreaux]

For TVS topologies I think that's true. But aren't we talking about the infinite dimensional case too?

[Oliver Nash]

I'm not clear on what the proposal is: I just wanted to make this one remark which I expected was known to some but not all people in this thread!

[Jason KY.]

My understanding is that we have the topology induced by the operator norm on bounded linear maps between normed spaces and Eric wants a compatible topology on bounded linear maps between TVS

[Oliver Nash]

Oh btw Mathlib will soon know the above: #13460

[Sebastien Gouezel]

Yes but you can't register this topology as an instance because otherwise, when both spaces are normes spaces, you will have two non defeq topologies on the space of continuous linear maps.

[Kevin Buzzard]

One could maybe bundle the topology in a normed vector space? I am more worried about e.g. the weak and strong topologies on the dual space.

[Jireh Loreaux]

We already have type synonyms for that.

[Kevin Buzzard]

oh nice!

[Jireh Loreaux]

docs#weak_dual

[Jireh Loreaux]

If the question is: "will the topology corresponding to the von Neumann bornology work?" then I think the answer should be yes for the reason @Jason KY. explained.

[Jireh Loreaux]

You would have to bundle the topology into normed space though.

[Jireh Loreaux]

actually, isn't there a way to do this? I mean, can't we put the topology on the linear maps, and then when we declare the metric / normed group instances we can use one of those "inducing" constructions that makes sure the generated topology agrees in a defeq way?

[Moritz Doll]

Doesn't @Anatole Dedecker have a PR for topologies on the space of linear maps?

[Eric Wieser]

Sorry all for the vagueness, I extracted this from a thread it didn't belong in but didn't clean up the first post enough to be clear!

[Eric Wieser]

Moritz Doll said:

Doesn't Anatole Dedecker have a PR for topologies on the space of linear maps?

Yes, that's

Oliver Nash said:

Oh btw Mathlib will soon know the above: #13460

But I think doesn't fully address this thread

[Kevin Buzzard]

Can you clarify what the question is? I can't really understand the first post

[Eric Wieser]

Sure, I'm asking for a

noncomputable instance continuous_linear_map.topological_space
  {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6}
  -- maybe doesn't need `field`?
  [add_comm_group E] [add_comm_group F] [field 𝕜] [field 𝕜₂] [module 𝕜 E] [module 𝕜₂ F]
  -- maybe needs `[topological_add_group E] [has_continuous_smul 𝕜 E]` etc?
  [topological_space E] [topological_space F]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂] :
topological_space (E →SL[σ₁₂] F)

which is compatible with the norm induced by docs#continuous_linear_map.to_normed_group

[Eric Wieser]

The motivation would be to be able to talk about continuous bi-linear maps without having to choose a particular norm on the codomain.

[Kevin Buzzard]

docs#ring_hom_isometric

[Kevin Buzzard]

This needs a norm, which I don't think you have?

[Sebastien Gouezel]

You have all the details about this at https://en.wikipedia.org/wiki/Topologies_on_spaces_of_linear_maps. Look in particular for the topology of "uniform convergence on bounded sets" for the definition of a topology which, in normed spaces, coincides with the norm topology on operators.

[Eric Wieser]

Kevin Buzzard said:

This needs a norm, which I don't think you have?

Ah yes, I probably meant [fact (continuous σ₁₂)].

[Anatole Dedecker]

Moritz Doll said:

Doesn't Anatole Dedecker have a PR for topologies on the space of linear maps?

Sorry for the delay, I had my exams last week. I don't have anything yet, but it is a few PR away from what we have now and I do have a precise plan for getting there. Basically, what's missing is :

• docs#uniform_convergence_on.uniform_space is a uniform group when the codomain is a uniform group
• when restricted to continuous linear maps, if all the elements of $\mathfrak{S}$ are bounded, then we get a topological vector space topology

Then the plan is to make an instance with $\mathfrak{S}$ being the full Von Neumann bornology, which coincides with the norm topology when it exists, and then fix definitional equalities as usual

[Anatole Dedecker]

Eric Wieser said:

The motivation would be to be able to talk about continuous bi-linear maps without having to choose a particular norm on the codomain.

Note however that with this topology, continuous bilinear maps $A\times B\to C$ do not correspond to continuous linear maps $\mathcal{L}(A,\mathcal{L}(B,C))$ in general

[Eric Wieser]

I'm not sure I understand your point; I assume $\times$ should be $\otimes$ in that first one? Either way, it sounds like you're in a much better position to explore this than I am; I hope the exams went well, and I'd be curious to see whatever PR comes of this even if its mostly over my head!

[Anatole Dedecker]

What I'm saying is that there are bilinear maps $b : A \times B \to C$ such that $x \mapsto b(x,\cdot)$ is continuous but $b$ is not. Actually, even having both $x\mapsto b(x,\cdot)$ and $y\mapsto b(\cdot,y)$ be continuous does not imply continuity of $b$, that's called hypocontinuity.

[Eric Wieser]

In mathlib we seem to use "continuous bilinear map" to mean only the L(A, L(B, C)) version

[Anatole Dedecker]

I've been talking about it for a loooong time, but it is finally here! #16053 (still WIP but the math content is complete) defines the strong topology associted to a family of bounded subsets of the domain, declares the special case of considering all bounded subsetes as a topological_space instance on continuous linear maps, and redefines docs#continuous_linear_map.to_seminormed_add_comm_group using forgetful inheritance so that everything is completely transparent. It is sitting on a few preliminary PRs, but as I said the math content is here.

[Anatole Dedecker]

I was scared at the last minute because most people (including Bourbaki) do this only for ℝ or ℂ, and the naive proof to prove that it indeed gives the same topology as the operator norm use the "sup of the unit ball" definition of the operator norm, but I think our definition isn't equivalent to this in general (although it is for ℝ or ℂ), or at least we don't seem to have it and it is non trivial, because we can't just divide a vector by its norm. Thankfully I managed to find a way around it.

[Anatole Dedecker]

Kevin Buzzard said:

This needs a norm, which I don't think you have?

You have a norm on the field, which is what you need here

[Jireh Loreaux]

For future reference, we should have (not yet) a sup over the unit ball lemma which holds over a docs#densely_normed_field but of course if you managed to avoid it, that's even better.

[Anatole Dedecker]

For some reason this change seems to confuse Lean in some specific places (you can look at the diff for analysis/convolution and analysis/normed_space/bounded_linear_maps in the PR), but just adding a little bit more information fixes it. I don't think it is a big deal since it only happened twice in the whole library, but if someone has an idea of what could be causing that it would be nice

[Notification Bot]

40 messages were moved from this topic to #maths > generalizing deriv to TVS by Yury G. Kudryashov.