Primitive roots modulo prime powers

DefinitionMultiplicative order modulo \(n\)#✓fully proved

For natural numbers \(n\) and \(a\), \(\operatorname{ord}_n(a)\) is the multiplicative order of the residue class of \(a\) in the unit group \((\mathbb{Z}/n\mathbb{Z})^\times\) when \(a\) is coprime to \(n\), and \(0\) otherwise.

noncomputable def mulOrdMod (n a : ℕ) : ℕ :=
  if h : Nat.Coprime a n then orderOf (ZMod.unitOfCoprime a h) else 0

Used by 2

Used byUnique order-preserving lift modulo \(p^2\) · The order of \(a + kp\) modulo \(p^2\)

DefinitionReduction of units modulo \(p^2\) to units modulo \(p\)#✓fully proved

For a natural number \(p\), this is the group homomorphism \((\mathbb{Z}/p^2\mathbb{Z})^\times \to (\mathbb{Z}/p\mathbb{Z})^\times\) induced on units by the reduction ring homomorphism \(\mathbb{Z}/p^2\mathbb{Z} \to \mathbb{Z}/p\mathbb{Z}\), which sends the class of \(x\) modulo \(p^2\) to the class of \(x\) modulo \(p\).

def unitReduceSq (p : ℕ) : (ZMod (p ^ 2))ˣ →* (ZMod p)ˣ :=
  Units.map (ZMod.castHom (⟨p, by ring⟩ : p ∣ p ^ 2) (ZMod p)).toMonoidHom

Used by 2

Used byUnique order-preserving element of a fiber modulo \(p^2\) · Fibers of reduction modulo \(p\) on units modulo \(p^2\)

DefinitionFibers of reduction modulo \(p\) on units modulo \(p^2\)#✓fully proved

For a natural number \(p\) and a unit \(a\) of \(\mathbb{Z}/p^2\mathbb{Z}\), the fiber \(P_a\) is the set of units \(x\) of \(\mathbb{Z}/p^2\mathbb{Z}\) with \(x \equiv a \pmod p\), that is, the units whose image under the reduction map \((\mathbb{Z}/p^2\mathbb{Z})^\times \to (\mathbb{Z}/p\mathbb{Z})^\times\) equals the image of \(a\).

def liftFiber (p : ℕ) (a : (ZMod (p ^ 2))ˣ) : Set (ZMod (p ^ 2))ˣ :=
  {x | unitReduceSq p x = unitReduceSq p a}

Uses 1 · Used by 4

Statement usesReduction of units modulo \(p^2\) to units modulo \(p\)

Used byUnique order-preserving element of a fiber modulo \(p^2\) · The lift of order \(p - 1\) of a primitive root · Endomorphisms of the units modulo \(p^2\) respect the fibers · Power maps on the fibers modulo \(p^2\)

TheoremThe order of \(a + kp\) modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime and let \(a\) and \(k\) be natural numbers with \(a\) coprime to \(p\). Writing \(\operatorname{ord}_n(b)\) for the multiplicative order of \(b\) modulo \(n\), the order \(\operatorname{ord}_{p^2}(a + kp)\) is either \(\operatorname{ord}_p(a)\) or \(p \cdot \operatorname{ord}_p(a)\).

theorem_wanted order_add_mul_prime_eq_or_mul
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (a k : ℕ)
    (ha : Nat.Coprime a p) :
    mulOrdMod (p ^ 2) (a + k * p) = mulOrdMod p a ∨
      mulOrdMod (p ^ 2) (a + k * p) = p * mulOrdMod p a

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Lemma 1.

Uses 1

Statement usesMultiplicative order modulo \(n\)

TheoremUnique order-preserving lift modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime and let \(a\) be a natural number coprime to \(p\). Writing \(\operatorname{ord}_n(b)\) for the multiplicative order of \(b\) modulo \(n\), there is exactly one \(m \in \{0, 1, \dots, p - 1\}\) such that \(\operatorname{ord}_{p^2}(a + mp) = \operatorname{ord}_p(a)\).

theorem_wanted existsUnique_order_add_mul_prime_eq
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (a : ℕ)
    (ha : Nat.Coprime a p) :
    ∃! m : ZMod p, mulOrdMod (p ^ 2) (a + m.val * p) = mulOrdMod p a

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Theorem 2.

Uses 1

Statement usesMultiplicative order modulo \(n\)

TheoremUnique order-preserving element of a fiber modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime, let \(x_0\) be a unit modulo \(p^2\), and let \(P_{x_0}\) be the set of units \(x\) modulo \(p^2\) with \(x \equiv x_0 \pmod p\). There is exactly one \(x \in P_{x_0}\) whose multiplicative order modulo \(p^2\) equals the multiplicative order of its reduction modulo \(p\).

theorem_wanted existsUnique_mem_liftFiber_order_eq
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (x₀ : (ZMod (p ^ 2))ˣ) :
    ∃! x, x ∈ liftFiber p x₀ ∧ orderOf x = orderOf (unitReduceSq p x)

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Theorem 2.

Uses 2

Statement usesFibers of reduction modulo \(p\) on units modulo \(p^2\) · Reduction of units modulo \(p^2\) to units modulo \(p\)

TheoremGauss's theorem on primitive roots modulo prime powers#●ready to prove

Let \(p\) be an odd prime and let \(g\) be a natural number that is a primitive root modulo \(p\), where a primitive root modulo \(n\) is a residue class modulo \(n\) of multiplicative order \(\varphi(n)\). Then there is a natural number \(k\) such that \(g + kp\) is a primitive root modulo \(p^\ell\) for every \(\ell \ge 2\).

theorem_wanted exists_primitiveRoot_add_mul_prime_pow
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (g : ℕ)
    (hg : IsPrimitiveRoot ((g : ZMod p)) (Nat.totient p)) :
    ∃ k : ℕ, ∀ ℓ : ℕ, 2 ≤ ℓ →
      IsPrimitiveRoot (((g + k * p : ℕ) : ZMod (p ^ ℓ)))
        (Nat.totient (p ^ ℓ))

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Theorem 1.

TheoremExactly one lift of a primitive root fails modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime and let \(g\) be a natural number that is a primitive root modulo \(p\), where a primitive root modulo \(n\) is a residue class modulo \(n\) of multiplicative order \(\varphi(n)\). Then there is exactly one \(m \in \{0, 1, \dots, p - 1\}\) such that \(g + mp\) is not a primitive root modulo \(p^2\), and \(g + kp\) is a primitive root modulo \(p^2\) for every other \(k \in \{0, 1, \dots, p - 1\}\).

theorem_wanted existsUnique_not_primitiveRoot_add_mul_prime
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (g : ℕ)
    (hg : IsPrimitiveRoot ((g : ZMod p)) (Nat.totient p)) :
    ∃! m : ZMod p,
      ¬ IsPrimitiveRoot (((g + m.val * p : ℕ) : ZMod (p ^ 2)))
          (Nat.totient (p ^ 2)) ∧
        ∀ k : ZMod p, k ≠ m →
          IsPrimitiveRoot (((g + k.val * p : ℕ) : ZMod (p ^ 2)))
            (Nat.totient (p ^ 2))

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Corollary 1.

TheoremThe lift of order \(p - 1\) of a primitive root#●ready to prove

Let \(p\) be an odd prime and let \(g\) be a natural number that is a primitive root modulo \(p\), that is, a residue class modulo \(p\) of multiplicative order \(\varphi(p) = p - 1\). Let \(P_g\) be the set of units \(x\) modulo \(p^2\) with \(x \equiv g \pmod p\). Then exactly one \(x \in P_g\) has multiplicative order \(p - 1\) modulo \(p^2\).

theorem_wanted existsUnique_mem_liftFiber_order_eq_sub_one
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (g : ℕ)
    (hg : IsPrimitiveRoot ((g : ZMod p)) (Nat.totient p)) :
    ∃! x, x ∈ liftFiber p (ZMod.unitOfCoprime g
        (((ZMod.isUnit_iff_coprime g p).mp
          (hg.isUnit (Nat.totient_pos.mpr hp.pos).ne')).pow_right 2)) ∧
      orderOf x = p - 1

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Corollary 1.

Uses 1

Statement usesFibers of reduction modulo \(p\) on units modulo \(p^2\)

TheoremPrimitive roots modulo \(p^\ell\) of the form \(g^p + kp\)#●ready to prove

Let \(p\) be an odd prime and let \(g\) be a natural number that is a primitive root modulo \(p\). If \(k\) is a natural number not divisible by \(p\), then \(g^p + kp\) is a primitive root modulo \(p^\ell\) for every natural number \(\ell > 1\).

Here a natural number \(a\) is a primitive root modulo \(n\) when its residue class in \(\mathbb{Z}/n\mathbb{Z}\) is a primitive \(\varphi(n)\)-th root of unity, where \(\varphi\) is Euler's totient function.

theorem_wanted primitiveRoot_pow_add_mul_prime_pow
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (g k : ℕ)
    (hg : IsPrimitiveRoot ((g : ZMod p)) (Nat.totient p))
    (hk : ¬ p ∣ k) :
    ∀ ℓ : ℕ, 1 < ℓ →
      IsPrimitiveRoot (((g ^ p + k * p : ℕ) : ZMod (p ^ ℓ)))
        (Nat.totient (p ^ ℓ))

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Theorem 3.

TheoremEndomorphisms of the units modulo \(p^2\) respect the fibers#●ready to prove

Let \(p\) be an odd prime, let \(f\) be a group endomorphism of \((\mathbb{Z}/p^2\mathbb{Z})^\times\), and let \(a\) be a unit modulo \(p^2\). Writing \(P_b\) for the set of units \(x\) modulo \(p^2\) with \(x \equiv b \pmod p\), the image of \(P_a\) under \(f\) is contained in \(P_{f(a)}\).

theorem_wanted monoidHom_image_liftFiber_subset
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2)
    (f : (ZMod (p ^ 2))ˣ →* (ZMod (p ^ 2))ˣ) (a : (ZMod (p ^ 2))ˣ) :
    f '' liftFiber p a ⊆ liftFiber p (f a)

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Lemma 3.

Uses 1

Statement usesFibers of reduction modulo \(p\) on units modulo \(p^2\)

TheoremPower maps on the fibers modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime, let \(a\) be a unit modulo \(p^2\), and let \(n\) be a natural number coprime to \(p\) and to the multiplicative order of \(a\). Writing \(P_b\) for the set of units \(x\) modulo \(p^2\) with \(x \equiv b \pmod p\), the map \(x \mapsto x^n\) is injective on \(P_a\), maps \(P_a\) onto \(P_{a^n}\), and preserves the multiplicative order of every element of \(P_a\).

theorem_wanted pow_injectiveOn_liftFiber_and_order_eq
    (p : ℕ) (hp : p.Prime) (hpo : p ≠ 2) (a : (ZMod (p ^ 2))ˣ)
    (n : ℕ) (hnp : Nat.Coprime n p) (hno : Nat.Coprime n (orderOf a)) :
    Set.InjOn (fun x => x ^ n) (liftFiber p a) ∧
      (fun x => x ^ n) '' liftFiber p a = liftFiber p (a ^ n) ∧
      ∀ b ∈ liftFiber p a, orderOf (b ^ n) = orderOf b

Sources

• V. P. Ramesh and S. Sivakumar, "A Note on Gauss's Theorem on the Primitive Roots Modulo p^ℓ", Lemma 4.

Uses 1

Statement usesFibers of reduction modulo \(p\) on units modulo \(p^2\)

3 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.