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.

@[simp]

theorem AddChar.zmodAuxAux_apply (n : ℕ) (z : ℤ) : (AddChar.zmodAuxAux n) z = Additive.ofMul (Circle.e (↑z / ↑n))

@[simp]

theorem AddChar.aux (n : ℕ) (h : (AddChar.zmodAuxAux n) ↑n = 0) : ↑{ val := AddChar.zmodAuxAux n, property := h } = AddChar.zmodAuxAux n

@[simp]

theorem AddChar.zmodAux_apply (n : ℕ) (z : ℤ) : (AddChar.zmodAux n) ↑z = Circle.e (↑z / ↑n)

theorem AddChar.zmodAux_injective {n : ℕ} (hn : n ≠ 0) : Function.Injective ⇑(AddChar.zmodAux n)

def AddChar.zmod (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

• AddChar.zmod n x = AddChar.compAddMonoidHom (AddChar.zmodAux n) (AddMonoidHom.mulLeft x)

@[simp]

theorem AddChar.zmod_apply (n : ℕ) (x : ℤ) (y : ℤ) : (AddChar.zmod n ↑x) ↑y = Circle.e (↑x * ↑y / ↑n)

@[simp]

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

@[simp]

theorem AddChar.zmod_add (n : ℕ) (x : ZMod n) (y : ZMod n) : AddChar.zmod n (x + y) = AddChar.zmod n x * AddChar.zmod n y

theorem AddChar.zmod_injective {n : ℕ} (hn : n ≠ 0) : Function.Injective (AddChar.zmod n)

@[simp]

theorem AddChar.zmod_inj {n : ℕ} (hn : n ≠ 0) {x : ZMod n} {y : ZMod n} : AddChar.zmod n x = AddChar.zmod n y ↔ x = y

def AddChar.zmodHom (n : ℕ) : AddChar (ZMod n) (AddChar (ZMod n) ↥circle)

Equations

• AddChar.zmodHom n = { toFun := AddChar.zmod n, map_zero_one' := ⋯, map_add_mul' := ⋯ }

def AddChar.mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : (i : ι) → ZMod (n i)) : AddChar (DirectSum ι fun (i : ι) => ZMod (n i)) ↥circle

Equations

• AddChar.mkZModAux n u = AddChar.directSum fun (i : ι) => AddChar.zmod (n i) (u i)

theorem AddChar.mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} (hn : ∀ (i : ι), n i ≠ 0) : Function.Injective (AddChar.mkZModAux n)

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 α

def AddChar.zmodAddEquiv {n : ℕ} (hn : n ≠ 0) : ZMod n ≃+ AddChar (ZMod n) ℂ

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

Equations

• AddChar.zmodAddEquiv hn = AddEquiv.ofBijective (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddChar.circleEquivComplex) (AddChar.toAddMonoidHom (AddChar.zmodHom n))) ⋯

@[simp]

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

def AddChar.complexBasis (α : Type u_1) [AddCommGroup α] [Finite α] : 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 α] : ⇑(AddChar.complexBasis α) = DFunLike.coe

@[simp]

theorem AddChar.complexBasis_apply {α : Type u_1} [AddCommGroup α] [Finite α] (ψ : AddChar α ℂ) : (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 ⇑AddChar.doubleDualEmb

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

@[simp]

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

@[simp]

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

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

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

The double dual isomorphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem AddChar.sum_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (a : α) : (Finset.sum Finset.univ fun (ψ : AddChar α ℂ) => ψ a) = if a = 0 then ↑(Fintype.card α) else 0

theorem AddChar.expect_apply_eq_ite {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (a : α) : (Finset.expect Finset.univ 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 α] : (Finset.sum Finset.univ fun (ψ : AddChar α ℂ) => ψ a) = 0 ↔ a ≠ 0

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

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

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