[Merged by Bors] - feat: InnerProductSpace (SeparationQuotient E)

[eric-wieser]

---

[eric-wieser]

Thanks @ADedecker for pointing out that this map and .eq API existed!

[github-actions]

PR summary e347b5a8eb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Inseparable.inner_eq_inner
+ inner_mk_mk
+ instance : Inner 𝕜 (SeparationQuotient E)
+ instance : InnerProductSpace 𝕜 (SeparationQuotient E)

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[ADedecker]

Sorry, could you explain quickly what is the relation between this and #16707 ?

Also, @yoh-tanimoto, I see you have the GNS in mind, do you already have some working code ? I was planning on doing this before the summer, but I don't want to step on your toes.

[eric-wieser]

My thought here is that #16707 could probably cover the equivalence between SeparationQuotient and the quotient module by the null-space submodule; but that we shouldn't take that as the definition, and should just directly lift the inner operation through the quotient as I did for norm in #17452, and as we already did for dist.

[ADedecker]

Ah, I see. My opinion on this is "just use SeparationQuotient", so I'm not even sure we really need to state the other construction. But we can discuss that somewhere else.

bors d+
(In case you want to wait on @yoh-tanimoto's review)

[mathlib-bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors merge

so I'm not even sure we really need to state the other construction. But we can discuss that somewhere else.

I think it would be nice to state simply to show equivalence, but probably if @yoh-tanimoto has further goals it isn't actually necessary to reach them.

[yoh-tanimoto]

you two are very quick, and the code is so short, I'm impressed!

@ADedecker No, I don't have a single line of code of GNS. I'm not sure what I will work on next, so if you wish, please go ahead.

I don't know whether other constructions (by lift of toDualMap?) are needed, but implementing lifts as (continuous) linear maps is necessary, I think. For example, if you have an automorphism of a C^*-algebra preserving the state, in the GNS representation it is represented by a unitary operator. That should be the norm completion of the lift.

Should I use #16707 for this purpose, or open a new one?

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style