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?
Kevin Buzzard (Feb 01 2021 at 10:00):
"space equipped with a symmetric bilinear form"?
Kevin Buzzard (Feb 01 2021 at 10:02):
I've never seen the nLab's convention used anywhere else BTW
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 , since it is not linearly ordered and thus the positive definiteness condition doesn't make sense in that case?
Kevin Buzzard (Feb 01 2021 at 10:33):
in the C case you assume sesquilinearity so (x,x) is always real-valued.
Andrea Berlingieri (Feb 01 2021 at 10:34):
Oh, I see. Thanks.
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
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 (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.
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
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