post composition for continuous bilinear maps

Stream: Is there code for X?

[Jireh Loreaux]

Suppose E, F, G and H are normed spaces over a nontrivially normed field 𝕜. If I have a continous bilinear map f₁ : E →L[𝕜] F →L[𝕜] G and a continuous linear map f₂ : G →L[𝕜] H, I would like to compose them to obtain a continuous bilinear map E →L[𝕜] F →L[𝕜] H. Outside of normed spaces, I think this is not possible, but in a normed space, we can curry the bilinear map to a multilinear map (E × F) [×2]→L[𝕜] G (I'm fudging the notation here), then compose, and then uncurry.

But presumably I shouldn't actually do this with docs#ContinuousLinearMap.uncurryLeft and the like. Where is the API for what I want to do?

[Aaron Liu]

Could you use docs#ContinuousLinearMap.postcomp twice?

[Aaron Liu]

import Mathlib

example {𝕜 E F G H : Type*} [NormedField 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    [NormedAddCommGroup G] [NormedSpace 𝕜 G]
    [NormedAddCommGroup H] [NormedSpace 𝕜 H]
    (f₁ : E →L[𝕜] F →L[𝕜] G) (f₂ : G →L[𝕜] H) :
    E →L[𝕜] F →L[𝕜] H :=
  (f₂.postcomp F).comp f₁

[Jireh Loreaux]

aha, thanks. It seems my claim about not working outside of normed spaces is probably bogus then. :laughing:

[Eric Wieser]

Should this name be standardized? I think the one for LinearMap is named something different.

[Eric Wieser]

This operation is compr\_2 there