Is there a theorem about cyclic group?

Stream: new members

[Yicheng Tao]

When I was formalizing this exercise in Lean, I got stuck for some seemingly unformalized theorem in Mathlib.

Let $p$ be a prime number. Find the number of generators of the cyclic group $Z_{p^r}$ , where $r$ is an integer ≥ 1.

I might need theorem like this:
image.png

Or more universal theorem:
image.png

For now, I got Lean code as follows:

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.GroupTheory.Subgroup.ZPowers
import Mathlib.Data.Nat.Prime

variable (p r : ℕ)(G : ZMod (p ^ r))(generators: Finset (ZMod (p ^ r)))

example
(h₀ : ∀ n ∈ generators, AddSubgroup.zmultiples n = ZMod (p ^ r))
(h₁ : Fact (Nat.Prime p))
(h₂ : r ≥ 1):
  generators.card = p ^ r - p ^ (r - 1) := by
  sorry

Before handling the problem of counting, I need to convert the problem to count the elements that is relatively prime with $p^r$, which need the theorems above. I wonder if there have been similar theorems in Mathlib(since I haven't found any in cyclic group or ZMod).

[Michael Stoll]

This is basically docs#Nat.totient_prime_pow, at least assuming you know the general statement that a cyclic group of order $n$ has exactly $\varphi(n)$ generators.

[Michael Stoll]

(BTW, you can use double dollars $$...$$ to get $\LaTeX$ rendered in Zulip.)

[Yicheng Tao]

Michael Stoll 发言道：

This is basically docs#Nat.totient_prime_pow, at least assuming you know the general statement that a cyclic group of order $n$ has exactly $\varphi(n)$ generators.

Thanks! We have just found Nat.totient. Counting is no problem now, we only need to complete the first step.

[Riccardo Brasca]

Cyclic groups are in Mathlib.GroupTheory.SpecificGroups.Cyclic. If you look for totient in that file we see quite a lof of results.

[Kevin Buzzard]

The statement looks false to me. It has a natural subtraction in which is sometimes a code smell. What happens if r=0?

[Michael Stoll]

Also, generators could be the empty set...

[Riccardo Brasca]

@loogle ZMod, "totient"

[loogle]

:search: ZMod.card_units_eq_totient, ZMod.pow_totient

[Riccardo Brasca]

the first one looks very promising

[Yicheng Tao]

Kevin Buzzard 发言道：

The statement looks false to me. It has a natural subtraction in which is sometimes a code smell. What happens if r=0?

The statement says r is equal or greater than 1, which also means generators is not empty. I don't know if it's obvious to Lean.

Sorry for dropping this hypothesis in the displayed code.

[Yicheng Tao]

Riccardo Brasca 发言道：

the first one looks very promising

I think there is still a problem about the equivalence between generators and (ZMod n)ˣ.

[Ruben Van de Velde]

I don't think the way you've phrased generators as any set whose elements have some property is going to work. If your example applies to a particular set, it also applies to all subsets of that set, so they can hardly all have the same cardinality

[Ruben Van de Velde]

Do you mean to say something about the set of all elements with that property?

[Yicheng Tao]

Ruben Van de Velde 发言道：

I don't think the way you've phrased generators as any set whose elements have some property is going to work. If your example applies to a particular set, it also applies to all subsets of that set, so they can hardly all have the same cardinality

I agree with you. Actually I'm trying to fix that problem now by using set notation and Set.ncard.

[Yicheng Tao]

Updated code:

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Set.Card
import Mathlib.GroupTheory.Subgroup.ZPowers
import Mathlib.Data.Nat.Totient

variable (p r : ℕ)(G : ZMod (p ^ r))

def generators : Set (ZMod (p ^ r)) :=
  {n | AddSubgroup.zmultiples n = ⊤}

example
(h₀ : Nat.Prime p)
(h₁ : r ≥ 1):
  Set.ncard (generators p r) = p ^ (r - 1)  * (p - 1) := by
  have : Set.ncard (generators p r) = Nat.totient (p ^ r) := sorry
  rw [this]
  apply Nat.totient_prime_pow h₀; exact h₁

[Yicheng Tao]

I wonder if I can use the theorem ZMod.card_units_eq_totient. But that means I need to prove Set.ncard (generators p r) = Fintype.card (ZMod (p ^ r))ˣ .

[Ruben Van de Velde]

Okay, that's getting closer, but you've hit a peculiarity of type theory: we don't write "the subgroup is the entire group" but "the subgroup is the entire subgroup when seen as a subgroup of itself" (quite a mouthful, huh). The latter is written as \top, so:

def generators : Set (ZMod (p ^ r)) :=
  {n | AddSubgroup.zmultiples n = ⊤}

[Yicheng Tao]

Ruben Van de Velde 发言道：

Okay, that's getting closer, but you've hit a peculiarity of type theory: we don't write "the subgroup is the entire group" but "the subgroup is the entire subgroup when seen as a subgroup of itself" (quite a mouthful, huh). The latter is written as \top, so:

def generators : Set (ZMod (p ^ r)) :=
  {n | AddSubgroup.zmultiples n = ⊤}

Thanks for correction.

[Kevin Buzzard]

Yicheng Tao said:

Kevin Buzzard 发言道：

The statement looks false to me. It has a natural subtraction in which is sometimes a code smell. What happens if r=0?

The statement says r is equal or greater than 1

Aah yes, sorry for the noise! The natural subtraction is still a code smell though, why not use s=r-1 instead of r? Then you don't need a natural subtraction or the bound on the variable so it's slightly cleaner (you'll have to do this in the proof anyway in some sense)

[Yicheng Tao]

We finally come up with a solution as follows:

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Set.Card
import Mathlib.GroupTheory.Subgroup.ZPowers
import Mathlib.Data.Nat.Totient

open Classical
variable (p r : ℕ)(G : ZMod (p ^ r)) [h₀ : Fact (p.Prime)]

def generators : Set (ZMod (p ^ r)) :=
  {n | AddSubgroup.zmultiples n = ⊤}

example
(h₁ : r ≥ 1):
  Fintype.card (generators p r) = p ^ (r - 1)  * (p - 1) := by
  let trivialmap : generators p r → {n // Nat.Coprime (ZMod.val n) (p^r)} := fun
    | .mk v h => {
      val := v
      property := by
        simp [generators, AddSubgroup.eq_top_iff', AddSubgroup.mem_zmultiples_iff] at h
        have : ∃ (k : ℤ), k * v = 1 := h 1
        rw [Nat.coprime_iff_gcd_eq_one]
        rcases this with ⟨k, hk⟩
        simp at hk
        rw [show ↑k * v = ((k * v.val):ℤ)   by simp, show (1:ZMod (p^r)) = (1 : ℤ) by simp ] at hk
        rw [ZMod.int_cast_eq_int_cast_iff_dvd_sub (k * v.val) 1 (p^r)] at hk
        rcases hk with ⟨b, hb⟩
        simp at hb
        have h' : ∃ b : ℤ , k * v.val - b * ↑(p ^ r) = (1 : ℕ)  := by
          use -b
          simp
          linarith
        rcases h' with ⟨c, hc⟩

        have : (Nat.gcd (ZMod.val v) (p ^ r) : ℤ ) ∣ (k * (ZMod.val v) - c * ↑(p ^ r)) := by
          have aux1 : ↑(Nat.gcd (ZMod.val v) (p ^ r)) ∣ (ZMod.val v : ℤ) := by
            apply Int.ofNat_dvd.mpr
            exact Nat.gcd_dvd_left (ZMod.val v) (p ^ r)
          have aux2 : (Nat.gcd (ZMod.val v) (p ^ r) : ℤ) ∣ ↑(p ^ r) := by
            apply Int.ofNat_dvd.mpr
            exact Nat.gcd_dvd_right (ZMod.val v) (p ^ r)
          apply Int.dvd_sub
          · apply Int.dvd_trans aux1
            apply Int.dvd_mul_left
          · apply Int.dvd_trans aux2
            apply Int.dvd_mul_left
        rw [hc] at this
        rw [Int.ofNat_dvd] at this
        simp at this
        assumption
    }

  let trivialinverse : {n //  Nat.Coprime (ZMod.val n) (p^r)} → generators p r := fun
    | .mk v h => {
      val := v
      property := by
        simp [generators]
        rw [AddSubgroup.eq_top_iff' _]
        intro x
        rw [AddSubgroup.mem_zmultiples_iff]
        use (x.val * Nat.gcdA v.val (p^r))
        have this := (Nat.gcd_eq_gcd_ab v.val (p^r)).symm
        simp
        have : ↑(Nat.gcdA (ZMod.val v) (p ^ r)) * v  = 1 := by
          rw [Nat.Coprime.gcd_eq_one h] at this
          rw [show (1 : ZMod (p^r)) = (((1 : ℕ ): ℤ) : ZMod (p^r)) by simp ]
          rw [this.symm]
          simp only [ZMod.nat_cast_val, Int.cast_add, Int.cast_mul,
            ZMod.int_cast_cast, ZMod.cast_id', id_eq, Int.cast_pow, Int.cast_ofNat]
          rw [ZMod.nat_cast_self (p ^ r)]
          simp [mul_comm]
        rw [mul_assoc, this]
        simp
    }
  let iso : generators p r ≃ {n // Nat.Coprime (ZMod.val n) (p^r)} := {
    toFun := trivialmap
    invFun := trivialinverse
    left_inv := by
      intro a
      simp [trivialmap, trivialinverse]
    right_inv := by
      intro a
      simp [trivialmap, trivialinverse]
  }
  have : Fintype.card (generators p r) = Nat.totient (p ^ r) := by
    calc
      Fintype.card (generators p r) = Fintype.card {n // Nat.Coprime (ZMod.val n) (p^r)} := (Fintype.card_congr iso)
      _ = Fintype.card (ZMod (p^r))ˣ := (Fintype.card_congr ZMod.unitsEquivCoprime.symm)
      _ = Nat.totient (p ^ r) := ZMod.card_units_eq_totient _
  rw [this]
  apply Nat.totient_prime_pow h₀.out; exact h₁

Is there anything we can do to improve? Maybe simpler ideas?

[Antoine Chambert-Loir]

You can make the proof lighter by proving an equivalence: n generates iff p does not divide n.

[Jireh Loreaux]

This branch#j-loreaux/generator is very old now, but it contains a refactor where I introduce the type of generators of a group (which may be empty when the group is not cyclic). But I ran into some headaches with to_additive which made me abandon it.