Order of product of commuting elements of a group

Stream: maths

[Oliver Nash]

I just needed a version of the following lemma:

import group_theory.order_of_element

-- How generally is this true?
lemma commute.order_of_mul_eq_of_order_of_sq_dvd {G : Type*} [group G] {x y : G}
  (h_comm : commute x y) (hy : is_of_fin_order y) (h_dvd : (order_of x)^2 ∣ order_of y) :
  order_of (x * y) = order_of y :=
begin
  sorry,
end

I needed it when G was the add_circle (where it is definitely true). Can anyone less rusty on group theory comment on how generally this should be true?

[Kevin Buzzard]

It's true when v_p(o(x)) >= 1 implies v_p(o(x)) < v_p(o(y)), i.e. "if a prime goes into order_of x at least once, then it goes into order_of y more times than it goes into order_of x". This is tight in the sense that if there exists a prime dividing o(x) at least once and o(y) the same number of times, then you can get cancellation at that prime.

[Kevin Buzzard]

The way I think about it is to consider the finite abelian group generated by x and y, and decompose it into a product of abelian p-groups; the order of an element is a product of the "local orders" which are prime powers. If we have the "radical" of a positive integer, i.e. the product of the primes dividing that integer, then you want (radical(o(x)))^2 divides o(y).

[Yaël Dillies]

Do we have a definition of $rad$, actually? It would also be useful for a few olympiad problems

[Kevin Buzzard]

Oh wait that radical^2 is wrong, it's o(x)*radical(o(x)) divides o(y)

[Kevin Buzzard]

ie "each prime dividing o(x) also divides o(y)/o(x)"

[Oliver Nash]

Thanks for this, exactly what I wanted. Now if only I could snipe someone into proving it for me ;-)

[Oliver Nash]

I guess the statement would be:

import group_theory.order_of_element

@[to_additive]
lemma commute.order_of_mul_eq_order_of_iff {G : Type*} [group G] {x y : G}
  (h_comm : commute x y) (hy : is_of_fin_order y) :
  order_of (x * y) = order_of y ↔
  ∀ (p : ℕ), p.prime → p ∣ order_of x → (p * order_of x) ∣ order_of y :=
begin
  sorry,
end

[Junyan Xu]

I've written a proof but it's more painful than expected, and dealing with the ≠ 0 hypotheses is rather annoying; maybe we should switch the whole file data.nat.factorization.basic and docs#nat.lcm_ne_zero to use the ne_zero class. Notice I only proved one direction because the other isn't true: if x = y = (1 : zmod 3), then add_order_of (x + y) = 3 and 3 ∣ add_order_of x, but ¬ 9 ∣ add_order_of y.

import group_theory.order_of_element
import data.nat.factorization.basic

lemma dvd_of_forall_prime_mul_dvd {a b : ℕ}
  (hdvd : ∀ p : ℕ, p.prime → p ∣ a → p * a ∣ b) : a ∣ b :=
begin
  obtain rfl | ha := eq_or_ne a 1,
  { apply one_dvd },
  { obtain ⟨p, hp⟩ := nat.exists_prime_and_dvd ha,
    exact trans (dvd_mul_left a p) (hdvd p hp.1 hp.2) },
end

theorem nat.factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
  (a.lcm b).factorization = a.factorization ⊔ b.factorization :=
begin
  rw ← add_right_inj (a.gcd b).factorization,
  rw [← nat.factorization_mul (mt nat.gcd_eq_zero_iff.1 $ λ h, ha h.1) (nat.lcm_ne_zero ha hb),
    nat.gcd_mul_lcm, nat.factorization_gcd ha hb, nat.factorization_mul ha hb],
  ext1, exact (min_add_max _ _).symm,
end

theorem nat.dvd_iff_factorization_prime_le {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
  a ∣ b ↔ ∀ p : ℕ, p.prime → a.factorization p ≤ b.factorization p :=
begin
  rw ← nat.ord_proj_dvd_ord_proj_iff_dvd ha hb,
  refine forall_congr (λ p, ⟨λ h hp, _, λ h, _⟩),
  { rwa [nat.pow_dvd_pow_iff_le_right hp.one_lt] at h },
  by_cases hp : p.prime,
  { exact pow_dvd_pow _ (h hp) },
  { simp_rw nat.ord_proj_of_not_prime _ _ hp },
end

lemma commute.order_of_mul_eq_order_of {G : Type*} [group G] {x y : G}
  (h_comm : commute x y) (hy : is_of_fin_order y)
  (hdvd : ∀ (p : ℕ), p.prime → p ∣ order_of x → (p * order_of x) ∣ order_of y) :
  order_of (x * y) = order_of y :=
begin
  have hxdy := dvd_of_forall_prime_mul_dvd hdvd,
  apply nat.dvd_antisymm (h_comm.order_of_mul_dvd_lcm.trans $ nat.lcm_dvd hxdy dvd_rfl),
  have hoy := (order_of_pos' hy).ne',
  by_cases hoxy : order_of (x * y) = 0, { rw hoxy, apply dvd_zero },
  rw nat.dvd_iff_factorization_prime_le hoy hoxy,
  by_contra', obtain ⟨p, hp, hl⟩ := this,
  have := ((commute.refl x).mul_right h_comm).inv_left.order_of_mul_dvd_lcm,
  have hox := ne_zero_of_dvd_ne_zero hoy hxdy,
  rw [inv_mul_cancel_left, order_of_inv,
    ← nat.factorization_le_iff_dvd hoy (nat.lcm_ne_zero hox hoxy)] at this,
  apply (this p).not_lt,
  rw nat.factorization_lcm hox hoxy,
  refine max_lt _ hl,
  specialize hdvd p hp,
  contrapose! hdvd,
  refine ⟨nat.dvd_of_factorization_pos ((pos_of_gt hl).trans_le hdvd).ne', _⟩,
  rw ← nat.factorization_le_iff_dvd (mul_ne_zero hp.ne_zero hox) hoy,
  rw nat.factorization_mul hp.ne_zero hox,
  refine λ h, ((h p).trans hdvd).not_lt (lt_add_of_pos_left _ _),
  rw hp.factorization_self,
  exact zero_lt_one,
end

[Junyan Xu]

Nice, this proof is now short enough:

import group_theory.order_of_element

lemma dvd_of_forall_prime_mul_dvd {a b : ℕ}
  (hdvd : ∀ p : ℕ, p.prime → p ∣ a → p * a ∣ b) : a ∣ b :=
begin
  obtain rfl | ha := eq_or_ne a 1,
  { apply one_dvd },
  { obtain ⟨p, hp⟩ := nat.exists_prime_and_dvd ha,
    exact trans (dvd_mul_left a p) (hdvd p hp.1 hp.2) },
end

lemma commute.order_of_mul_eq_order_of {G : Type*} [group G] {x y : G}
  (hc : commute x y) (hy : is_of_fin_order y)
  (hdvd : ∀ (p : ℕ), p.prime → p ∣ order_of x → (p * order_of x) ∣ order_of y) :
  order_of (x * y) = order_of y :=
begin
  have hoy := order_of_pos' hy,
  have hxy := dvd_of_forall_prime_mul_dvd hdvd,
  apply order_of_eq_of_pow_and_pow_div_prime hoy; simp only [ne, ← order_of_dvd_iff_pow_eq_one],
  { exact hc.order_of_mul_dvd_lcm.trans (nat.lcm_dvd hxy dvd_rfl) },
  intros p hp hpy hd,
  have := ((commute.refl x).mul_right hc).inv_left.order_of_mul_dvd_lcm.trans (nat.lcm_dvd _ hd),
  { rw [inv_mul_cancel_left, nat.dvd_div_iff hpy] at this,
    apply hp.ne_one,
    rwa [← nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul] },
  { rw [order_of_inv, nat.dvd_div_iff hpy],
    by_cases p ∣ order_of x,
    exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy] },
end

[Oliver Nash]

Oh, wow I thought it was a 100:1 shot that someone would do this! Is there a PR?

[Oliver Nash]

Thanks so much.

[Junyan Xu]

I originally thought it straightforwardly follows from docs#commute.order_of_mul_dvd_lcm, but then I realized I need something about factorizations and the proof gets much longer than expected; fortunately docs#order_of_eq_of_pow_and_pow_div_prime came to rescue in the end.

I'll generalize to monoids and make a PR later today.

[Junyan Xu]

#17997