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.

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

@[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

noncomputable 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' := ⋯ }

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.

@[simp]

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

noncomputable 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) ⋯

@[simp]

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

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

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

Equations

• AddChar.complexBasis α = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[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

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

The double dual isomorphism of a finite abelian group.

Equations

• AddChar.doubleDualEquiv = AddEquiv.ofBijective AddChar.doubleDualEmb ⋯

@[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