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 = (A →ₜ* Circle)

@[instance_reducible]

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

Equations

• instTopologicalSpacePontryaginDual A = { IsOpen := instTopologicalSpacePontryaginDual._aux_1 A, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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

A discrete monoid has compact Pontryagin dual.

@[instance_reducible]

noncomputable instance PontryaginDual.instCommGroup {A : Type u_1} [Monoid A] [TopologicalSpace A] : CommGroup (PontryaginDual A)

Equations

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

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

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

instance PontryaginDual.instIsTopologicalGroup {A : Type u_1} [Monoid A] [TopologicalSpace A] : IsTopologicalGroup (PontryaginDual A)

@[instance_reducible]

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

Equations

• PontryaginDual.instFunLikeCircle = { coe := PontryaginDual.instFunLikeCircle._aux_1, coe_injective := ⋯ }

instance PontryaginDual.instT2Space {A : Type u_1} [Monoid A] [TopologicalSpace A] : T2Space (PontryaginDual A)

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

@[instance_reducible]

noncomputable instance PontryaginDual.instInhabited {A : Type u_1} [Monoid A] [TopologicalSpace A] : Inhabited (PontryaginDual A)

Equations

• PontryaginDual.instInhabited = { default := PontryaginDual.instInhabited._aux_1 }

theorem PontryaginDual.ext {A : Type u_1} [Monoid A] [TopologicalSpace A] {ψ φ : PontryaginDual A} (h : ∀ (a : A), ψ a = φ a) : ψ = φ

theorem PontryaginDual.ext_iff {A : Type u_1} [Monoid A] [TopologicalSpace A] {ψ φ : PontryaginDual A} : ψ = φ ↔ ∀ (a : A), ψ a = φ a

@[simp]

theorem PontryaginDual.one_apply {A : Type u_1} [Monoid A] [TopologicalSpace A] (a : A) : 1 a = 1

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

A compact monoid has discrete Pontryagin dual.

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

@[instance_reducible]

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

Equations

• PontryaginDual.instFintypeOfDiscreteTopologyOfCompactSpace = Fintype.ofFinite (PontryaginDual A)

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.

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 : 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.

Equations

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