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.lean. This requires to write some more glue.

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

@[simp]

theorem AddChar.zmod_intCast (n : ℕ) [NeZero n] (x y : ℤ) : (zmod n ↑x) ↑y = Circle.exp (2 * Real.pi * (↑x * ↑y / ↑n))

@[simp]

theorem AddChar.zmod_zero (n : ℕ) [NeZero n] : zmod n 0 = 1

@[simp]

theorem AddChar.zmod_add {n : ℕ} [NeZero n] (x y : ZMod n) : zmod n (x + y) = zmod n x * zmod n y

theorem AddChar.zmod_injective {n : ℕ} [NeZero n] : Function.Injective (zmod n)

@[simp]

theorem AddChar.zmod_inj {n : ℕ} [NeZero n] {x y : ZMod n} : zmod n x = zmod n y ↔ x = y

def AddChar.zmodHom {n : ℕ} [NeZero n] : AddChar (ZMod n) (AddChar (ZMod n) Circle)

AddChar.zmod bundled as an AddChar.

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.

@[simp]

theorem AddChar.card_eq {α : Type u_1} [AddCommGroup α] [Fintype α] : Fintype.card (AddChar α ℂ) = Fintype.card α

def AddChar.zmodAddEquiv {n : ℕ} [NeZero n] : ZMod n ≃+ AddChar (ZMod n) ℂ

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

@[simp]

theorem AddChar.zmodAddEquiv_apply {n : ℕ} [NeZero n] (x : ZMod n) : zmodAddEquiv x = circleEquivComplex (zmod n x)

def AddChar.complexBasis (α : Type u_1) [AddCommGroup α] [Finite α] : Module.Basis (AddChar α ℂ) ℂ (α → ℂ)

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

@[simp]

theorem AddChar.coe_complexBasis (α : Type u_1) [AddCommGroup α] [Finite α] : ⇑(complexBasis α) = DFunLike.coe

@[simp]

theorem AddChar.complexBasis_apply {α : Type u_1} [AddCommGroup α] [Finite α] (ψ : AddChar α ℂ) : (complexBasis α) ψ = ⇑ψ

theorem AddChar.exists_apply_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : (∃ (ψ : AddChar α ℂ), ψ a ≠ 1) ↔ a ≠ 0

theorem AddChar.forall_apply_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : (∀ (ψ : AddChar α ℂ), ψ a = 1) ↔ a = 0

theorem AddChar.doubleDualEmb_injective {α : Type u_1} [AddCommGroup α] [Finite α] : Function.Injective ⇑doubleDualEmb

theorem AddChar.doubleDualEmb_bijective {α : Type u_1} [AddCommGroup α] [Finite α] : Function.Bijective ⇑doubleDualEmb

@[simp]

theorem AddChar.doubleDualEmb_inj {α : Type u_1} [AddCommGroup α] {a b : α} [Finite α] : doubleDualEmb a = doubleDualEmb b ↔ a = b

@[simp]

theorem AddChar.doubleDualEmb_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : doubleDualEmb a = 0 ↔ a = 0

theorem AddChar.doubleDualEmb_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : doubleDualEmb a ≠ 0 ↔ a ≠ 0

def AddChar.doubleDualEquiv {α : Type u_1} [AddCommGroup α] [Finite α] : α ≃+ AddChar (AddChar α ℂ) ℂ

The double dual isomorphism of a finite abelian group.

@[simp]

theorem AddChar.coe_doubleDualEquiv {α : Type u_1} [AddCommGroup α] [Finite α] : ⇑doubleDualEquiv = ⇑doubleDualEmb

@[simp]

theorem AddChar.doubleDualEmb_doubleDualEquiv_symm_apply {α : Type u_1} [AddCommGroup α] [Finite α] (a : AddChar (AddChar α ℂ) ℂ) : doubleDualEmb (doubleDualEquiv.symm a) = a

@[simp]

theorem AddChar.doubleDualEquiv_symm_doubleDualEmb_apply {α : Type u_1} [AddCommGroup α] [Finite α] (a : AddChar (AddChar α ℂ) ℂ) : doubleDualEquiv.symm (doubleDualEmb a) = a

theorem AddChar.sum_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (a : α) : ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then ↑(Fintype.card α) else 0

theorem AddChar.expect_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Finite α] [DecidableEq α] (a : α) : (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) = if a = 0 then 1 else 0

theorem AddChar.sum_apply_eq_zero_iff_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0

theorem AddChar.sum_apply_ne_zero_iff_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : ∑ ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0

theorem AddChar.expect_apply_eq_zero_iff_ne_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) = 0 ↔ a ≠ 0

theorem AddChar.expect_apply_ne_zero_iff_eq_zero {α : Type u_1} [AddCommGroup α] {a : α} [Finite α] : (Finset.univ.expect fun (ψ : AddChar α ℂ) => ψ a) ≠ 0 ↔ a = 0