The units modulo a power of two

For every e, the unit group (ℤ/2^(e+2))ˣ is the internal direct product of the subgroup {±1} and the cyclic subgroup of order 2 ^ e generated by the class of 5. Concretely, TauCeti.ZMod.unitsTwoPowEquiv e is a group isomorphism (ZMod (2 ^ (e + 2)))ˣ ≃* Multiplicative (ZMod 2 × ZMod (2 ^ e)) sending -1 to (1, 0) and 5 to (0, 1); its inverse sends (s, k) to (-1) ^ s * 5 ^ k. The indexing by e + 2 encodes that the modulus is at least 4: modulo 1 and 2 there is only one unit, and modulo 4 the second factor is trivial. From the modulus 8 on, the unit group is not cyclic (ZMod.isCyclic_units_two_pow_iff).

This explicit form, rather than the bare isomorphism type, is what reads off characters of two-power level from their values at -1 and 5.

Main definitions and results

• TauCeti.ZMod.unitsMap_unitFive_eq_one: reduction modulo 4 sends ZMod.unitFive to 1.
• TauCeti.ZMod.neg_one_notMem_zpowers_unitFive: -1 is not a power of ZMod.unitFive.
• TauCeti.ZMod.unitsTwoPowEquiv: the isomorphism with ℤ/2 × ℤ/2^e.
• TauCeti.ZMod.unitsTwoPowEquiv_symm_apply, TauCeti.ZMod.unitsTwoPowEquiv_symm_ofAdd_natCast, TauCeti.ZMod.unitsTwoPowEquiv_neg_one, TauCeti.ZMod.unitsTwoPowEquiv_five: its values.

Reference

Victor Shoup, A Computational Introduction to Number Theory and Algebra (2nd ed.), Theorem 7.28 and its proof for p = 2.

@[simp]

theorem TauCeti.ZMod.unitsMap_unitFive_eq_one (e : ℕ) (h : 4 ∣ 2 ^ (e + 2)) : (ZMod.unitsMap h) ZMod.unitFive = 1

Reduction modulo 4 sends the unit 5 modulo 2 ^ (e + 2) to 1.

@[simp]

theorem TauCeti.ZMod.neg_one_notMem_zpowers_unitFive (e : ℕ) : -1 ∉ Subgroup.zpowers ZMod.unitFive

The unit -1 modulo 2 ^ (e + 2) is not a power of 5.

noncomputable def TauCeti.ZMod.unitsTwoPowEquiv (e : ℕ) : (ZMod (2 ^ (e + 2)))ˣ ≃* Multiplicative (ZMod 2 × ZMod (2 ^ e))

The units modulo 2 ^ (e + 2). The group (ℤ/2^(e+2))ˣ is isomorphic to ℤ/2 × ℤ/2^e, with -1 corresponding to (1, 0) and 5 to (0, 1). The inverse is (s, k) ↦ (-1) ^ s * 5 ^ k (unitsTwoPowEquiv_symm_apply).

@[simp]

theorem TauCeti.ZMod.unitsTwoPowEquiv_symm_apply (e : ℕ) (x : ZMod 2 × ZMod (2 ^ e)) : (unitsTwoPowEquiv e).symm (Multiplicative.ofAdd x) = (-1) ^ x.1.val * ZMod.unitFive ^ x.2.val

The inverse of ZMod.unitsTwoPowEquiv sends (s, k) to (-1) ^ s * 5 ^ k, with s and k read through their canonical representatives.

theorem TauCeti.ZMod.unitsTwoPowEquiv_symm_ofAdd_natCast (e s k : ℕ) : (unitsTwoPowEquiv e).symm (Multiplicative.ofAdd (↑s, ↑k)) = (-1) ^ s * ZMod.unitFive ^ k

The inverse of ZMod.unitsTwoPowEquiv sends the classes of natural numbers s and k to (-1) ^ s * 5 ^ k.

@[simp]

theorem TauCeti.ZMod.unitsTwoPowEquiv_neg_one (e : ℕ) : (unitsTwoPowEquiv e) (-1) = Multiplicative.ofAdd (1, 0)

ZMod.unitsTwoPowEquiv sends -1 to (1, 0).

@[simp]

theorem TauCeti.ZMod.unitsTwoPowEquiv_five (e : ℕ) : (unitsTwoPowEquiv e) ZMod.unitFive = Multiplicative.ofAdd (0, 1)

ZMod.unitsTwoPowEquiv sends 5 to (0, 1).

Examples