-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(group_theory/exponent): exponent G = ⨆ g : G, order_of g #10767
Changes from 28 commits
b6cd9b8
fe3de83
d423e26
d1f4899
22dc2b3
32c3589
5ae4e7f
cdae685
6b167e3
289fbb2
c99a719
b41f030
bd06c3f
8ce4eac
86c0955
c89bc24
fdf5b33
d663777
27e872b
2fe2b58
6aecd72
e1d8ff7
d967662
7767754
7aab462
c9f3890
0c64ca4
7666489
af7fdfe
612c048
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -6,14 +6,15 @@ Authors: Julian Kuelshammer | |
import group_theory.order_of_element | ||
import algebra.punit_instances | ||
import algebra.gcd_monoid.finset | ||
import ring_theory.int.basic | ||
import tactic.by_contra | ||
import number_theory.padics.padic_norm | ||
|
||
/-! | ||
# Exponent of a group | ||
|
||
This file defines the exponent of a group, or more generally a monoid. For a group `G` it is defined | ||
to be the minimal `n≥1` such that `g ^ n = 1` for all `g ∈ G`. For a finite group `G` it is equal to | ||
the lowest common multiple of the order of all elements of the group `G`. | ||
to be the minimal `n≥1` such that `g ^ n = 1` for all `g ∈ G`. For a finite group `G`, | ||
it is equal to the lowest common multiple of the order of all elements of the group `G`. | ||
|
||
## Main definitions | ||
|
||
|
@@ -26,22 +27,27 @@ the lowest common multiple of the order of all elements of the group `G`. | |
|
||
## Main results | ||
|
||
* `lcm_order_eq_exponent`: For a finite group `G`, the exponent is equal to the `lcm` of the order | ||
of its elements. | ||
* `monoid.lcm_order_eq_exponent`: For a finite left cancel monoid `G`, the exponent is equal to the | ||
`finset.lcm` of the order of its elements. | ||
* `monoid.exponent_eq_Sup_order_of(')`: For a commutative cancel monoid, the exponent is | ||
equal to the supremum of the order of its elements (or zero if it has any order-zero elements). | ||
|
||
## TODO | ||
* Compute the exponent of cyclic groups. | ||
* Refactor the characteristic of a ring to be the exponent of its underlying additive group. | ||
-/ | ||
|
||
universe u | ||
|
||
variables (G : Type u) [monoid G] | ||
variable {G : Type u} | ||
|
||
open_locale classical | ||
|
||
namespace monoid | ||
|
||
section monoid | ||
|
||
variables (G) [monoid G] | ||
|
||
/--A predicate on a monoid saying that there is a positive integer `n` such that `g ^ n = 1` | ||
for all `g`.-/ | ||
@[to_additive "A predicate on an additive monoid saying that there is a positive integer `n` such | ||
|
@@ -55,12 +61,27 @@ def exponent_exists := ∃ n, 0 < n ∧ ∀ g : G, g ^ n = 1 | |
noncomputable def exponent := | ||
if h : exponent_exists G then nat.find h else 0 | ||
|
||
variable {G} | ||
|
||
@[to_additive] | ||
lemma exponent_eq_zero_iff : exponent G = 0 ↔ ¬ exponent_exists G := | ||
begin | ||
rw [exponent], | ||
split_ifs, | ||
{ simp [h, @not_lt_zero' ℕ] }, --if this isn't done this way, `to_additive` freaks | ||
{ tauto } | ||
end | ||
|
||
@[to_additive] | ||
lemma exponent_eq_zero_of_order_zero {g : G} (hg : order_of g = 0) : exponent G = 0 := | ||
exponent_eq_zero_iff.mpr $ λ ⟨n, hn, hgn⟩, order_of_eq_zero_iff'.mp hg n hn $ hgn g | ||
|
||
@[to_additive exponent_nsmul_eq_zero] | ||
lemma pow_exponent_eq_one (g : G) : g ^ exponent G = 1 := | ||
begin | ||
by_cases exponent_exists G, | ||
{ simp_rw [exponent, dif_pos h], | ||
exact (nat.find_spec h).2 g}, | ||
exact (nat.find_spec h).2 g }, | ||
{ simp_rw [exponent, dif_neg h, pow_zero] } | ||
end | ||
|
||
|
@@ -91,66 +112,190 @@ end | |
@[to_additive] | ||
lemma exponent_min (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ g : G, g ^ m ≠ 1 := | ||
begin | ||
by_contradiction, | ||
push_neg at h, | ||
have hcon : exponent G ≤ m := exponent_min' G m hpos h, | ||
by_contra' h, | ||
have hcon : exponent G ≤ m := exponent_min' m hpos h, | ||
linarith, | ||
end | ||
|
||
@[simp, to_additive] | ||
lemma exp_eq_one_of_subsingleton [subsingleton G] : exponent G = 1 := | ||
begin | ||
apply le_antisymm, | ||
{ apply exponent_min' _ _ nat.one_pos, | ||
{ apply exponent_min' _ nat.one_pos, | ||
simp }, | ||
{ apply nat.succ_le_of_lt, | ||
apply exponent_pos_of_exists _ 1 (nat.one_pos), | ||
apply exponent_pos_of_exists 1 (nat.one_pos), | ||
simp }, | ||
end | ||
|
||
@[to_additive add_order_dvd_exponent] | ||
lemma order_dvd_exponent (g : G) : (order_of g) ∣ exponent G := | ||
order_of_dvd_of_pow_eq_one (pow_exponent_eq_one G g) | ||
order_of_dvd_of_pow_eq_one $ pow_exponent_eq_one g | ||
|
||
@[to_additive] | ||
lemma exponent_dvd_of_forall_pow_eq_one (n : ℕ) (hG : ∀ g : G, g ^ n = 1) : | ||
variable (G) | ||
|
||
@[to_additive exponent_dvd_of_forall_nsmul_eq_zero] | ||
lemma exponent_dvd_of_forall_pow_eq_one (G) [monoid G] (n : ℕ) (hG : ∀ g : G, g ^ n = 1) : | ||
exponent G ∣ n := | ||
begin | ||
by_cases hpos : n = 0, { simp [hpos], }, | ||
rcases n.eq_zero_or_pos with rfl | hpos, | ||
{ exact dvd_zero _ }, | ||
apply nat.dvd_of_mod_eq_zero, | ||
by_contradiction h, | ||
have h₁ := nat.pos_of_ne_zero h, | ||
have h₂ : n % exponent G < exponent G := | ||
nat.mod_lt _ (exponent_pos_of_exists _ n (nat.pos_of_ne_zero hpos) hG), | ||
have h₂ : n % exponent G < exponent G := nat.mod_lt _ (exponent_pos_of_exists n hpos hG), | ||
have h₃ : exponent G ≤ n % exponent G, | ||
{ apply exponent_min' _ _ h₁, | ||
{ apply exponent_min' _ h₁, | ||
simp_rw ←pow_eq_mod_exponent, | ||
exact hG }, | ||
linarith, | ||
end | ||
|
||
variable [fintype G] | ||
|
||
@[to_additive lcm_add_order_of_dvd_exponent] | ||
lemma lcm_order_of_dvd_exponent : (finset.univ : finset G).lcm order_of ∣ exponent G := | ||
lemma lcm_order_of_dvd_exponent [fintype G] : (finset.univ : finset G).lcm order_of ∣ exponent G := | ||
begin | ||
apply finset.lcm_dvd, | ||
intros g hg, | ||
exact order_dvd_exponent G g | ||
exact order_dvd_exponent g | ||
end | ||
|
||
@[to_additive exists_order_of_eq_pow_padic_val_nat_add_exponent] | ||
lemma _root_.nat.prime.exists_order_of_eq_pow_padic_val_nat_exponent {p : ℕ} (hp : p.prime) : | ||
∃ g : G, order_of g = p ^ padic_val_nat p (exponent G) := | ||
begin | ||
haveI := fact.mk hp, | ||
rcases (padic_val_nat p $ exponent G).eq_zero_or_pos with h | h, | ||
{ refine ⟨1, by rw [h, pow_zero, order_of_one]⟩ }, | ||
have he : 0 < exponent G := ne.bot_lt (λ ht, by {rw ht at h, exact h.ne' (padic_val_nat_zero _)}), | ||
obtain ⟨g, hg⟩ : ∃ (g : G), g ^ (exponent G / p) ≠ 1, | ||
{ suffices key : ¬ exponent G ∣ exponent G / p, | ||
{ by simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key }, | ||
exact λ hd, hp.one_lt.not_le ((mul_le_iff_le_one_left he).mp $ | ||
nat.le_of_dvd he $ nat.mul_dvd_of_dvd_div (dvd_of_one_le_padic_val_nat h) hd) }, | ||
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := pow_padic_val_nat_dvd; try {apply_instance}, | ||
obtain ⟨t, ht⟩ := nat.exists_eq_succ_of_ne_zero h.ne', | ||
refine ⟨g ^ k, _⟩, | ||
rw ht, | ||
apply order_of_eq_prime_pow, | ||
{ rwa [hk, mul_comm, ht, pow_succ', ←mul_assoc, nat.mul_div_cancel _ hp.pos, pow_mul] at hg }, | ||
{ rw [←nat.succ_eq_add_one, ←ht, ←pow_mul, mul_comm, ←hk], | ||
exact pow_exponent_eq_one g }, | ||
end | ||
|
||
variable {G} | ||
|
||
@[to_additive] lemma exponent_ne_zero_iff_range_order_of_finite (h : ∀ g : G, 0 < order_of g) : | ||
exponent G ≠ 0 ↔ (set.range (order_of : G → ℕ)).finite := | ||
begin | ||
refine ⟨λ he, _, λ he, _⟩, | ||
{ by_contra h, | ||
obtain ⟨m, ⟨t, rfl⟩, het⟩ := set.infinite.exists_nat_lt h (exponent G), | ||
exact pow_ne_one_of_lt_order_of' he het (pow_exponent_eq_one t) }, | ||
{ lift (set.range order_of) to finset ℕ using he with t ht, | ||
have htpos : 0 < t.prod id, | ||
{ refine finset.prod_pos (λ a ha, _), | ||
rw [←finset.mem_coe, ht] at ha, | ||
obtain ⟨k, rfl⟩ := ha, | ||
exact h k }, | ||
suffices : exponent G ∣ t.prod id, | ||
{ intro h, | ||
rw [h, zero_dvd_iff] at this, | ||
exact htpos.ne' this }, | ||
refine exponent_dvd_of_forall_pow_eq_one _ _ (λ g, _), | ||
rw [pow_eq_mod_order_of, nat.mod_eq_zero_of_dvd, pow_zero g], | ||
apply finset.dvd_prod_of_mem, | ||
rw [←finset.mem_coe, ht], | ||
exact set.mem_range_self g }, | ||
end | ||
|
||
@[to_additive] lemma exponent_eq_zero_iff_range_order_of_infinite (h : ∀ g : G, 0 < order_of g) : | ||
exponent G = 0 ↔ (set.range (order_of : G → ℕ)).infinite := | ||
have _ := exponent_ne_zero_iff_range_order_of_finite h, | ||
by rwa [ne.def, not_iff_comm, iff.comm] at this | ||
|
||
end monoid | ||
|
||
section left_cancel_monoid | ||
|
||
variable [left_cancel_monoid G] | ||
|
||
@[to_additive lcm_add_order_eq_exponent] | ||
lemma lcm_order_eq_exponent {H : Type u} [fintype H] [left_cancel_monoid H] : | ||
(finset.univ : finset H).lcm order_of = exponent H := | ||
lemma lcm_order_eq_exponent [fintype G] : (finset.univ : finset G).lcm order_of = exponent G := | ||
begin | ||
apply nat.dvd_antisymm (lcm_order_of_dvd_exponent H), | ||
apply exponent_dvd_of_forall_pow_eq_one, | ||
intro g, | ||
have h : (order_of g) ∣ (finset.univ : finset H).lcm order_of, | ||
{ apply finset.dvd_lcm, | ||
exact finset.mem_univ g }, | ||
cases h with m hm, | ||
apply nat.dvd_antisymm (lcm_order_of_dvd_exponent G), | ||
refine exponent_dvd_of_forall_pow_eq_one G _ (λ g, _), | ||
obtain ⟨m, hm⟩ : order_of g ∣ finset.univ.lcm order_of := finset.dvd_lcm (finset.mem_univ g), | ||
rw [hm, pow_mul, pow_order_of_eq_one, one_pow] | ||
end | ||
|
||
@[to_additive] | ||
lemma exponent_ne_zero_of_fintype [fintype G] : exponent G ≠ 0 := | ||
by simpa [←lcm_order_eq_exponent, finset.lcm_eq_zero_iff] using λ x, (order_of_pos x).ne' | ||
|
||
end left_cancel_monoid | ||
|
||
section comm_monoid | ||
|
||
variable [cancel_comm_monoid G] | ||
|
||
@[to_additive] lemma exponent_eq_Sup_order_of (h : ∀ g : G, 0 < order_of g) : | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Do you see any way to split/golf this proof? Intuitively, I think it looks a lot longer than I would expect a proof of this result to be. But I haven't loaded it into VScode yet. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. my only thoughts are that the first half could maybe be made into a private lemma, and the second half could be turned into a There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. the order arguments were a lot more finicky here than I expected; I wish I could just say "if |
||
exponent G = Sup (set.range (order_of : G → ℕ)) := | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We usually use There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ooh, I didn't know about this. Is there an alternative for There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I just ended up just |
||
begin | ||
rcases eq_or_ne (exponent G) 0 with he | he, | ||
{ rw [he, set.infinite.nat.Sup_eq_zero $ (exponent_eq_zero_iff_range_order_of_infinite h).1 he] }, | ||
have hne : (set.range (order_of : G → ℕ)).nonempty := ⟨1, 1, order_of_one⟩, | ||
have hfin : (set.range (order_of : G → ℕ)).finite, | ||
{ rwa [← exponent_ne_zero_iff_range_order_of_finite h] }, | ||
obtain ⟨t, ht⟩ := hne.cSup_mem hfin, | ||
apply nat.dvd_antisymm _, | ||
{ rw ←ht, | ||
apply order_dvd_exponent }, | ||
refine nat.dvd_of_factors_subperm he _, | ||
rw list.subperm_ext_iff, | ||
by_contra' h, | ||
obtain ⟨p, hp, hpe⟩ := h, | ||
haveI hp := fact.mk (nat.prime_of_mem_factors hp), | ||
simp only [←padic_val_nat_eq_factors_count p] at hpe, | ||
set k := padic_val_nat p (order_of t) with hk, | ||
obtain ⟨g, hg⟩ := hp.1.exists_order_of_eq_pow_padic_val_nat_exponent G, | ||
suffices : order_of t < order_of (t ^ (p ^ k) * g), | ||
{ rw ht at this, | ||
exact this.not_le (le_cSup hfin.bdd_above $ set.mem_range_self _) }, | ||
have hpk : p ^ k ∣ order_of t := pow_padic_val_nat_dvd, | ||
have hpk' : order_of (t ^ p ^ k) = order_of t / p ^ k, | ||
{ rw [order_of_pow' t (pow_ne_zero k hp.1.ne_zero), nat.gcd_eq_right hpk] }, | ||
obtain ⟨a, ha⟩ := nat.exists_eq_add_of_lt hpe, | ||
have hcoprime : (order_of (t ^ p ^ k)).coprime (order_of g), | ||
{ rw [hg, nat.coprime_pow_right_iff (pos_of_gt hpe), nat.coprime_comm], | ||
apply or.resolve_right (nat.coprime_or_dvd_of_prime hp.1 _), | ||
nth_rewrite 0 ←pow_one p, | ||
convert pow_succ_padic_val_nat_not_dvd (h $ t ^ p ^ k), | ||
rw [hpk', padic_val_nat.div_pow hpk, hk, nat.sub_self], | ||
apply_instance }, | ||
rw [(commute.all _ g).order_of_mul_eq_mul_order_of_of_coprime hcoprime, hpk', hg, ha, ←ht, ←hk, | ||
pow_add, pow_add, pow_one, ←mul_assoc, ←mul_assoc, nat.div_mul_cancel, mul_assoc, | ||
lt_mul_iff_one_lt_right $ h t, ←pow_succ'], | ||
exact one_lt_pow hp.1.one_lt a.succ_ne_zero, | ||
exact hpk | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm really confused as to why, but if you put this |
||
end | ||
|
||
@[to_additive] lemma exponent_eq_Sup_order_of' : | ||
exponent G = if ∃ g : G, order_of g = 0 then 0 else Sup (set.range (order_of : G → ℕ)) := | ||
begin | ||
split_ifs, | ||
{ obtain ⟨g, hg⟩ := h, | ||
exact exponent_eq_zero_of_order_zero hg }, | ||
{ have := not_exists.mp h, | ||
exact exponent_eq_Sup_order_of (λ g, ne.bot_lt $ this g) } | ||
end | ||
|
||
@[to_additive] lemma exponent_eq_max'_order_of [fintype G] : | ||
exponent G = ((@finset.univ G _).image order_of).max' ⟨1, by simp⟩ := | ||
begin | ||
rw [←finset.nonempty.cSup_eq_max', finset.coe_image, finset.coe_univ, set.image_univ], | ||
exact exponent_eq_Sup_order_of order_of_pos | ||
end | ||
|
||
end comm_monoid | ||
|
||
end monoid |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should the name rather be
exponent_eq_zero_of_order_of_eq_zero
?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I feel like in the rest of the file,
order
has been used interchangably withorder_of
; I can change it but I prefer snappier names (at least as much as possible within the naming conventions)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we rename
order_of
toorder
? And update all the names? (Not in this PR, of course.)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd be in favour of that!