Topic: Inner product spaces
Alexander Bentkamp (Mar 15 2019 at 20:15):
Is there anyone else currently interested in inner product spaces? I'd like to start working on this.
I found this formalization:
@Andreas Swerdlow Are there still plans to bring this into mathlib?
I am also aware of the Lean2 formalization: https://github.com/leanprover/lean2/blob/master/library/theories/analysis/inner_product.lean
The ImperialCollege formalization is over complex numbers and the Lean2 formalization is over the reals. I am interested in the reals, but I will try to find a generalization that subsumes both. Are there any concepts like this already?
Johan Commelin (Mar 15 2019 at 20:19):
There is the whole theory of quadratic forms, which works over any field (though characteristic 2 can be hairy).
Johan Commelin (Mar 15 2019 at 20:20):
Then you can specialise to nondegenerate forms, symmetric forms, alternating forms, hermitian forms, etc...
Kevin Buzzard (Mar 15 2019 at 20:30):
In number theory we define unitary groups in the setting where K is a field (say) and L/K is a finite etale K-algebra of degree 2, which is a fancy way of saying either L=K+K or L is a separable quadratic extension of K. The non-trivial K-automorphism of L is denoted c, say (c for complex conjugation if K=real and L=complex) and then one can consider a non-degenerate hermitian sesquilinear form on an L-vector space. For it to be positive definite you need some notion of positive though, so then K should embed into the reals.
Alexander Bentkamp (Mar 15 2019 at 20:54):
Ok, thanks. I'll see what I can do.
Andreas Swerdlow (Mar 16 2019 at 02:41):
I was thinking of submitting to mathlib fairly soon. A more up to date version is available here: https://github.com/leanprover-fork/mathlib-backup/blob/inner_product_spaces/linear_algebra/herm_inner_product_space.lean
Alexander Bentkamp (Mar 16 2019 at 17:34):
I have transferred the Lean2 formalization to Lean3 now. It's for real vector spaces only. Let's see if we can merge after you submit to mathlib.
Last updated: May 14 2021 at 05:20 UTC