Commit 2025-12-15 09:35 12909179

chore(RingTheory): rename RingHom.specComap to PrimeSpectrum.comap (#32703) and remove the old PrimeSpectrum.comap, which was RingHom.specComap bundled as a continuous map. Having both RingHom.specComap and PrimeSpectrum.comap leads to two ways of writing the same thing, with every lemma written before the topology-on-PrimeSpectrum-barrier stated in terms of RingHom.specComap and most lemmas after it stated in terms of PrimeSpectrum.comap. Since the bundled continuous map version is not useful, because the topology library rarely takes continuous maps as input, we remove the bundled version, but keep the name PrimeSpectrum.comap for the unbundled one.