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 PontryaginDual.instFunLikeSubtypeComplexMemSubmonoidCircle {A : Type u_1} [Monoid A] [TopologicalSpace A] : FunLike (PontryaginDual A) A ↥circle

Equations

• PontryaginDual.instFunLikeSubtypeComplexMemSubmonoidCircle = ContinuousMonoidHom.funLike

noncomputable instance PontryaginDual.instContinuousMonoidHomClassSubtypeComplexMemSubmonoidCircle {A : Type u_1} [Monoid A] [TopologicalSpace A] : ContinuousMonoidHomClass (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} {E : Type u_5} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom A E) : PontryaginDual.map (f * g) = PontryaginDual.map f * PontryaginDual.map g

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

ContinuousMonoidHom.dual as a ContinuousMonoidHom.

Equations

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