mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/normed_space/star/multiplier): construct the multiplier algebra of a C*-algebra

Open j-loreaux opened this issue 3 years ago • 1 comments

Define the multiplier algebra of a C⋆-algebra as the algebra (over 𝕜) of double centralizers, for which we provide the localized notation 𝓜(𝕜, A). A double centralizer is a pair of continuous linear maps L R : A →L[𝕜] A satisfying the intertwining condition R x * y = x * L y.

There is a natural embedding A → 𝓜(𝕜, A) which sends a : A to the continuous linear maps L R : A →L[𝕜] A given by left and right multiplication by a, and we provide this map as a coercion.

In this PR we put all the natural structures on 𝓜(𝕜, A), culminating in the fact that it is a unital C⋆-algebra when A is a (unital or non-unital) C⋆-algebra.

  • [x] depends on: #15868
  • [x] depends on: #15657
  • [ ] depends on: #16963
  • [ ] depends on: #16964

Co-authored-by: Jon Bannon

Open in Gitpod

j-loreaux avatar Aug 04 '22 22:08 j-loreaux

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15868~~
  • ~~leanprover-community/mathlib#15657~~
  • ~~leanprover-community/mathlib#16963~~
  • leanprover-community/mathlib#16964 By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Aug 09 '22 22:08 mathlib-dependent-issues-bot

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15868~~
  • ~~leanprover-community/mathlib#15657~~
  • ~~leanprover-community/mathlib#16963~~
  • ~~leanprover-community/mathlib#16964~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Nov 09 '22 23:11 mathlib-dependent-issues-bot

What fun. :-) This is lovely.

kim-em avatar Nov 11 '22 10:11 kim-em

:v: j-loreaux 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[bot] avatar Feb 23 '23 20:02 bors[bot]

I actually considered that a week ago. Actually to be more precise, I sent Yaël a direct message in which I put a (local instance) star structure on the product and constructed this as a star_subalgebra. It worked and it wasn't terribly long, but:

  1. I think type class inference will behave better with a dedicated type instead of coe_to_sort. I have had some issues with the continuous functional calculus in this regard (at least, I think that's what the problem is).
  2. We don't have to deal with mul_opposite as much this way
  3. I only did the star algebra structure in my test, not the norm structure. I don't anticipate it would cause any issues though.

j-loreaux avatar Feb 23 '23 20:02 j-loreaux

bors merge

j-loreaux avatar Feb 23 '23 22:02 j-loreaux

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Feb 24 '23 00:02 bors[bot]