Making a continuous bilinear map

Stream: Is there code for X?

[David Loeffler]

Say A, B, C are vector spaces over 𝕜 and I have a bilinear map A × B → C, represented as a map f: A →l[𝕜] B →l[𝕜] C as usual. If A, B, C are normed spaces, and I have a proof that f is continuous as a map A × B → C, is there a simple way of promoting f to a continuous bilinear form, represented an element of A →L[𝕜] B →L[𝕜] C?

There is docs#LinearMap.mkContinuous₂, but that requires an explicit bound on the operator norm.

[David Loeffler]

(sorry, for some reason I can't get that to linkify)

[Michael Stoll]

The linkifier doesn't like subscripts etc.

[Michael Stoll]

(You can use the [xxx](url) syntax to emulate what it should do.)

[Michael Stoll]

docs#LinearMap.mkContinuous₂

[David Loeffler]

NB, in case this gets missed: the question is still unaswered (the upvote was for help fixing formatting in the question)

[Yaël Dillies]

Just to make sure, is continuity in A × B → C the same as continuity in A → B → C when talking about linear maps? In general, this is not the case.

[Eric Wieser]

Is this related to the question of continuous bilinear maps over a TVS? Did that every result in a PR?

[Anatole Dedecker]

It’s the same for normed spaces. It definitely isn’t in general

[Anatole Dedecker]

Note that docs#ContinuousMultilinearMap uses the correct definition (no currying trick), but I’m not sure it would be practical to use that API here

[Jireh Loreaux]

Anatole, they're the same for bornological spaces too, right?

[David Loeffler]

Anatole Dedecker said:

It’s the same for normed spaces. It definitely isn’t in general

Is there a proof of this easily accessible in the library?

[David Loeffler]

I guess I'll have to convert my f into a MultlinearMap, and then use the n = 2 case of docs#MultilinearMap.exists_bound_of_continuous. I'd hoped it would be less painful than this.

[David Loeffler]

The context here is trying to define Banach modules over a Banach algebra, without assuming that the scalar multiplication necessarily satifies $\|a * v\| \le \|a \| \cdot \|v\|$ – I wanted to assume [ContinuousSMul A V], not [BoundedSMul A V]. The problem is that in the literature many authors (e.g. Kevin in his previous life...) are very insistent that a Banach space should be a space with an equivalence class of norms (but we shouldn't single out one specific choice of the norm as part of the data).

[Anatole Dedecker]

Topological equivalence or Lipschitz equivalence? EDIT: if I understand correctly the modules you care about also happen to be normed spaces over the base field, so it should still be the same thing. If I'm right, this means that the equivalence class of norms is entirely determined by the topology, so it would make sense to use a Normable typeclass similar to docs#Metrizable, right?

[Anatole Dedecker]

I definitely think we want to keep the choice of norm in the usual setup, but it shouldn't be too hard to make an intermediate structure if needed.

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

Regarding normed modules in general, I think we should have some discussion about how we want to setup everything, especially to make sure that everything works well with the current setup. In particular (this is a bit orthogonal to your original question) I would like some opinions on the plan I made some time ago to make docs#BoundedSMul more natural (imho).

[David Loeffler]

David Loeffler said:

The problem is that in the literature many authors (e.g. Kevin in his previous life...) are very insistent that a Banach space should be a space with an equivalence class of norms (but we shouldn't single out one specific choice of the norm as part of the data).

Actually I checked and my memory seems to have been playing tricks on me – both Kevin's /Eigenvarieties/ paper and Bosch–Güntzer–Remmert require a normed module over a normed algebra to have a specific norm satisfing $\|a \bullet v\| \le \|a\| \cdot \|v\|$. So this thread was a wild-goose chase.