Characters for the cyclotomic input to global class field theory

Let q > 1 and N > 0, and put m = q ^ N - 1. The class of q in (ZMod m)ˣ has exact order N (TauCeti.ZMod.orderOf_unitOfCoprime_pow_sub_one). Consequently there is an additive character of (ZMod m)ˣ taking q to 1 / N in ℚ / ℤ. Composing this character with the action on a primitive m-th root of unity gives a character of a cyclotomic Galois group with the same prescribed value.

These are the finite-group ingredients in the cyclotomic construction used to produce an idele class of invariant 1 / N: at a finite place with residue cardinality q, arithmetic Frobenius acts on the m-th roots of unity as the q-th power. The global carry class attached to the resulting character therefore has local invariant 1 / N at a uniformizer of that place.

Main results

• CharacterModule.exists_apply_unitOfCoprime_pow_sub_one: a character of (ZMod (q ^ N - 1))ˣ takes q to 1 / N; it is obtained from the general TauCeti.CharacterModule.exists_apply_eq_inv_addOrderOf.
• IsPrimitiveRoot.exists_character_autToPow_apply: the corresponding character on a cyclotomic Galois group.

References

• J. S. Milne, Class Field Theory, Chapter VII, Lemma 7.3.

theorem TauCeti.CharacterModule.exists_apply_unitOfCoprime_pow_sub_one (q N : ℕ) (hq : 1 < q) (hN : N ≠ 0) : ∃ (χ : CharacterModule (Additive (ZMod (q ^ N - 1))ˣ)), χ (Additive.ofMul (ZMod.unitOfCoprime q ⋯)) = ↑(1 / ↑N)

If q > 1 and N > 0, there is a character of (ZMod (q ^ N - 1))ˣ taking the class of q to 1 / N.

theorem IsPrimitiveRoot.exists_character_autToPow_apply {K : Type u_1} {E : Type u_2} [CommRing K] [CommRing E] [IsDomain E] [Algebra K E] {q N : ℕ} (hq : 1 < q) (hN : N ≠ 0) {ζ : E} (hζ : IsPrimitiveRoot ζ (q ^ N - 1)) : ∃ (χ : Additive (E ≃ₐ[K] E) →+ AddCircle 1), ∀ (σ : E ≃ₐ[K] E), ζ ^ q = σ ζ → χ (Additive.ofMul σ) = ↑(1 / ↑N)

The prescribed cyclotomic character. Let ζ be a primitive (q ^ N - 1)-th root of unity in an extension E/K. There is a character of Aut(E/K) taking every automorphism acting on ζ by the q-th power to 1 / N.

At a finite place of residue cardinality q, this hypothesis is precisely the arithmetic Frobenius action on roots of unity.