Polish spaces of continuous homomorphisms

The compact-open space of continuous homomorphisms from a second-countable locally compact monoid to a Polish topological monoid is Polish. In particular, this supplies the regularity of spaces of characters needed for uniqueness of Fourier–Stieltjes measures.

instance ContinuousMonoidHom.instPolishSpace {A : Type u_1} {B : Type u_2} [Monoid A] [TopologicalSpace A] [LocallyCompactSpace A] [SecondCountableTopology A] [Monoid B] [TopologicalSpace B] [ContinuousMul B] [PolishSpace B] : PolishSpace (A →ₜ* B)

Continuous homomorphisms from a second-countable locally compact monoid to a Polish topological monoid form a Polish space in the compact-open topology.