Strong topology on linear maps

Stream: maths

[Anatole Dedecker]

Now that bornologies have landed in mathlib, I'd like to define the topology of $\mathfrak{S}$-convergence on spaces of linear maps between two TVSs $E$ and $F$, where $\mathfrak{S}$ is a set of Von Neumann bounded sets of E, but I'd like to discuss a few design decisions before actually starting to work on that :

• do we want to have type aliases for each possible $\mathfrak{S}$ ? for each bornology $\mathfrak{S}$ (since taking the generated bornology doesn't change the topology) ? Or is the von Neumann bornology canonical enough that we can put it as the default topology on E ->L[k] F ?
• If we put a topology on E ->L[k] F, we'll have to make sure that the instance coming from the normed_space structure is defeq to the more general one. Would it work to separate the PRs by first localizing the new instance, and then making it global when everything is fixed ?
• Is there any point to first define the topology of $\mathfrak{S}$-convergence on $E -> F$ like Bourbaki does (which might mean a new type synonym again...). For example we could redefine compact-open topology from it ?
• What do you think would be easier : giving a neighborhood basis (this is what mathlib does for the compact-open topology), or define it as the initial topology associated with restrictions to set of $\mathfrak{S}$, whith the topology of uniform convergence on the codomain (this is what Bourbaki does)
• If we don't redefine the compact open topology, nor the weak dual, or anything which could be a special case of this general setup, do we want a topology_of_convergence S Prop-valued typeclass asserting that the topology on a type is (provably) equal to the topology of S-convergence ?

@Jireh Loreaux @Moritz Doll You might have started to work on / think about this, so I'd like to hear your thoughts in particular. I've also seen @Heather Macbeth @Patrick Massot might need some of this in the sphere-version project, am I right ?

Anyway, thanks in advance !

[Jireh Loreaux]

To be honest, I have not done much here, and have not started on any of the above. There is #12078 (which is open and ready for anyone reading this; I think Moritz already had a look) that puts a bornology instance on metric spaces. I will probably not contribute much to bornology unless anyone has something specific they want me to do because I have plenty of other things to work on.

[Moritz Doll]

I think we should define bornological spaces first, @Yaël Dillies wanted to define bornivorous sets, which is needed for that. I thought a bit about the question whether to use type synonyms for all kinds operator topologies and I am tending towards no. Maybe @Sebastien Gouezel has some ideas about that (seems quite related the issues with polish spaces).

[Moritz Doll]

@4 I think the initial topology might be less code (but more weird code IMO). You can see the difference between docs#weak_bilin and docs#seminorm_family.module_filter_basis the weirdness comes when you try to calculate the filter basis - for weak_bilin it is in #12623 (as you can see nobody wants to review that :grinning: ). In the end it should not matter that much as you have the same results. I found writing the module filter basis way easier as all steps are straightforward.

[Yaël Dillies]

I'll try to get bornivores out this weekend!

[Anatole Dedecker]

Could you expand on why we need bornological spaces for this ? I see why we need bornologies, but not bornological spaces. Sorry, I'm discovering the maths at the same time, so I don't see the full picture yet :sweat_smile:

[Anatole Dedecker]

But anyway I can wait / help if we need to setup more things first

[Anatole Dedecker]

Moritz Doll said:

@4 I think the initial topology might be less code (but more weird code IMO). You can see the difference between docs#weak_bilin and docs#seminorm_family.module_filter_basis the weirdness comes when you try to calculate the filter basis - for weak_bilin it is in #12623 (as you can see nobody wants to review that :grinning: ). In the end it should not matter that much as you have the same results. I found writing the module filter basis way easier as all steps are straightforward.

Yeah I know, sometimes filter bases are just painful to use. I've been keeping #12118 "WIP" for waaaay too long because I need to refactor some things about filter bases first

[Moritz Doll]

Anatole Dedecker said:

Could you expand on why we need bornological spaces for this ? I see why we need bornologies, but not bornological spaces. Sorry, I'm discovering the maths at the same time, so I don't see the full picture yet :sweat_smile:

I might have been wrong here, I was under the impression that bornological spaces were needed for some results because they connect the bornology with the TVS structure. I don't know that much about this extremely abstract functional analysis and especially not about bornologies, I also use lean as a way to learn it.

[Sebastien Gouezel]

I would use type synonyms for the three or so standard topologies on operator spaces. More precisely, I would put the standard one (that corresponds to the norm topology) on E ->L[k] F, and use type synonyms for respectively the pointwise convergence topology, and the pointwise weak convergence topology.

[Moritz Doll]

Does the topology on E ->L[k] F have to be defeq to the topology induced by the operator norm? Right now the normed space structure on E ->L[k] F is defined using normed_space.of_core. If have a topology (or probably a uniformity) on E ->L[k] F in a more general case then we cannot use of_core but have to provide our proof that the topologies (uniformities) coincide.

[Moritz Doll]

Also it seems that the construction in Bourbaki GT.X is more general than what is in docs#compact_convergence so we should get a generalization of docs#continuous_map.compact_open_eq_compact_convergence for the relationship with the compact open topology.

[Moritz Doll]

The weak topologies should also be a special case, but I would not worry about that for now.

[Anatole Dedecker]

Moritz Doll said:

Also it seems that the construction in Bourbaki GT.X is more general than what is in docs#compact_convergence so we should get a generalization of docs#continuous_map.compact_open_eq_compact_convergence for the relationship with the compact open topology.

Oh you made me realize that we can't define the compact-open topology this way, because compact-open topology doesn't involve any uniform structure :face_palm:

[Anatole Dedecker]

Do we already have a type synonym for functions to an uniform space with the topology of uniform convergence (on the whole domain) ?

[Anatole Dedecker]

Like, all the functions, not only the continuous ones

[Yury G. Kudryashov]

I have some questions about strong topology on linear maps.

1. Am I right that docs#ContinuousMap.compactConvergenceTopology is the same as docs#UniformOnFun.topologicalSpace for 𝔖 = {K | IsCompact K}?

2. Am I right that https://en.wikipedia.org/wiki/Strong_operator_topology is equal to each of:

   • docs#ContinuousLinearMap.strongTopology with 𝔖 = Set.range singleton
   • docs#ContinuousLinearMap.strongTopology with 𝔖 = {s | Set.Finite s}
   • the topology induced from functions?
     Should we mention this in the module docstring?

3. Do we ever need docs#ContinuousLinearMap.strongTopology for 𝔖 not being the set of bounded sets for some bornology? If no, what do you think about de-generalizing the definition?

4. Do we need any extra assumptions to conclude that evaluation at a point is continuous as a function of two arguments? The domain is locally bounded (a.k.a. normable)? Or is it true with weaker assumptions?
5. What assumptions do we need to conclude that ContinuousLinearEquiv.symm is continuous in the topology induced by projection to ContinuousLinearMaps? If we need extra assumptions, then what is the right topology when we don't have them: the one induced by projection to ContinuousLinearMap, or the one induced by embedding into the product (like we do with Units)? I would choose the latter for consistency but possibly there are reasons not to.
6. What assumptions do we need to prove that docs#ContinuousLinearMap.flip is well-defined and is a continuous linear map?

[Anatole Dedecker]

Oh that’s a lot of questions, give me some time 😅

[Anatole Dedecker]

1. Yes that is true, and I think we should get rid of docs#ContinuousMap.compactConvergenceTopology for this reason. I should have opened an issue about it some time ago, sorry for not doing it. I'll do that this afternoon unless you beat me to it.

[Anatole Dedecker]

2. That is also true. Here I must admit that the naming scheme is badly chosen, for the simple reason that I only learned about this terminology after doing all of this work. Moreover, I had in mind the case where the target space is the base field, where this gives you the "strong dual", but if you are talking about operators then this becomes the "strong operator topology", which is a bit stupid in my opinion. So I agree we should at least add a comment about that, and maybe even better choose another name.

[Anatole Dedecker]

3. Well that is almost true, except that (as we talked about a few times already) we don't have the right notion of bornology. For clarity, I'll use "bornology" for docs#Bornology and "ideal" for "Order.Ideal" on the lattice of sets. That means that a bornology is precisely an ideal that contains the singletons.
   The result that is true, is that when you replace 𝔖 by the generated ideal, you do not change the topology of uniform convergence (this is in a rotten Mathlib3 PR of mine, but I had to work around bornology by hand so it didn't feel satisfying enouh). But if you take the generated bornology then you can clearly change the topology because having all singletons in your set forces the resulting topology to be T2 (docs#UniformOnFun.t2Space_of_covering)

[Anatole Dedecker]

I maintain my opinion that we shouldn't require bornologies to contain singletons and that they should be exactly ideals of sets (this is what Bourbaki does), because it's super easy to add some typeclass saying "singletons are bounded" to make everything works transparently. But if people really disagree about that then we'll have to make more API for ideals of sets. Once either of these is done, I would be in favor of requiring 𝔖 to be an ideal and adding a few lemmas about what happens when 𝔖 is generated by a convenient family of sets.

[Anatole Dedecker]

I don't know the answers to 4, 5 and 6, I will think about it this afternoon. But I really want to emphasize that a lot of things definitely are not true in general. I know that in general:

• continuous bilinear maps are NOT the same as our curried bilinear maps
• uncurried composition is NOT continuous. I think curried composition isn't either, but I have to think about it

[Anatole Dedecker]

I'm also pretty sure that flipping the arguments isn't well defined in general, but one case I care about where it is true is when one of the spaces is finite dimensional. This means that vector valued distributions have a well defined "Fréchet derivative distribution" as long as the domain is finite dimensional, which means that we don't have to choose a basis and talk about partial derivatives.

[Anatole Dedecker]

On and I should mention that a lot more of these things are (obviously) true when 𝔖 is the bornology of finite sets.

[Anatole Dedecker]

I think we shouldn't spend too much time searching for generalizations outside of the normed setting if we don't have a use case in mind (but maybe you do, in which case I'd be interested to hear about it!), because as I said a lot of things just aren't true in greater generality, and the useful cases are quite heavily studied.
So the way I envision it is that these generalization happen when people need them, and maybe if we have multiple sets of hypotheses for a same result then we can try to find common ancesters

[Anatole Dedecker]

Oh and since we're talking about this, could I get a look on !3#19128 ? :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

Thanks a lot for the answers! I merged !3#19128. As for applications, the original reason was to find out if we can weaken assumptions in the vector bundle hom construction.

[Yury G. Kudryashov]

It seems that the answer is "no" but we may want introduce a Prop-valued typeclass [Seminormable _] (or a Type _-valued typeclass [NormableAddCommGroup _] and use it instead of [NormedAddCommGroup _] here and there. Then constructions won't rely on a specific choice of norm, so we don't have to choose a norm, e.g., to speak about finite-dimensional matrices.

[Yury G. Kudryashov]

Anatole Dedecker said:

Oh and since we're talking about this, could I get a look on !3#19128 ? :grinning_face_with_smiling_eyes:

Now it's on the #outofsync list.

[Eric Wieser]

A downside of these seminormable classes is that we need one for every normed class we currently have

[Eric Wieser]

We'd need at least NormableAddGroup, NormableModule, NormableRing, NormableAlgebra

[Eric Wieser]

Maybe that's acceptable to unblock things on matrix analysis

[Yaël Dillies]

Why can't we make it a mixin?

[Eric Wieser]

In my above message I'm assuming they are mixins already

[Eric Wieser]

If they're not mixins it becomes much worse