[Merged by Bors] - feat: abstract continuous functional calculus for unital algebras #5750

j-loreaux · 2023-07-06T22:41:25Z

This PR introduces two classes ContinuousFunctionalCalculus and UniqueContinuousFunctionalCalculus. The former provides a collection of star algebra homomoprhisms from the continuous functions on the spectrum of an element a : A, into the algebra A itself, subject to the constraint that a satisfies a certain predicate p : A → Prop. These morphisms are continuous (even closed embeddings) and send the identity function to a itself, and moreover, the spectrum of the image of an element is its range.

The latter class says that there is at most one such star algebra homomorphism which is continuous and maps the identity to a; in practice, this is a consequence of the Stone-Weierstrass theorem, but we create a separate class because we will also want a version for ℝ≥0-valued functions. This latter class is the key to establish the compositional property of the continuous functional calculus, cfc_comp : cfc a (g ∘ f) = cfc (cfc a f) g. This is one of the key properties of the continuous functional calculus that makes it useful.

Note to reviewers: this PR has been completely overhauled, so none of the messages ‌/ reviews prior to 2024-02-19 are relevant.

Also, any line labeled -- hack is there to make fun_prop see through the autoParam. This will be fixed in #10724.

Mathlib/Topology/ContinuousFunction/CFC.lean

ADedecker · 2023-07-07T11:44:51Z

I haven't looked at everything carefully, but this looks very promising. One thing I'm wondering is wether we could find a typeclass that would also encompass the Borel Functional Calculus, but that is probably too much to ask for.

Quick questions:

I'm probably missing something obvious, but do you have examples where CFCCoreClass holds but not CFCClass?
regarding the names, what do you think about CFC and SpectrumPreservingCFC? There is also the closed embedding difference of course, but maybe we can not insist on that in the names.

j-loreaux · 2023-07-07T15:13:10Z

No, I don't have an example.

The CFCCoreClass only exists to make the proof of the composition property easier. When proving that, you need to construct a CFC in the middle of the proof, then you use that it is a subsingleton to say that the one you constructed is equal to the one you already have. However, since the subsingleton property holds for Core we can do less work in the construction.

Note: I am also keen to use the Subsingleton proof because we will be able to supply an instance when the scalars are NNReal too, even though right now the only one we have is for IsROrC.

ADedecker · 2023-07-21T20:19:11Z

I spent some time thinking about how I would do this, here's a summary of my (untested!) ideas. Some of them are probably overkill but I still want to write them down somewhere, and I hope at least some of it will be useful. Also disclaimer that I'm probably not familiar enough with the material to avoid making some silly mistake, sorry in advance!

My first and main idea is to have a class FunctionalCalculus R F a X expressing that the R (?)-algebra F (which is morally an algebra of functions) on the element a : A, where A is a R (?)-algebra, and that this functional calculus maps some distinguished element X : F to a. Under this assumption, we would be able to write fc R a f for any f : F.
Here (?)-algebra means that we have to think about what assumptions we put on the algebra. We also get to choose properties of the functional calculus (the bare minimum being of course algebra homomorphism), and depending on the level of generality we choose we'll be able to state some of the followings:

when A is a C*-algebra and a : A is star-normal, we can have two instances encompassing both your cfc₁ and cfc₂, namely FunctionalCalculus R C(spectrum R a, R) a X.toContinuousMapOn as well as FunctionalCalculus R C(R, R) a X.toContinuousMap [1]. That means that we can kind of unify the APIs, at least for the user perspective (we still need to define all of the instances twice though). This also means that, even if we don't want it as an global instance, a user could add instances of FunctionalCalculus R C(T, R) a X.toContinuousMapOn if they know that T contains the spectrum of a. [2]
if we don't impose too strong continuity assumption, this same setup could apply to the borel functional calculus.
if we don't ask for unital algebras, this same setup could apply to the continuous functional calculus of non-unital C*-algebras [3]
I'm not sure how useful it is, but we can make an instance for polynomials 😅 It may be convenient if we want to use some general composition setup, see below.

Of course this doesn't allow for a lot of factoring in the actual mathematical content, because a lot of properties will only work for one functional calculus. But the point is that, for the user, it provides a more unified experience and less lemma names to remember (and less chance that we forget stating a result for only one of the calculi).

The next step is figuring how to state and prove the spectrum and composition properties in this setup. I think from the user point of view, the most basic version would be to have the following two mixins:

MapsSpectrum R F x im, where im : F -> Set R [4], saying that the spectrum of fc R a f is exactly im f. Typically im would be the range of f / f(Sp a) / the essential range of f.
CompFCClass R f1 a cmp, where f1 : F1, cmp F2 -> F3, [FunctionalCalculus R F1 a X1], [FunctionalCalculus R F3 a X3], [FunctionalCalculus R F2 (fc R f1 a) X2], saying that for all f2 : F2, we have fc R (fc R a f1) f2 = fc R a (cmp f2). Typically, cmp would be pre-composition by f1. The nice thing is that, from the user perspective there'd be exactly one lemma for your three existing versions [EDIT: actually it doesn't quite work for the full cfc₁ version, because C(spectrum R a, spectrum R (cfc₁ f a)) is not an algebra], because we still, and the same lemma could also apply to compositions between continuous and borel functional calculi for example. The not-so-nice thing is that you still have to provide all of these instances by hand. This leads me to my other idea.

This second idea is a way of systematizing the proofs of composition properties, either in the context of the aforementioned CompFCClass or just for proving manual lemmas. This can be adapted to be independent of the previous idea if necessary. We would have a class/structure UniqueFunctionalCalculus R F a X p q [5] where p : FunctionalCalculus R F a X -> Prop adds additional restrictions to the functional calculus (typically continuity if we don't require it in FunctionalCalculus and q : F -> F -> Prop is a relation of functions. This would be defined as "given two functional calculi φ and ψ satisfying p, and which are compatible with the relation q, then they are equal". In the unital CFC case, we would have the usual UniqueFunctionalCalculus R C(spectrum R a, R) a X.toContinuousMapOn continuous (· = ·), but also UniqueFunctionalCalculus R C(R, R) a X.toContinuousMap continuous (EqOn (spectrum R A)) giving some kind of uniqueness result for cfc₂. Using that we can write a "composition factory" lemma to prove the composition property purely by verifying that the predicate p and the relation q behave "nicely" under our composition operation, whatever it is. (I'll edit it in there later, I need some time to write this lemma properly).

Again, this is probably overkill, but the semilinear maps API suggest that it is at least possible, and I wanted to write in completely somewhere if we decide to pick some ideas from it in the future.

Footnotes:

[1] using Polynomial.toContinuousMap[On] seems a bit weird, using ContinuousMap.id seems easier but I don't know if we have a name for the inclusion map as a bundled ContinuousMap
[2] I think we could also use the freedom given by the choice of algebra to take care some of the "change of base ring" stuff, but I haven't thought about it enough.
[3] if we do so we'll probably need a UnitalFunctionalCalculus typeclass that extends FunctionalCalculus, and we could have notations like fcₙ for the non-unital one and fc for the unital one
[4] would be an OutParam

j-loreaux · 2024-02-23T16:53:23Z

@YaelDillies see https://github.com/leanprover-community/mathlib4/tree/j-loreaux%2Funital-cfc-class-prop

OmarMohsenGit · 2024-02-23T16:58:41Z

Out of curiosity do you know a (studied) case where cfc isn't unique?

j-loreaux · 2024-02-23T17:58:51Z

@OmarMohsenGit I guess it depends on what you mean. Among functional calculi that people use, no, but if you take a non-compact set s to replace the spectrum and look at all continuous functions (not just those vanishing at infinity), then I think it likely won't be unique (because Stone--Weierstrass doesn't apply). So, with the type class assumptions that we have available I don't think it's provable, because for compactness of the spectrum we'd need a Banach algebra.

And I think the reason no one uses it if it isn't uniquely determined is that the composition property won't be provable (probably).

I'm not sure whether this adequately answers your question or not.

dupuisf · 2024-02-23T21:18:59Z

Two final notes to reviewers:

1. Currently, almost everything is just dropped into the root namespace. Should we hide any / all of these behind a namespace?

Since pretty much everything is named cfc_something I think it's fine.

2. Anatole pointed out to me that the current setup has the unfortunate side effect that we can't put the C⋆-norm as a local instance on matrices without then getting conflicts for `cfc` (i.e., two different instances of `ContinuousFunctionalCalculus`). One fix for this would be to turn the class into a `Prop` (this is relatively easy and only takes changes to a few lines). Since the cfc is unique in all cases we care about, this doesn't really hurt us. The only issue is that, in order to use properties specific to a particular version (e.g., on a C⋆-algebra it's an isometry), we would need to first identify it with an existing thing that we know is an isometry. With the non-`Prop` version, we can just appeal to the definition. I'm inclined to make it a `Prop`.

Well, I was in favor of this solution pretty much from the start -- I'm glad Anatole found a concrete issue to make my vague concerns more substantial :-)

j-loreaux · 2024-02-23T22:00:28Z

Alright, I've switch to a Prop version. The switch is painless, so if we decide sometime soon that we want to go back, then we can, but I think this is preferable too.

ADedecker

Here is my final review! We may be able to clean up some other things at some point, but this is looking great!

Final question: do we really want this file in the Topology folder? I mean technically it doesn't mention any norm at all, but it feels like it should be in Analysis, no?

Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

ADedecker · 2024-02-24T18:33:09Z

Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

+  induction q using Polynomial.induction_on with
+  | h_C r => simp [cfc_const a r]
+  | h_add q₁ q₂ hq₁ hq₂ =>
+    simp only [eval_add, map_add, ← hq₁, ← hq₂, cfc_add a (q₁.eval <| f ·) (q₂.eval <| f ·)]
+  | h_monomial n r _ =>
+    simp only [eval_mul, eval_C, eval_pow, eval_X, map_mul, aeval_C, map_pow, aeval_X]
+    rw [cfc_const_mul .., cfc_pow _ _ (n + 1),
+      ← smul_eq_mul, algebraMap_smul]


If you add

open Polynomial in lemma cfcHom_map_polynomial (q : R[X]) (f : C(spectrum R a, R)) : cfcHom ha (aeval f q) = aeval (cfcHom ha f) q := .symm <| aeval_algHom_apply _ _ _

as well as

@[simp] lemma ContinuousMap.aeval_apply {X R A : Type*} [CommSemiring R] [TopologicalSpace X] [TopologicalSpace A] [CommSemiring A] [Algebra R A] [TopologicalSemiring A] (f : C(X, A)) (q : R[X]) (x : X) : aeval f q x = aeval (f x) q := by rw [← coeFnAlgHom_apply R, ← aeval_algHom_apply] -- note : aeval_fn_apply should be generalized to algebras exact .symm <| aeval_algHom_apply (Pi.evalAlgHom R (fun _ ↦ A) x) _ _

you can do

Suggested change

induction q using Polynomial.induction_on with

| h_C r => simp [cfc_const a r]

| h_add q₁ q₂ hq₁ hq₂ =>

simp only [eval_add, map_add, ← hq₁, ← hq₂, cfc_add a (q₁.eval <| f ·) (q₂.eval <| f ·)]

| h_monomial n r _ =>

simp only [eval_mul, eval_C, eval_pow, eval_X, map_mul, aeval_C, map_pow, aeval_X]

rw [cfc_const_mul .., cfc_pow _ _ (n + 1),

← smul_eq_mul, algebraMap_smul]

rw [cfc_apply a _, cfc_apply a _, ← cfcHom_map_polynomial]

congr 1

ext x

simp

This can wait for another PR.

Nice! I'll wait for another PR just because ContinuousMap.aeval_apply should go in a different file.

Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

j-loreaux · 2024-02-25T06:20:27Z

Final question: do we really want this file in the Topology folder? I mean technically it doesn't mention any norm at all, but it feels like it should be in Analysis, no?

C⋆-algebras are just noncommutative topology, so I actually think we should move all of the C⋆-algebra material into the Topology folder. (:rofl: obviously joking)

In all seriousness, I considered both ways. On the one hand, it makes more sense in Analysis, but in another sense it's a bit weird to be importing that for matrices. I'm okay with putting it elsewhere, whatever reviewers decide.

OmarMohsenGit · 2024-02-25T09:35:31Z

I think creating an operator algebra folder is more logical but I am not experienced enough with mathlib.

YaelDillies · 2024-02-25T14:31:03Z

I think the folder doesn't matter too much at this point. We can always change it as we acquire more material.

ADedecker · 2024-02-27T18:33:58Z

The discussion around eta-expansion was not competely settled but I think 1) for now we definitely want the extended versions for fun_prop to work, and 2) this is easy to change later (and we will probably have to change some bits of the API anyway). So let's move forward!

bors r+

Thanks a lot! 🎉

) This PR introduces two classes `ContinuousFunctionalCalculus` and `UniqueContinuousFunctionalCalculus`. The former provides a collection of star algebra homomoprhisms from the continuous functions on the spectrum of an element `a : A`, into the algebra `A` itself, subject to the constraint that `a` satisfies a certain predicate `p : A → Prop`. These morphisms are continuous (even closed embeddings) and send the identity function to `a` itself, and moreover, the spectrum of the image of an element is its range. The latter class says that there is at most one such star algebra homomorphism which is continuous and maps the identity to `a`; in practice, this is a consequence of the Stone-Weierstrass theorem, but we create a separate class because we will also want a version for `ℝ≥0`-valued functions. This latter class is the key to establish the compositional property of the continuous functional calculus, `cfc_comp : cfc a (g ∘ f) = cfc (cfc a f) g`. This is one of the key properties of the continuous functional calculus that makes it useful.

mathlib-bors · 2024-02-27T19:35:40Z

Build failed (retrying...):

Build

) This PR introduces two classes `ContinuousFunctionalCalculus` and `UniqueContinuousFunctionalCalculus`. The former provides a collection of star algebra homomoprhisms from the continuous functions on the spectrum of an element `a : A`, into the algebra `A` itself, subject to the constraint that `a` satisfies a certain predicate `p : A → Prop`. These morphisms are continuous (even closed embeddings) and send the identity function to `a` itself, and moreover, the spectrum of the image of an element is its range. The latter class says that there is at most one such star algebra homomorphism which is continuous and maps the identity to `a`; in practice, this is a consequence of the Stone-Weierstrass theorem, but we create a separate class because we will also want a version for `ℝ≥0`-valued functions. This latter class is the key to establish the compositional property of the continuous functional calculus, `cfc_comp : cfc a (g ∘ f) = cfc (cfc a f) g`. This is one of the key properties of the continuous functional calculus that makes it useful.

mathlib-bors · 2024-02-27T20:02:26Z

Pull request successfully merged into master.

Build succeeded:

) This PR introduces two classes `ContinuousFunctionalCalculus` and `UniqueContinuousFunctionalCalculus`. The former provides a collection of star algebra homomoprhisms from the continuous functions on the spectrum of an element `a : A`, into the algebra `A` itself, subject to the constraint that `a` satisfies a certain predicate `p : A → Prop`. These morphisms are continuous (even closed embeddings) and send the identity function to `a` itself, and moreover, the spectrum of the image of an element is its range. The latter class says that there is at most one such star algebra homomorphism which is continuous and maps the identity to `a`; in practice, this is a consequence of the Stone-Weierstrass theorem, but we create a separate class because we will also want a version for `ℝ≥0`-valued functions. This latter class is the key to establish the compositional property of the continuous functional calculus, `cfc_comp : cfc a (g ∘ f) = cfc (cfc a f) g`. This is one of the key properties of the continuous functional calculus that makes it useful.

j-loreaux added 6 commits July 6, 2023 11:05

feat: link the Stone-Weierstrass theorem to the StarSubalgebra API

d361d27

refactor to avoid ConjInvariantSubalgebra

454e1df

fix Gelfand duality

41ccd64

lint

0de4ec2

fix

eddd31f

error free

6705d9d

j-loreaux added awaiting-review labels Jul 6, 2023

semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Jul 6, 2023

ocfnash added the RFC Request for comment label Jul 7, 2023

ADedecker reviewed Jul 7, 2023

View reviewed changes

Mathlib/Topology/ContinuousFunction/CFC.lean Outdated Show resolved Hide resolved

j-loreaux added WIP Work in progress and removed awaiting-review labels Jul 7, 2023

j-loreaux added 6 commits July 18, 2023 15:10

some changes

3f48084

some changes

7327b6b

some commuting things

5da3ca9

lots o' changes

6849756

import into Mathlib.lean

f30dbc0

merge master

1d9199b

j-loreaux added 2 commits July 24, 2023 10:46

some changes

1a3496b

make H an outParam

fae2b66

semorrison removed the after-port label Jul 25, 2023

try to add Unique stuff

5928d2b

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Jul 28, 2023

leanprover-community deleted a comment from semorrison Jul 28, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 28, 2023

switch cfc_comp and cfc_comp'

5af3a75

j-loreaux added 2 commits February 23, 2024 15:42

make ContinuousFunctionalCalculus a Prop

390242b

remove IsCFCHom structure

bd208b5

ADedecker approved these changes Feb 24, 2024

View reviewed changes

Apply suggestions from code review

7866c0d

Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

fixes

23ba6f3

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 27, 2024

mathlib-bors bot changed the title ~~feat: abstract continuous functional calculus for unital algebras~~ [Merged by Bors] - feat: abstract continuous functional calculus for unital algebras Feb 27, 2024

mathlib-bors bot closed this Feb 27, 2024

mathlib-bors bot deleted the j-loreaux/unital-cfc-class branch February 27, 2024 20:02

j-loreaux restored the j-loreaux/unital-cfc-class branch February 27, 2024 21:08

j-loreaux deleted the j-loreaux/unital-cfc-class branch February 27, 2024 21:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: abstract continuous functional calculus for unital algebras #5750

[Merged by Bors] - feat: abstract continuous functional calculus for unital algebras #5750

j-loreaux commented Jul 6, 2023 •

edited by YaelDillies

Loading

ADedecker commented Jul 7, 2023

j-loreaux commented Jul 7, 2023

ADedecker commented Jul 21, 2023 •

edited

Loading

j-loreaux commented Feb 23, 2024

OmarMohsenGit commented Feb 23, 2024

j-loreaux commented Feb 23, 2024 •

edited

Loading

dupuisf commented Feb 23, 2024

j-loreaux commented Feb 23, 2024

ADedecker left a comment

ADedecker Feb 24, 2024

j-loreaux Feb 25, 2024

j-loreaux commented Feb 25, 2024

OmarMohsenGit commented Feb 25, 2024

YaelDillies commented Feb 25, 2024

ADedecker commented Feb 27, 2024

mathlib-bors bot commented Feb 27, 2024

mathlib-bors bot commented Feb 27, 2024

[Merged by Bors] - feat: abstract continuous functional calculus for unital algebras #5750

[Merged by Bors] - feat: abstract continuous functional calculus for unital algebras #5750

Conversation

j-loreaux commented Jul 6, 2023 • edited by YaelDillies Loading

ADedecker commented Jul 7, 2023

j-loreaux commented Jul 7, 2023

ADedecker commented Jul 21, 2023 • edited Loading

j-loreaux commented Feb 23, 2024

OmarMohsenGit commented Feb 23, 2024

j-loreaux commented Feb 23, 2024 • edited Loading

dupuisf commented Feb 23, 2024

j-loreaux commented Feb 23, 2024

ADedecker left a comment

Choose a reason for hiding this comment

ADedecker Feb 24, 2024

Choose a reason for hiding this comment

j-loreaux Feb 25, 2024

Choose a reason for hiding this comment

j-loreaux commented Feb 25, 2024

OmarMohsenGit commented Feb 25, 2024

YaelDillies commented Feb 25, 2024

ADedecker commented Feb 27, 2024

mathlib-bors bot commented Feb 27, 2024

mathlib-bors bot commented Feb 27, 2024

j-loreaux commented Jul 6, 2023 •

edited by YaelDillies

Loading

ADedecker commented Jul 21, 2023 •

edited

Loading

j-loreaux commented Feb 23, 2024 •

edited

Loading