Non-positive-definite inner product spaces

Stream: maths

[Eric Wieser]

Currently, docs#inner_product_space requires positive definite-ness.
nLab suggests that this is not a necessary condition for something to be an "inner product space", while wikipedia suggests that it is a necessary condition.

Without wanting to argue about whether the mathlib definition is correct, what would be a suitable name for the version whose inner product is not-necessarily-positive definite?

[Kevin Buzzard]

"space equipped with a symmetric bilinear form"?

[Kevin Buzzard]

I've never seen the nLab's convention used anywhere else BTW

[Andrea Berlingieri]

Maybe it's a silly question, and slightly off-topic w.r.t. your question, but isn't Wikipedia's definition "problematic" when the inner product goes to $\mathbb{C}$ , since it is not linearly ordered and thus the positive definiteness condition doesn't make sense in that case?

[Kevin Buzzard]

in the C case you assume sesquilinearity so (x,x) is always real-valued.

[Andrea Berlingieri]

Oh, I see. Thanks.

[Eric Wieser]

To motivate my question - this comes up when wanting to work in minkowski spacetime, for instance, where one unit basis vector squares to -1. It would be nice to still get norm and inner notation(and maybe dist), and have at least the bits of inner_product_space that show they are consistent with each other

[Yury G. Kudryashov]

You can't have norm in this case because norm is a real-valued function, and in Minkowski spacetime some squared norms are negative.

[Eric Wieser]

Oh, that's a good point - and I guess dist also has a square-root in it that makes it undesirable there. So I guess I don't have a reason to care about lemmas for norm and dist

[Jean-Philippe Burelle]

Many useful lemmas actually only involve the squared norm, and can be useful in indefinite signature. For instance, the "Pythagorean theorem" works as-is. Cauchy-Schwarz can also be adapted, but there are different cases depending on the sign of the "squared norm" of the vectors.