Commit 2026-02-23 18:16 a4b2839e

refactor: weaken IsClosedEmbedding requirement in ContinuousFunctionalCalculus (#35551) Consider the following. Suppose A is a C⋆-algebra. We are constantly considering various alternative topologies on A, e.g., the weak operator topology, the strong operator topology, the ultraweak topology, the strict topology on the multiplier algebra, the strong and strong-* topologies, etc. With the current incarnation of ContinuousFunctionalCalculus we can get an instance on A. However, when we work the the type synonym WeakerOpTopology A we also want to be able to do things involving the functional calculus on that type. But as-is, the ContinuousFunctionalCalculus class is too restrictive because it requires the map from C(spectrum R a, R) into the algebra to be a closed embedding. This means that, at least locally on the closed star subalgebra generated by a single element, the topology is induced by a C⋆-norm; thereby prohibiting any type synonym of A with a weaker topology. The reason IsClosedEmbedding was originally a requirement is because we wanted to be able to recover the ⋆-algebra equivalence with the C⋆-subalgebra generated by element of A. This is still important (but can be accomplished with the isometric variant of the ContinuousFunctionalCalculus class). However, when working in a type synonym, this condition doesn't really make any sense anyway, because the topological closure would be taken relative to a different topology (the norm topology) than the one you have on your type synonym. And indeed, taking the closure relative to this weaker topology will in general result in a subalgebra which is too big. At the same time, the vast majority of properties of the functional calculus don't need this condition, and all that is really needed is injectivity and continuity. Injectivity will of course still be satisfied by the type synonym, and so will continuity because cfcHom : C(spectrum R a, R) → A → WeakerOpTopology A is a composition of continuous maps. Note that even ContinuousMap.UniqueHom will still in general be satisfied as long as the weaker topology is Hausdorff which it always is for topologies we care about, so the composition property holds; at least for ℝ or ℂ. For ℝ≥0 there is currently an IsTopologicalRing A requirement which will in general not be satisfied by the weaker topology, because multiplication is not jointly continuous. However, this can likely be addressed by introducing classes for one-sided continuity of multiplication. Everything about the above applies equally well to non-unital algebras. This PR weakens the requirements of the homomorphisms in ContinuousFunctionalCalculus from IsClosedEmbedding to Continuous + Injective. The existing IsClosedEmbedding version around under a different name for now, but this may perhaps be removed in the future.