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 homomorphismsA →* Circle
.
Equations
- instTopologicalSpacePontryaginDual A = inferInstance
Equations
- instCommGroupPontryaginDual A = inferInstance
Equations
- instInhabitedPontryaginDual A = inferInstance
instance
instLocallyCompactSpacePontryaginDual
(H : Type u_5)
[Group H]
[TopologicalSpace H]
[TopologicalGroup H]
[LocallyCompactSpace H]
:
instance
PontryaginDual.instFunLikeCircle
{A : Type u_1}
[Monoid A]
[TopologicalSpace A]
:
FunLike (PontryaginDual A) A Circle
Equations
- PontryaginDual.instFunLikeCircle = ContinuousMonoidHom.instFunLike
noncomputable def
PontryaginDual.map
{A : Type u_1}
{B : Type u_2}
[Monoid A]
[Monoid B]
[TopologicalSpace A]
[TopologicalSpace B]
(f : ContinuousMonoidHom A B)
:
PontryaginDual
is a contravariant functor.
Equations
Instances For
@[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]
:
@[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.dual
as a ContinuousMonoidHom
.
Equations
- PontryaginDual.mapHom A G = { toFun := PontryaginDual.map, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }