TVS and NormedSpace on Finsupp, DFinsupp, DirectSum, ..

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere? Can we take the same norm and topology that we use on finite product spaces?

[Kevin Buzzard]

"the same" -- no because it's not finite. It's not really clear to me what you mean. You can put topologies on arbitrary products but these are coproducts.

[Kevin Buzzard]

I guess that for norms the answer is "probably yes" but I would not immediately like to punt on the "correct" topology to put on an uncountable infinite sum of topological abelian groups.

[Eric Wieser]

At least for the norm, I'm suggesting we generalize the ‖f‖₊ = Finset.univ.sup fun i => ‖f i‖₊ which we have to ‖f‖₊ = f.support.sup fun i => ‖f i‖₊

[Kevin Buzzard]

Yes, for norms this doesn't sound crazy. For topologies I wonder whether some kind of universal topology (e.g. the finest one making all the inclusions continuous) would coincide with the topology induced by the norm (I'm thinking about additive groups here).

[Eric Wieser]

The follow up question would be whether we want / need a continuous version of Basis

[Kevin Buzzard]

Again I don't immediately know what you mean.

[Kevin Buzzard]

The basis for an arbitrary direct sum of based vector spaces is just the disjoint union of the bases.

[Eric Wieser]

For b : Basis _ _ V, Continuous b.repr and Continuous b.repr.symm (which are currently unstateable) are obviously true for Module.Finite _ V, but I have no idea if they're true in the infinite case

[Kevin Buzzard]

They're not true in general for Module.Finite _ V unless M has the product topology (which is not true in general).

[Kevin Buzzard]

For example $\mathbb{Q}(\sqrt{2})\subseteq\R$ can be given the subspace topology, as can $\mathbb{Q}$, and then it's not true at all for the basis $\{1,\sqrt{2}\}$ even though it's a perfectly good topological module for the topological ring $\mathbb{Q}$.

[Kevin Buzzard]

In general there are many topologies which you can put on a module over a topological ring which make it into a topological module. The docs#moduleTopology is a special topology for which your statements are true in the finite case; this is something I proved recently and PRed to mathlib.

[Eric Wieser]

I meant in the generality of normed spaces, for which I think it's true?

[Eric Wieser]

(via docs#LinearMap.toContinuousLinearMap)

[Kevin Buzzard]

Why isn't my example a counterexample in the normed space case as well?

[Kevin Buzzard]

Eric Wieser said:

(via docs#LinearMap.toContinuousLinearMap)

[CompleteSpace 𝕜]

[Eric Wieser]

Yep, sorry for being vague

[Kevin Buzzard]

My $\mathbb{Q}$ example is of course not complete, this is exactly why I can make screwy counterexamples.

[Eric Wieser]

The fact you're a professional mathematician also makes you very qualified to make screwy counterexamples

[Kevin Buzzard]

The thing about infinite coproducts is that in contrast to the finite coproduct case, an infinite coproduct of (positive-dimensional) complete normed spaces is no longer complete, and if you have a complete k hypothesis then you are likely to be interested in completeness. The theory of Hilbert spaces and $\ell^p$ spaces etc are what you start to get if you take coproducts, put some norm on them, and then complete. Again in stark contrast to the finite coproduct case, the completion depends very much on the exact norm you choose. All norms on a finite-dimensional vector space over a complete field are equivalent, i.e. induce the same topology. For infinite coproducts this is no longer the case; your precise definitions matter and the completion then depends on basically how quickly elements can tend to zero.

[Kevin Buzzard]

docs#IsModuleTopology.continuous_of_linearMap is a second proof that a linear map is automatically continuous, but instead of the hypothesis that k is a complete field, we assume that the source has the module topology (and the base ring can be an arbitrary topological ring). Here there are no finiteness hypotheses at all.

[Kevin Buzzard]

For the continuous basis question, even over a complete field such as the reals it's possible to write down two infinite-dimensional normed vector spaces which are isomorphic as abstract vector spaces but not as topological vector spaces or normed vector spaces, so in this case there is no possible topology you can put on ι →₀ R which will make Basis.repr continuous for both choices (they can both have the same ι).

[Aaron Liu]

Kevin Buzzard said:

so in this case there is no possible topology you can put on ι →₀ R which will make Basis.repr continuous for both choices (they can both have the same ι).

I followed all your reasoning until this part

[Kevin Buzzard]

I can think of two vector spaces $V$ and $W$ with norms which are isomorphic as abstract vector spaces but not as topological vector spaces or normed vector spaces. Because they're isomorphic as abstract vector spaces I can find bases for $V$ and $W$ which are both indexed by the same indexing type ι. This gives me two isomorphisms of abstract real vector spaces V ≃ₗ[ℝ] ι →₀ ℝ and W ≃ₗ[ℝ] ι →₀ ℝ. If one could magically put a norm or topology on the RHS making both of these isomorphisms, then we could conclude that $V$ and $W$ were isomorphic as normed or topological vector spaces, but they're not.

To be honest I can only do this for $p$-adic vector spaces, but the real story is strictly worse than the $p$-adic story so when I say "I can think of..." what I really means is "according to my mathematician's instinct...". I'm guessing that $\ell^1(\N)$ and $\ell^\infty(\N)$ work.

[Aaron Liu]

Oh you want both maps in the isomorphism to be continuous

[Kevin Buzzard]

No, Eric does. I'm arguing that there are problems with this.

[Kevin Buzzard]

According to ChatGPT $\ell^1(\N)$ and $\ell^\infty(\N)$ have dimension $2^{\aleph_0}$ so they're abstractly isomorphic as vector spaces, but apparently one is separable and the other isn't so they're not isomorphic as topological vector spaces. Note: this argument sounds plausible to me but I've forgotten enough of my undergrad functional analysis to be 100% confident about this.

[Yaël Dillies]

Both claims are correct, yes

[Aaron Liu]

I remember reading something with ""infinite dimensional polytopes"" forum post and this distinction came up and the people were very confused because the norms are equivalent in the finite dimensional case but different in the infinite dimensional case

[Eric Wieser]

Kevin Buzzard said:

No, Eric does. I'm arguing that there are problems with this.

Well, what I actually want is a way of saying "this Basis is well-behaved topologically", and wanted to know if this was a reasonable thing to have to write or if all bases ended up behaving well

[Yaël Dillies]

They definitely do not all behave well, as the $\mathbb Q(\sqrt 2)$ example shows.

[Kevin Buzzard]

I suspect that for complete normed spaces, in the infinite-dimensional case in some sense "no basis behaves well". This is why people talk about different concepts other than abstract algebraic bases in the infinite case, for example a "Hilbert space basis" (which is not a basis). See for example https://en.wikipedia.org/wiki/Orthonormal_basis (again, an orthonormal basis is not a basis in the infinite-dimensional case). In short, instead of trying to use the abstract vector space basis, you modify the concept of basis to allow infinite linear combinations.

[Michał Mrugała]

Aaron Liu said:

I remember reading something with ""infinite dimensional polytopes"" forum post and this distinction came up and the people were very confused because the norms are equivalent in the finite dimensional case but different in the infinite dimensional case

Off topic slightly: There is a third equivalent condition for this, which is that the unit ball is only compact in finite dimensional spaces. My intuition is that there should be a nice way to think about this being the same thing as having all equivalent norms.

[Aaron Liu]

In which topology?

[Michał Mrugała]

In any topology coming from a norm.

[Anatole Dedecker]

Michał Mrugała said:

Aaron Liu said:

I remember reading something with ""infinite dimensional polytopes"" forum post and this distinction came up and the people were very confused because the norms are equivalent in the finite dimensional case but different in the infinite dimensional case

Off topic slightly: There is a third equivalent condition for this, which is that the unit ball is only compact in finite dimensional spaces. My intuition is that there should be a nice way to think about this being the same thing as having all equivalent norms.

People often use compactness to prove the equivalence of norms, but this is not "the right way": the theorem actually holds for non-locally-compact fields, where no unit ball is compact even in dimension one.

[Michał Mrugała]

Yes sorry, I'm only talking about real or complex normed vector spaces above. Do you have any good examples of non-locally compact fields that mathematicians work with?

[Kevin Buzzard]

$\mathbb{C}_p$.

[Kevin Buzzard]

It took Tate to figure out how to do a basic theory of finite-dimensional manifolds over that field.

[Anatole Dedecker]

I don't know how to start answering to this thread, so instead let me mention one funny fact. First, real coproducts almost never exist in the setting of Banach spaces (see https://math.stackexchange.com/questions/813427/is-there-a-concept-of-a-free-hilbert-space-on-a-set/813727#813727).

But, in some sense, the $\ell^1$ sum of Banach spaces and the $\ell^\infty$ product of Banach space behave as coproduct and product, in the following sense: given $(X_i)_i$ and $Y$ Banach spaces, one has isometric isomorphisms

$$\mathrm{Hom}\left(Y, {\prod_i}^{\ell^\infty} X_i\right) \simeq {\prod_i}^{\ell^\infty} \mathrm{Hom}(Y, X_i) \\ \mathrm{Hom}\left({\bigoplus_i}^{\ell^1} X_i, Y\right) \simeq {\prod_i}^{\ell^\infty} \mathrm{Hom}(X_i, Y)$$

I don't quite know how to turn this into a proper categorical thing (are enriched categories the right thing here ? Because this is definitely considering the hom sets as Banach spaces).

But one way to do so is to arbitrarily impose that you only take morphisms of norm less than one, and then they become proper coproducts and products (but I don't like this solution)

[Anatole Dedecker]

All of this is to say: if we ever want to put a topology on Finsupp, I think the more natural choice is the l^1 one. But really I think we should just use docs#WithLp.

[Eric Wieser]

As in, you're suggesting we create a NormedSpace (WithLp _ (Finsupp _ _)) instance (which is a good idea in my mind), and don't bother thinking about the other one?

[Anatole Dedecker]

Which other one ? There are a bunch of context where we want to consider different norms on Finsupp (I should have started by this), so doing all the l^p ones is a good start.

[Anatole Dedecker]

Yes, I should have been clearer about this : we do not want any norm on Finsupp, because we will keep putting norms on it to gt different completions. E.g any choice of unitary representation of a discrete group G will give a norm on MonoidAlgebra ℂ G whose completion will be some $C^\ast$ algbra.

[Eric Wieser]

My thinking was that we should put the same norm on un-synonymed Finsupp as we do on Pi types; in both cases it sounds like we can't make everyone happy (a lot of new users want the L2 norm by default), but doing so feels somewhat consistent

[Kevin Buzzard]

I'm a bit confused about how you put a norm on Pi types in the infinite case. What's the norm of $(1,2,3,4,5,6,\ldots)$ in $\prod_{n=1}^\infty\R$?

[Eric Wieser]

In mathlib we don't define the norm in that case

[Kevin Buzzard]

If we don't define it for infinite products then maybe we shouldn't define it for infinite coproducts. But I agree that there's a natural definition. The problem is that in the finite case all the variants of the natural definition (e.g. max $|x_i|$, sum of $|x_i|$) are all equivalent and hence induce the same topology. In the infinite case this is not true.

[Jireh Loreaux]

I agree that we should not have a norm or topology on Finsupp or any such variant. There simply is no canonical one for the reasons mentioned above.