Character modules of finite abelian groups

The characters CharacterModule M = M →+ AddCircle (1 : ℚ) of an abelian group M separate its points, and when M is finite its character module is finite with as many elements as M:

• TauCeti.CharacterModule.eval_injective: evaluation embeds M in its double character module;
• an instance Finite (CharacterModule M) for finite M;
• TauCeti.natCard_characterModule: Nat.card (CharacterModule M) = Nat.card M.

A finite-order element can moreover be detected by a single character with a prescribed value:

• TauCeti.CharacterModule.ofSpanSingleton_apply_self: Mathlib's canonical character of the cyclic subgroup generated by a takes a to 1 / addOrderOf a;
• TauCeti.CharacterModule.exists_apply_eq_inv_addOrderOf: some character of the whole group takes a to 1 / addOrderOf a.

instance TauCeti.instFiniteCharacterModule_tauCeti (M : Type u_1) [AddCommGroup M] [Finite M] : Finite (CharacterModule M)

The character module of a finite abelian group is finite.

theorem TauCeti.CharacterModule.eval_injective (M : Type u_1) [AddCommGroup M] : Function.Injective ⇑AddMonoidHom.eval

Evaluation m ↦ (c ↦ c m), Mathlib's AddMonoidHom.eval, embeds an abelian group in its double character module: the characters of M separate its points.

@[simp]

theorem TauCeti.natCard_characterModule (M : Type u_1) [AddCommGroup M] [Finite M] : Nat.card (CharacterModule M) = Nat.card M

The cardinality of the character module equals the cardinality of the group.

theorem TauCeti.CharacterModule.ofSpanSingleton_apply_self {A : Type u_1} [AddCommGroup A] (a : A) (ha : addOrderOf a ≠ 0) : (CharacterModule.ofSpanSingleton a) ⟨a, ⋯⟩ = ↑(1 / ↑(addOrderOf a))

Mathlib's canonical character CharacterModule.ofSpanSingleton a of the cyclic subgroup generated by a finite-order element a takes a to the reciprocal of its additive order in ℚ / ℤ.

theorem TauCeti.CharacterModule.exists_apply_eq_inv_addOrderOf {A : Type u_1} [AddCommGroup A] (a : A) (ha : addOrderOf a ≠ 0) : ∃ (χ : CharacterModule A), χ a = ↑(1 / ↑(addOrderOf a))

A finite-order element of an abelian group admits a character taking it to the reciprocal of its additive order in ℚ / ℤ.