Units of ℤ/p as a direct product in arithmetic progression (Anderson–Cameron–Preece)

For a prime p = 6m + 1, m > 1, the unit group of ℤ/p is an internal direct product of cyclic subgroups generated by x, x + k, x + 2k with orders 2, 3, m in some order if and only if m ≡ 1, 5 (mod 6) and some root α of X² + 3X + 3 has order m, or α/2 has order m, or α has order p − 1 and the other root order (p − 1)/2 (Theorem of the Day; Cameron and Preece). The root must be quantified existentially: with a fixed labelling the statement fails at p = 31. Proof: α + 1 has order 3, and with t = 2α + 3, α = −(α+1)² t, t² = −3; the arithmetic-progression condition fixes the order-m generator in each of the six placements.

Main results

• ACP.internal_of_coprime: pairwise coprime orders with product p − 1 give an internal direct product
• ACP.classification: Anderson–Cameron–Preece classification (∃ root)

References

• R. Whitty, Theorem of the Day, «A Theorem of Anderson, Cameron and Preece on Groups of Units» (NumberTheory/ZnUnits).
• P. J. Cameron, D. A. Preece, arXiv:1111.3507, §2; I. Anderson, D. A. Preece, INTEGERS 12 (2012) A52.

def ACP.Internal3 {G : Type u_1} [CommGroup G] (u v w : G) : Prop

u, v, w give an internal direct product decomposition G = ⟨u⟩ × ⟨v⟩ × ⟨w⟩.

Equations

• ACP.Internal3 u v w = Function.Bijective fun (t : ↥(Subgroup.zpowers u) × ↥(Subgroup.zpowers v) × ↥(Subgroup.zpowers w)) => ↑t.1 * ↑t.2.1 * ↑t.2.2

Part 1: pairwise coprime orders with product |G|

theorem ACP.ord_mul {G : Type u_1} [CommMonoid G] {x y : G} (h : (orderOf x).Coprime (orderOf y)) : orderOf (x * y) = orderOf x * orderOf y

theorem ACP.internal_of_coprime {G : Type u_1} [CommGroup G] [Finite G] (u v w : G) (huv : (orderOf u).Coprime (orderOf v)) (huw : (orderOf u).Coprime (orderOf w)) (hvw : (orderOf v).Coprime (orderOf w)) (h : orderOf u * orderOf v * orderOf w = Nat.card G) : Internal3 u v w

Pairwise coprime orders whose product is |G| give an internal direct product.

theorem ACP.Internal3.disj_uv {G : Type u_1} [CommGroup G] {u v w : G} (h : Internal3 u v w) : Disjoint (Subgroup.zpowers u) (Subgroup.zpowers v)

Injectivity: ⟨u⟩ ∩ ⟨v⟩ is trivial.

theorem ACP.Internal3.disj_uw {G : Type u_1} [CommGroup G] {u v w : G} (h : Internal3 u v w) : Disjoint (Subgroup.zpowers u) (Subgroup.zpowers w)

Injectivity: ⟨u⟩ ∩ ⟨w⟩ is trivial.

theorem ACP.Internal3.disj_vw {G : Type u_1} [CommGroup G] {u v w : G} (h : Internal3 u v w) : Disjoint (Subgroup.zpowers v) (Subgroup.zpowers w)

Injectivity: ⟨v⟩ ∩ ⟨w⟩ is trivial.

Part 2: small orders in a field

theorem ACP.coprime6_iff {m : ℕ} : m.Coprime 6 ↔ m % 6 = 1 ∨ m % 6 = 5

theorem ACP.perm_cases {a b c m : ℕ} (h : [a, b, c].Perm [2, 3, m]) : a = 2 ∧ b = 3 ∧ c = m ∨ a = 2 ∧ b = m ∧ c = 3 ∨ a = 3 ∧ b = 2 ∧ c = m ∨ a = 3 ∧ b = m ∧ c = 2 ∨ a = m ∧ b = 2 ∧ c = 3 ∨ a = m ∧ b = 3 ∧ c = 2

theorem ACP.eq_neg_one_of_orderOf_two {K : Type u_1} [Field K] {y : K} (h : orderOf y = 2) : y = -1

theorem ACP.orderOf_neg_one_two {K : Type u_1} [Field K] (h2 : 2 ≠ 0) : orderOf (-1) = 2

theorem ACP.cube_of_orderOf_three {K : Type u_1} [Field K] {y : K} (h : orderOf y = 3) : y ^ 2 + y + 1 = 0

theorem ACP.orderOf_three_of_cube {K : Type u_1} [Field K] (h3 : 3 ≠ 0) {y : K} (h : y ^ 2 + y + 1 = 0) : orderOf y = 3

theorem ACP.units_eq_of_orderOf_two {K : Type u_1} [Field K] {x y : Kˣ} (hx : orderOf x = 2) (hy : orderOf y = 2) : x = y

theorem ACP.mem_zpowers_of_orderOf_three {K : Type u_1} [Field K] {x y : Kˣ} (hx : orderOf x = 3) (hy : orderOf y = 3) : y ∈ Subgroup.zpowers x

theorem ACP.coprime6_of_disjoint {K : Type u_1} [Field K] {m : ℕ} (hm : 0 < m) {a b c : Kˣ} (ha : orderOf a = 2) (hb : orderOf b = 3) (hc : orderOf c = m) (dac : Disjoint (Subgroup.zpowers a) (Subgroup.zpowers c)) (dbc : Disjoint (Subgroup.zpowers b) (Subgroup.zpowers c)) : m.Coprime 6

Disjoint cyclic factors of orders 2, 3 and m force gcd (m, 6) = 1.

Part 3: the lemma ord t = m ↔ ord α = 6m ∧ ord β = 3m

theorem ACP.lemma3_aux {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {m : ℕ} (hm : 0 < m) (hcop : m.Coprime 6) {ω t : K} (hω : ω ^ 2 + ω + 1 = 0) : orderOf t = m ↔ orderOf (-ω ^ 2 * t) = 6 * m ∧ orderOf (ω * t) = 3 * m

theorem ACP.lemma3 {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {m : ℕ} (hm : 0 < m) (hcop : m.Coprime 6) {α : K} (hα : α ^ 2 + 3 * α + 3 = 0) : orderOf (2 * α + 3) = m ↔ orderOf α = 6 * m ∧ orderOf (-α - 3) = 3 * m

Part 4: necessity

theorem ACP.nec_core {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {m : ℕ} (hm : 0 < m) {a b c : Kˣ} (ha : orderOf a = 2) (hb : orderOf b = 3) (hc : orderOf c = m) (dac : Disjoint (Subgroup.zpowers a) (Subgroup.zpowers c)) (dbc : Disjoint (Subgroup.zpowers b) (Subgroup.zpowers c)) (hap : ↑a + ↑c = 2 * ↑b ∨ ↑a + ↑b = 2 * ↑c ∨ ↑b + ↑c = 2 * ↑a) : m.Coprime 6 ∧ ∃ (α : K), α ^ 2 + 3 * α + 3 = 0 ∧ (orderOf α = m ∨ orderOf (α / 2) = m ∨ orderOf α = 6 * m ∧ orderOf (-α - 3) = 3 * m)

theorem ACP.two_ne_zero_zmod {p m : ℕ} [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (hm : 1 < m) : 2 ≠ 0

theorem ACP.three_ne_zero_zmod {p m : ℕ} [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (hm : 1 < m) : 3 ≠ 0

theorem ACP.necessity (p m : ℕ) [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (hm : 1 < m) : (∃ (u : (ZMod p)ˣ) (v : (ZMod p)ˣ) (w : (ZMod p)ˣ), ↑u + ↑w = 2 * ↑v ∧ [orderOf u, orderOf v, orderOf w].Perm [2, 3, m] ∧ Internal3 u v w) → (m % 6 = 1 ∨ m % 6 = 5) ∧ ∃ (α : ZMod p), α ^ 2 + 3 * α + 3 = 0 ∧ (orderOf α = m ∨ orderOf (α / 2) = m ∨ orderOf α = p - 1 ∧ orderOf (-α - 3) = (p - 1) / 2)

Part 5: sufficiency

theorem ACP.suff_core {p m : ℕ} [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (a b c : ZMod p) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hap : a + c = 2 * b) {o1 o2 o3 : ℕ} (h1 : orderOf a = o1) (h2 : orderOf b = o2) (h3 : orderOf c = o3) (c12 : o1.Coprime o2) (c13 : o1.Coprime o3) (c23 : o2.Coprime o3) (hprod : o1 * o2 * o3 = 6 * m) (hperm : [o1, o2, o3].Perm [2, 3, m]) : ∃ (u : (ZMod p)ˣ) (v : (ZMod p)ˣ) (w : (ZMod p)ˣ), ↑u + ↑w = 2 * ↑v ∧ [orderOf u, orderOf v, orderOf w].Perm [2, 3, m] ∧ Internal3 u v w

theorem ACP.sufficiency (p m : ℕ) [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (hm : 1 < m) : ((m % 6 = 1 ∨ m % 6 = 5) ∧ ∃ (α : ZMod p), α ^ 2 + 3 * α + 3 = 0 ∧ (orderOf α = m ∨ orderOf (α / 2) = m ∨ orderOf α = p - 1 ∧ orderOf (-α - 3) = (p - 1) / 2)) → ∃ (u : (ZMod p)ˣ) (v : (ZMod p)ˣ) (w : (ZMod p)ˣ), ↑u + ↑w = 2 * ↑v ∧ [orderOf u, orderOf v, orderOf w].Perm [2, 3, m] ∧ Internal3 u v w

theorem ACP.classification (p m : ℕ) [Fact (Nat.Prime p)] (hp : p = 6 * m + 1) (hm : 1 < m) : (∃ (u : (ZMod p)ˣ) (v : (ZMod p)ˣ) (w : (ZMod p)ˣ), ↑u + ↑w = 2 * ↑v ∧ [orderOf u, orderOf v, orderOf w].Perm [2, 3, m] ∧ Internal3 u v w) ↔ (m % 6 = 1 ∨ m % 6 = 5) ∧ ∃ (α : ZMod p), α ^ 2 + 3 * α + 3 = 0 ∧ (orderOf α = m ∨ orderOf (α / 2) = m ∨ orderOf α = p - 1 ∧ orderOf (-α - 3) = (p - 1) / 2)

Anderson–Cameron–Preece. Let p = 6m + 1 be prime, m > 1. The unit group of ℤ/p is an internal direct product ⟨x⟩ × ⟨x + k⟩ × ⟨x + 2k⟩ of cyclic subgroups whose generators are in arithmetic progression and have orders 2, 3, m in some order, if and only if m ≡ 1 or 5 (mod 6) and some root α of X² + 3X + 3 satisfies ord α = m, or ord (α/2) = m, or ord α = p − 1 and ord β = (p − 1)/2 for the other root β = −α − 3.