mathlib

e702f021 - feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an `alg_hom` (#16451)

feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an `alg_hom` (#16451) This defines the `gelfand_transform` as an algebra homomorphism from a `𝕜`-algebra `A` into the continuous functions from the `character_space 𝕜 A` into the base field `𝕜`, where the map is given by evaluation. For this definition it is only supposed that `𝕜` is a topological ring and `A` is a topological space. When the algebra `A` is a C⋆-algebra over `ℂ`, algebra homomorphisms of `A` into `ℂ` (hence also terms of `character_space ℂ A`) are automatically star-preserving. Therefore, in this setting the Gelfand transform may be upgraded to a `star_alg_hom`. However, we do not implement that here because, with more work, one may show that this is actually an equivalence. - [x] depends on: #16438