Documentation

Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Pontryagin duality for finite abelian groups #

This file proves the Pontryagin duality in case of finite abelian groups. This states that any finite abelian group is canonically isomorphic to its double dual (the space of complex-valued characters of its space of complex-valued characters).

We first prove it for ZMod n and then extend to all finite abelian groups using the Structure Theorem.

TODO #

Reuse the work done in Mathlib.GroupTheory.FiniteAbelian.Duality. This requires to write some more glue.

source
def AddChar.zmod (n : ℕ) [NeZero n] (x : ZMod n) :
AddChar (ZMod n) Circle

Indexing of the complex characters of ZMod n. AddChar.zmod n x is the character sending y to e ^ (2 * π * i * x * y / n).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AddChar.zmod_intCast (n : ℕ) [NeZero n] (x y : ℤ) :
    (AddChar.zmod n ↑x) ↑y = Circle.exp (2 * Real.pi * (↑x * ↑y / ↑n))
    source
    @[simp]
    theorem AddChar.zmod_zero (n : ℕ) [NeZero n] :
    AddChar.zmod n 0 = 1
    source
    @[simp]
    theorem AddChar.zmod_add {n : ℕ} [NeZero n] (x y : ZMod n) :
    AddChar.zmod n (x + y) = AddChar.zmod n x * AddChar.zmod n y
    source
    theorem AddChar.zmod_injective {n : ℕ} [NeZero n] :
    Function.Injective (AddChar.zmod n)
    source
    @[simp]
    theorem AddChar.zmod_inj {n : ℕ} [NeZero n] {x y : ZMod n} :
    AddChar.zmod n x = AddChar.zmod n y ↔ x = y
    source
    def AddChar.zmodHom {n : ℕ} [NeZero n] :
    AddChar (ZMod n) (AddChar (ZMod n) Circle)

    AddChar.zmod bundled as an AddChar.

    Equations
    • AddChar.zmodHom = { toFun := AddChar.zmod n, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
    Instances For
      source
      def AddChar.circleEquivComplex {α : Type u_1} [AddCommGroup α] [Finite α] :
      AddChar α Circle ≃+ AddChar α ℂ

      The circle-valued characters of a finite abelian group are the same as its complex-valued characters.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AddChar.card_eq {α : Type u_1} [AddCommGroup α] [Fintype α] :
        Fintype.card (AddChar α ℂ) = Fintype.card α
        source
        def AddChar.zmodAddEquiv {n : ℕ} [NeZero n] :
        ZMod n ≃+ AddChar (ZMod n) ℂ

        ZMod n is (noncanonically) isomorphic to its group of characters.

        Equations
        • AddChar.zmodAddEquiv = AddEquiv.ofBijective (AddChar.circleEquivComplex.toAddMonoidHom.comp AddChar.zmodHom.toAddMonoidHom) ⋯
        Instances For
          source
          @[simp]
          theorem AddChar.zmodAddEquiv_apply {n : ℕ} [NeZero n] (x : ZMod n) :
          AddChar.zmodAddEquiv x = AddChar.circleEquivComplex (AddChar.zmod n x)
          source
          def AddChar.complexBasis (α : Type u_1) [AddCommGroup α] [Finite α] :
          Basis (AddChar α ℂ) ℂ (α → ℂ)

          Complex-valued characters of a finite abelian group α form a basis of α → ℂ.

          Equations
          Instances For
            source
            @[simp]
            theorem AddChar.coe_complexBasis (α : Type u_1) [AddCommGroup α] [Finite α] :
            ⇑(AddChar.complexBasis α) = DFunLike.coe
            source
            @[simp]
            theorem AddChar.complexBasis_apply {α : Type u_1} [AddCommGroup α] [Finite α] (ψ : AddChar α ℂ) :
            (AddChar.complexBasis α) ψ = ⇑ψ
            source
            theorem AddChar.exists_apply_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
            (∃ (ψ : AddChar α ℂ), ψ a ≠ 1) ↔ a ≠ 0
            source
            theorem AddChar.forall_apply_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
            (∀ (ψ : AddChar α ℂ), ψ a = 1) ↔ a = 0
            source
            theorem AddChar.doubleDualEmb_injective {α : Type u_1} [AddCommGroup α] [Finite α] :
            Function.Injective ⇑AddChar.doubleDualEmb
            source
            theorem AddChar.doubleDualEmb_bijective {α : Type u_1} [AddCommGroup α] [Finite α] :
            Function.Bijective ⇑AddChar.doubleDualEmb
            source
            @[simp]
            theorem AddChar.doubleDualEmb_inj {α : Type u_1} [AddCommGroup α] {a b : α} [Finite α] :
            AddChar.doubleDualEmb a = AddChar.doubleDualEmb b ↔ a = b
            source
            @[simp]
            theorem AddChar.doubleDualEmb_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
            AddChar.doubleDualEmb a = 0 ↔ a = 0
            source
            theorem AddChar.doubleDualEmb_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
            AddChar.doubleDualEmb a ≠ 0 ↔ a ≠ 0
            source
            def AddChar.doubleDualEquiv {α : Type u_1} [AddCommGroup α] [Finite α] :
            α ≃+ AddChar (AddChar α ℂ) ℂ

            The double dual isomorphism of a finite abelian group.

            Equations
            Instances For
              source
              @[simp]
              theorem AddChar.coe_doubleDualEquiv {α : Type u_1} [AddCommGroup α] [Finite α] :
              ⇑AddChar.doubleDualEquiv = ⇑AddChar.doubleDualEmb
              source
              @[simp]
              theorem AddChar.doubleDualEmb_doubleDualEquiv_symm_apply {α : Type u_1} [AddCommGroup α] [Finite α] (a : AddChar (AddChar α ℂ) ℂ) :
              AddChar.doubleDualEmb (AddChar.doubleDualEquiv.symm a) = a
              source
              @[simp]
              theorem AddChar.doubleDualEquiv_symm_doubleDualEmb_apply {α : Type u_1} [AddCommGroup α] [Finite α] (a : AddChar (AddChar α ℂ) ℂ) :
              AddChar.doubleDualEquiv.symm (AddChar.doubleDualEmb a) = a
              source
              theorem AddChar.sum_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (a : α) :
              ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then ↑(Fintype.card α) else 0
              source
              theorem AddChar.expect_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (a : α) :
              (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) = if a = 0 then 1 else 0
              source
              theorem AddChar.sum_apply_eq_zero_iff_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
              ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0
              source
              theorem AddChar.sum_apply_ne_zero_iff_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
              ∑ ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0
              source
              theorem AddChar.expect_apply_eq_zero_iff_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
              (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) = 0 ↔ a ≠ 0
              source
              theorem AddChar.expect_apply_ne_zero_iff_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] :
              (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) ≠ 0 ↔ a = 0