Module

FiniteBidual.lean

Nyll.ProCGroups.Abelian.FiniteBidual

5 declarations indexed from sourceView source ↗

Module documentation

The actual evaluation map into the Pontryagin double dual

Evaluation is continuous for compact groups. For finite discrete abelian groups it is an isomorphism: finite character separation gives injectivity, and the finite dual cardinality theorem gives surjectivity.

Imports3

Nyll.ProCGroups.Duality
Mathlib.Topology.Algebra.PontryaginDual
Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Imported by2

def

bidualEvaluation

L28 ↗

ProCGroups.Duality.bidualEvaluation

Documentation

Evaluation of actual circle-valued continuous characters.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u
variable (G : Type u) [CommGroup G] [TopologicalSpace G] [CompactSpace G]

Lean source · full declaration

def bidualEvaluation : G →ₜ* PontryaginDual (PontryaginDual G) where
  toFun g :=
    { toFun := fun χ => χ g
      map_one' := rfl
      map_mul' _ _ := rfl
      continuous_toFun := continuous_of_discreteTopology }
  map_one' := PontryaginDual.ext fun χ => map_one χ
  map_mul' g h := PontryaginDual.ext fun χ => map_mul χ g h
  continuous_toFun := by
    apply ContinuousMonoidHom.continuous_of_continuous_uncurry
    exact (continuous_eval : Continuous
      (fun p : (G →ₜ* Circle) × G => p.1 p.2)).comp continuous_swap

theorem

bidualEvaluation_apply

L42 ↗

ProCGroups.Duality.bidualEvaluation_apply

Documentation

Evaluation on a character is its value at the original group element.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u
variable (G : Type u) [CommGroup G] [TopologicalSpace G] [CompactSpace G]

Lean source · statement

theorem bidualEvaluation_apply (g : G) (χ : PontryaginDual G) :
    bidualEvaluation G g χ = χ g

theorem

finite_characters_separate

L49 ↗

ProCGroups.Duality.finite_characters_separate

Documentation

Finite circle-valued characters separate group elements.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u
variable (G : Type u) [CommGroup G] [TopologicalSpace G] [CompactSpace G]
variable [Finite G] [DiscreteTopology G]
omit [CompactSpace G] in

Lean source · statement

theorem finite_characters_separate {x y : G}
    (h : ∀ χ : PontryaginDual G, χ x = χ y) : x = y

theorem

finite_bidualEvaluation_bijective

L66 ↗

ProCGroups.Duality.finite_bidualEvaluation_bijective

Documentation

The actual evaluation map for a finite discrete abelian group is bijective.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u
variable (G : Type u) [CommGroup G] [TopologicalSpace G] [CompactSpace G]
variable [Finite G] [DiscreteTopology G]

Lean source · statement

theorem finite_bidualEvaluation_bijective : Function.Bijective (bidualEvaluation G)

def

finiteBidualEquiv

L76 ↗

ProCGroups.Duality.finiteBidualEquiv

Documentation

A finite discrete abelian group is canonically its actual Pontryagin double dual.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups.Duality
universe u
variable (G : Type u) [CommGroup G] [TopologicalSpace G] [CompactSpace G]
variable [Finite G] [DiscreteTopology G]

Lean source · full declaration

def finiteBidualEquiv : G ≃ₜ* PontryaginDual (PontryaginDual G) where
  toMulEquiv := MulEquiv.ofBijective (bidualEvaluation G).toMonoidHom
    (finite_bidualEvaluation_bijective G)
  continuous_toFun := (bidualEvaluation G).continuous
  continuous_invFun := continuous_of_discreteTopology

Module documentation

The actual evaluation map into the Pontryagin double dual

Declarations

bidualEvaluation

bidualEvaluation_apply

finite_characters_separate

finite_bidualEvaluation_bijective

finiteBidualEquiv