pre-inner product spaces

Stream: maths

[Jireh Loreaux]

@Frédéric Dupuis It doesn't look like we have pre-inner product spaces (i.e., where λ x, ⟪x, x⟫ is not definite but only semi-definite. This will be an essential part of the Gelfand-Naimark-Segal construction of a cyclic representation from a state on a C^*-algebra. For this one needs the Cauchy-Schwarz inequality for pre-inner product spaces and other related results. Any thoughts about how to modify existing code to go about incorporating this?

[Jireh Loreaux]

For reference the argument of the GNS construction proceeds as follows: Given a C⋆-algebra A over 𝕜, a state φ : A → 𝕜 makes A itself into a pre-inner product space via ⟪a, b⟫ := φ a⋆ b. Then one can quotient out by the closed left-ideal with carrier { a : A | φ a⋆ a = 0 } (maybe it's a right-ideal since I normally think of inner products as being conjugate
linear in the second coordinate, but mathlib does it in the first). Finally, one completes this inner product space to a Hilbert space H. Then one obtains a cyclic representation ρ : A → (H →L[𝕜] H) arising from the natural action of multiplication on H by elements of A.

[Jireh Loreaux]

Oh, actually, perhaps it's not strictly necessary after all. Instead maybe you can just define an inner product directly on A/I where I is the indicated ideal.

[Frédéric Dupuis]

It would be nice to avoid it if possible, since currently inner product spaces extend normed spaces, so it can't be easily modified to extend pre-inner product spaces.

[Yaël Dillies]

Why can't preinner product spaces extend prenormed spaces?

[Frédéric Dupuis]

I mean, it could definitely be done, but it sounds like a lot of work :-)

[Frédéric Dupuis]

Maybe it's not too bad: you could probably switch most of the current code with most of the basic lemmas to pre-inner product spaces instead.

[Yaël Dillies]

Meh, just a matter of copy-pasteing a file or two :wink:

[Yaël Dillies]

Yeah exactly. I could do that in a day or two.

[Frédéric Dupuis]

Well, code duplication is exactly what I would want to avoid.

[Yaël Dillies]

Some boilerplate code will be duplicated, but lemmas shouldn't.

[Frédéric Dupuis]

Right.

[Frédéric Dupuis]

Although if we're seriously considering a refactor of inner product spaces, there is also the question of whether we want to base them on bilinear forms. Now we could have inner be of type E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜.

[Yaël Dillies]

Another option is to have inner_hom a bundled version of inner.

[Frédéric Dupuis]

Yes -- see the big fat TODO right above docs#inner_right :-)

[Yaël Dillies]

Either way should be fine for the infoview because everything is buried under notation, right? I wouldn't wish anyone to see an horrendous ⇑(⇑inner x) y.

[Frédéric Dupuis]

I'm still not sure it's worth the trouble though.

[Jireh Loreaux]

Yeah, I would say not. I'm betting most of the time you can just take the quotient ahead of time like in this situation with A/I. If it becomes an issue we can always refactor/add this feature later.