Topology of Pontryagin duals

The Pontryagin dual of a second-countable locally compact monoid is Polish. For locally compact abelian groups this ensures that finite Borel measures on the dual are tight and determined by their Fourier–Stieltjes transforms.

A continuous character of the discrete group ℤ is determined by its value at 1, which may be any point of the unit circle. This file packages that correspondence as an isomorphism of topological groups between the unit circle and the Pontryagin dual of ℤ. It lets statements about the dual of ℤ, such as Fourier–Stieltjes transforms of measures on it, be read on the concrete unit circle, where a character becomes the monomial z ↦ zⁿ.

Main definitions

• TauCeti.circleEquivPontryaginDualInt: the point z of the unit circle corresponds to the character n ↦ zⁿ of ℤ.

References

• W. Rudin, Fourier Analysis on Groups, Interscience (1962), §1.2 (the dual group).

instance TauCeti.instPolishSpacePontryaginDual {A : Type u_1} [Monoid A] [TopologicalSpace A] [LocallyCompactSpace A] [SecondCountableTopology A] : PolishSpace (PontryaginDual A)

The Pontryagin dual of a second-countable locally compact monoid is Polish.

noncomputable def TauCeti.circleEquivPontryaginDualInt : Circle ≃ₜ* PontryaginDual (Multiplicative ℤ)

The unit circle is the Pontryagin dual of ℤ: the point z corresponds to the character n ↦ zⁿ, and a character corresponds to its value at 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.circleEquivPontryaginDualInt_apply_apply (z : Circle) (n : Multiplicative ℤ) : (circleEquivPontryaginDualInt z) n = z ^ Multiplicative.toAdd n

The character attached to z sends n to zⁿ.

@[simp]

theorem TauCeti.circleEquivPontryaginDualInt_symm_apply (χ : PontryaginDual (Multiplicative ℤ)) : circleEquivPontryaginDualInt.symm χ = χ (Multiplicative.ofAdd 1)

The point of the circle attached to a character of ℤ is its value at 1.