Pontryagin dual

This file defines the Pontryagin dual of a topological group. The Pontryagin dual of a topological group A is the topological group of continuous homomorphisms A →* Circle with the compact-open topology. For example, ℤ and Circle are Pontryagin duals of each other. This is an example of Pontryagin duality, which states that a locally compact abelian topological group is canonically isomorphic to its double dual.

Main definitions

• PontryaginDual A: The group of continuous homomorphisms A →* Circle.

def PontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : Type u_1

The Pontryagin dual of A is the group of continuous homomorphism A → Circle.

instance instTopologicalSpacePontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : TopologicalSpace (PontryaginDual A)

instance instT2SpacePontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : T2Space (PontryaginDual A)

noncomputable instance instCommGroupPontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : CommGroup (PontryaginDual A)

instance instIsTopologicalGroupPontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : IsTopologicalGroup (PontryaginDual A)

noncomputable instance instInhabitedPontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] : Inhabited (PontryaginDual A)

instance instLocallyCompactSpacePontryaginDual (H : Type u_5) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace H] : LocallyCompactSpace (PontryaginDual H)

instance PontryaginDual.instFunLikeCircle {A : Type u_1} [Monoid A] [TopologicalSpace A] : FunLike (PontryaginDual A) A Circle

instance PontryaginDual.instContinuousMapClass {A : Type u_1} [Monoid A] [TopologicalSpace A] : ContinuousMapClass (PontryaginDual A) A Circle

instance PontryaginDual.instMonoidHomClass {A : Type u_1} [Monoid A] [TopologicalSpace A] : MonoidHomClass (PontryaginDual A) A Circle

instance PontryaginDual.instCompactSpaceOfDiscreteTopology {A : Type u_1} [Monoid A] [TopologicalSpace A] [DiscreteTopology A] : CompactSpace (PontryaginDual A)

A discrete monoid has compact Pontryagin dual.

noncomputable def PontryaginDual.map {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) : PontryaginDual B →ₜ* PontryaginDual A

PontryaginDual is a contravariant functor.

@[simp]

theorem PontryaginDual.map_apply {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →ₜ* B) (x : PontryaginDual B) (y : A) : ((map f) x) y = x (f y)

@[simp]

theorem PontryaginDual.map_one {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : map 1 = 1

@[simp]

theorem PontryaginDual.map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B) : map (g.comp f) = (map f).comp (map g)

@[simp]

theorem PontryaginDual.map_mul {A : Type u_1} {G : Type u_4} [Monoid A] [CommGroup G] [TopologicalSpace A] [TopologicalSpace G] [IsTopologicalGroup G] (f g : A →ₜ* G) : map (f * g) = map f * map g

noncomputable def PontryaginDual.mapHom (A : Type u_1) (G : Type u_4) [Monoid A] [CommGroup G] [TopologicalSpace A] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] : (A →ₜ* G) →ₜ* PontryaginDual G →ₜ* PontryaginDual A

ContinuousMonoidHom.dual as a ContinuousMonoidHom.