English
The construction mapHom defines a contravariant functor from continuous monoid homs to morphisms between Pontryagin duals, with the standard functorial coherence.
Русский
Построение mapHom определяет противооднозначный функтор между непрерывными моноидными гомоморфизмами и морфизмами между дуальными группами Понтрягиана, с корректной когерентностью функторов.
LaTeX
$$$\\text{mapHom}:[LocallyCompactSpace G]\\Rightarrow ( (A \\toₜ* G) \\toₜ* (PontryaginDual G) \\to PontryaginDual A)$$$
Lean4
/-- `ContinuousMonoidHom.dual` as a `ContinuousMonoidHom`. -/
def mapHom [LocallyCompactSpace G] : (A →ₜ* G) →ₜ* ((PontryaginDual G) →ₜ* (PontryaginDual A))
where
toFun := map
map_one' := map_one
map_mul' := map_mul
continuous_toFun := continuous_of_continuous_uncurry _ continuous_comp
