injectiveSeminorm

Stream: mathlib4

[David Gross]

It turns out that PiTensorProduct.injectiveSeminorm is extensionally equal to PiTensorProduct.projectiveSeminorm. Both implement what is commonly called the "projective tensor norm".

We had a helpful email conversation with the original author, @Sophie Morel. She says that this equality isn’t by design and agrees that injectiveSeminorm should be changed.

To discuss how to proceed, we’ve prepared two PRs.

#34137 removes injectiveSeminorm and ports all applications to projectiveSeminorm. This doesn't actually require too much work, leads to the same mathematical theory, and significantly reduces complexity (and potential for confusion!).

#33969 formalizes the equality of the current definitions and has a WIP / RFC implementation of the injective seminorm as commonly understood. This one is quite far from being done, though.

The PR description of #34137 has more technical details.

What would be the best way to proceed?

[Sophie Morel]

I confirm that we had the discussion and I made a mistake in defining injective seminorms. They should be removed or changed.