Commit 2025-01-14 02:38 266b0529

refactor: split Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances in a principled way (#20647) Before this PR, there were three files in which one could find instances of continuous functional calculi: Analysis.CStarAlgebra.ContinuousFunctionalCalculus.{Instances, Isometric, Unital}, which contained, respectively,

1. All generic instances of the CFC over ℂ, ℝ, ℝ≥0 for unital and non-unital algebras
2. All the instances of the isometric CFC.
3. The non-unital CFC for unital algebras. Note that importing Instances was therefore the general way to obtain a CFC on a CStarAlgebra. In this PR, the last one stays where it is, but there is a bit of shuffling for the others which we now explain. Here the problem with the above distribution of instances: if you are working on a generic CFC file (e.g., defining CFC.abs a := CFC.sqrt (star a * a), then you want to work in maximum generality. But to apply CFC.sqrt you need an instance of the ℝ≥0 functional calculus. The correct (i.e., well-behaved) way to do this is to assume that you have an ℝ-algebra (not an ℝ≥0-algebra, because those are ill-behaved) with the appropriate hypotheses. However, in order to get that instance, prior to this PR you would need to import Instances, which would pull in CStarAlgebra theory not relevant to the development of your file (and potentially, not even relevant to certain files downstream of the one on which you are working). The solution is to separate the instances which are inferred from existing instances (i.e., for obtaining ℝ from ℂ, or ℝ≥0 from ℝ) from the base level instances (i.e., the ones for ℂ which require CStarAlgebra). The former instances are left in either Instances or Isometric as the case may be, and the latter are moved into Basic. This means that Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic is now the entry point for getting all the relevant CFC instances for a CStarAlgebra. The rest of the files in this folder are for the more generic development of the CFC (with the exception of Order, which should likely be moved outside of this subfolder at some point. This should explain the large changes in the import hierarchy. The purpose of this refactor is to allow for more principled development of generic CFC functions, without importing more than necessary.