Zulip Chat Archive

Stream: maths

Topic: Non-positive-definite inner product spaces


view this post on Zulip Eric Wieser (Feb 01 2021 at 09:59):

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?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:00):

"space equipped with a symmetric bilinear form"?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:02):

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

view this post on Zulip Andrea Berlingieri (Feb 01 2021 at 10:33):

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 C\mathbb{C} , since it is not linearly ordered and thus the positive definiteness condition doesn't make sense in that case?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 10:33):

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

view this post on Zulip Andrea Berlingieri (Feb 01 2021 at 10:34):

Oh, I see. Thanks.

view this post on Zulip Eric Wieser (Feb 01 2021 at 10:51):

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

view this post on Zulip Yury G. Kudryashov (Feb 01 2021 at 14:44):

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

view this post on Zulip Eric Wieser (Feb 01 2021 at 16:02):

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

view this post on Zulip Jean-Philippe Burelle (Feb 04 2021 at 14:57):

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.


Last updated: May 10 2021 at 07:15 UTC