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.

Equations

• PontryaginDual A = ContinuousMonoidHom A Circle

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

Equations

• instTopologicalSpacePontryaginDual A = inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• instCommGroupPontryaginDual A = inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• instInhabitedPontryaginDual A = inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• PontryaginDual.instFunLikeCircle = ContinuousMonoidHom.instFunLike

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

PontryaginDual is a contravariant functor.

Equations

• PontryaginDual.map f = ContinuousMonoidHom.compLeft Circle f

@[simp]

theorem PontryaginDual.map_apply {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousMonoidHom A B) (x : PontryaginDual B) (y : A) : ((PontryaginDual.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] : PontryaginDual.map (ContinuousMonoidHom.one A B) = ContinuousMonoidHom.one (PontryaginDual B) (PontryaginDual A)

@[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 : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : PontryaginDual.map (g.comp f) = (PontryaginDual.map f).comp (PontryaginDual.map g)

@[simp]

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

noncomputable def PontryaginDual.mapHom (A : Type u_1) (G : Type u_4) [Monoid A] [CommGroup G] [TopologicalSpace A] [TopologicalSpace G] [TopologicalGroup G] [LocallyCompactSpace G] : ContinuousMonoidHom (ContinuousMonoidHom A G) (ContinuousMonoidHom (PontryaginDual G) (PontryaginDual A))

ContinuousMonoidHom.dual as a ContinuousMonoidHom.

Equations

• PontryaginDual.mapHom A G = { toFun := PontryaginDual.map, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }