Documentation

Mathlib.Topology.Algebra.PontryaginDual

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 #

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
Instances For
    noncomputable instance instCommGroupPontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] :
    Equations
    noncomputable instance instInhabitedPontryaginDual (A : Type u_1) [Monoid A] [TopologicalSpace A] :
    Equations
    Equations
    • PontryaginDual.instFunLikeCircle = ContinuousMonoidHom.instFunLike

    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)

      ContinuousMonoidHom.dual as a ContinuousMonoidHom.

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