[Merged by Bors] - feat(group_theory/exponent): Define the exponent of a group

[Julian-Kuelshammer]

This PR provides the definition and some very basic API for the exponent of a group/monoid.

---

[ericrbg]

looks generally good to me :)

[ericrbg]

What is the convention on docs of to_additive things?

[Julian-Kuelshammer]

I'm not quite sure, but I remember being told that additive versions should be in the documentation, but I might be wrong.

[ericrbg]

raised this on zulip here

[jcommelin]

I think this is looking good now. We just need to decide what to do about the additive things in the module docstring. I don't have a strong opinion, and I wouldn't mind merging now. We can easily fix it later.

One thing, maybe for a future PR: computing exponents of explicit examples: cyclic groups, zmod n, dihedral groups, units of zmod p...

[ericrbg]

So I decided to play with this a little, to see how the API felt, and proved the exponent of a cyclic group:

Code:

import group_theory.exponent
import set_theory.fincard

lemma exponent_eq_zero_iff {M} [monoid M] : monoid.exponent M = 0 ↔ ¬ monoid.exponent_exists M :=
begin
  rw [monoid.exponent],
  split_ifs,
  { classical,
    have := (nat.find_spec h).1.ne',
    simpa },
  tauto
end

lemma mem_powers_iff_mem_range_order_of' {G} [left_cancel_monoid G] [decidable_eq G]
  (x y : G) (hx : 0 < order_of x):
  y ∈ submonoid.powers x ↔ y ∈ (finset.range (order_of x)).image ((^) x : ℕ → G) :=
finset.mem_range_iff_mem_finset_range_of_mod_eq' hx (λ i, pow_eq_mod_order_of.symm)


example {G} [group G] [is_cyclic G] : monoid.exponent G = nat.card G :=
begin
  obtain ⟨g, hg⟩ := is_cyclic.exists_generator G,
  classical,
  casesI fintype_or_infinite G,
  { rw [nat.card_eq_fintype_card, ←monoid.lcm_order_eq_exponent],
    apply nat.dvd_antisymm,
    { rw finset.lcm_dvd_iff,
      rintros b -,
      exact order_of_dvd_card_univ },
    rw ←order_of_eq_card_of_forall_mem_zpowers hg,
    exact finset.dvd_lcm (finset.mem_univ g) },
  rw [nat.card_eq_zero_of_infinite, exponent_eq_zero_iff, monoid.exponent_exists],
  push_neg,
  refine λ n hn, ⟨g, λ hgn, _⟩,
  have ho := order_of_pos' ((is_of_fin_order_iff_pow_eq_one g).mpr ⟨n, hn, hgn⟩),
  obtain ⟨x, hx⟩ := infinite.exists_not_mem_finset
                    (finset.image (pow g) $ finset.range $ order_of g),
  apply hx,
  rw [←mem_powers_iff_mem_range_order_of' g x ho, submonoid.mem_powers_iff],
  obtain ⟨k, hk⟩ := hg x,
  obtain ⟨k, rfl | rfl⟩ := k.eq_coe_or_neg,
  { exact ⟨k, by exact_mod_cast hk⟩ },
  let t : ℤ := -k % (order_of g),
  rw zpow_eq_mod_order_of at hk,
  have : 0 ≤ t := int.mod_nonneg (-k) (by exact_mod_cast ho.ne'),
  refine ⟨t.to_nat, _⟩,
  rwa [←zpow_coe_nat, int.to_nat_of_nonneg this]
end

Now, this is nice and all (and honestly was a massive pain to figure out how to work with zpow and pow together, but anyways...) but I think the key thing is that I think a useful lemma is:

  lemma exponent_eq_zero_iff {M} [monoid M] : monoid.exponent M = 0 ↔ ¬ monoid.exponent_exists M :=
  begin
    rw [monoid.exponent],
    split_ifs,
    { classical,
      have := (nat.find_spec h).1.ne',
      simpa },
    tauto
  end

If you want to add the rest of the stuff to the PR, too, feel free, but I don't want to scope-creep so I'm happy to PR it separately. (also, I used nat.card because to unify the cases, but it's not imported in this file, but everything else is, so may be worth separating into an infinite and fintype case instead.)

[Julian-Kuelshammer]

Maybe it is better in another PR where one also proves the converse that a finite abelian group whose order is equal to the exponent must be cyclic?

I formalised some lemma that in some textbooks is used to prove these results, namely that if x and y are commuting elements of coprime order, then their product has order the product of the orders. It seems that you wouldn't benefit from that, right? You can see the progress in the branch order_of_lcm_commute (note that so far I only formalised the minimal_period version, from which the order_of version should follow almost immediately by definition.

[jcommelin]

Thanks @Julian-Kuelshammer for the PR.
Thanks @ericrbg for the reviews.

Let's leave the remaining stuff for a future PR.

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[alexjbest]

Looks like to additive gives this the name exponent_dvd_of_forall_pow_eq_zero which doesn't quite match the statement, not a big issue but if you are adding more to this file it would be nice to fix this!

[ericrbg]

mathlib/src/group_theory/exponent.lean

Line 138 in c99a719

@[to_additive exponent_dvd_of_forall_nsmul_eq_zero]

turns out I had already in those PRs :) that is the correct name right?

[alexjbest]

Oh nice, great minds think alike lol! Looks perfect :D