Characters of units modulo powers of two

The unit group modulo 2^(n+3) admits a character to ℚ/ℤ with kernel of order at most two and with nonzero value at -1. Its value on 5 has order 2^(n+1). Such a character cuts out a cyclic, totally complex subextension of a two-power cyclotomic extension.

The construction uses TauCeti.CharacterModule.exists_apply_eq_inv_addOrderOf to extend characters and ZMod.orderOf_unitFive for the kernel bound. A character modulo four ensures the nonzero value at -1.

Reference

• J. S. Milne, Class Field Theory, Chapter VII, Lemma 7.3, https://www.jmilne.org/math/CourseNotes/CFT.pdf.

theorem TauCeti.CharacterModule.exists_character_units_two_pow (n : ℕ) : ∃ (χ : Additive (ZMod (2 ^ (n + 3)))ˣ →+ AddCircle 1), χ (Additive.ofMul ZMod.unitFive) = ↑(1 / 2 ^ (n + 1)) ∧ χ (Additive.ofMul (-1)) ≠ 0 ∧ Nat.card ↥χ.ker ≤ 2

A character of the units modulo 2^(n+3) detects complex conjugation and has kernel of order at most two. Its value on 5 has order 2^(n+1).