integral lattice: inner product notation

Stream: mathlib4

[Johan Commelin]

I think it makes sense to use inner product notation for integral lattices. But that notation is introduced in Mathlib.Analysis.InnerProductSpace.Basic. So I suggest that we split that file. What would be a good place to put the file that introduces the inner product notation? Mathlib.Algebra.Module.Inner?

[Jireh Loreaux]

Somewhat unrelated: for a while I've been thinking it would be nice to have an inner product class which provides the semilinear map, but doesn't connect it to the topology or provide a norm. In this way, we could have the natural inner product on functions n \to \bbk without ruining everything.

[Johan Commelin]

With "semilinear map", do you mean the bilinear map?

[Johan Commelin]

Or are you talking about some Hermitian thing?

[Antoine Chambert-Loir]

That is of course a thing to have. Especially when we'll want to study orthogonal groups and things like that, in whatever characteristic.

[Jireh Loreaux]

@Johan Commelin I'm talking about having innerₛₗ without the topology requirement.

[Jireh Loreaux]

so that's conjugate linear in the first coordinate and linear in the second.

[Jireh Loreaux]

If we want the version that's bilinear instead of sesquilinear, it would be good to have different notation for it.

[Eric Wieser]

I worry that this will lead to the immediate question "why can't we have norm x = inner x x and keep ignoring topology", and now we either have an instance diamond, or have just slightly moved the annoyance rather than solving it

[Jireh Loreaux]

I don't think that fear is justified. I certainly am not asking for that, and I'm not really sure why people would want to talk about the norm without invoking the topology. That seems pretty niche. In contrast, having the inner product available (especially in bundled form) is handy.

[Eric Wieser]

I worry that this will encourage new users to write inner x y / norm y as part of a projection in linear algebra, and will end up much more confused by the wrong norm than they would have been if inner were just an error