PR summary e347b5a8eb

Import changes for modified files

No significant changes to the import graph

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

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

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.

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.

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)

✌️ 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.

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.

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?

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style