Order of an element in a commutative group

Stream: Is there code for X?

[Hallon]

Is there a theorem: For a CommGroup, the order of any element divdes the order of the element which has max order? I cant find in mathlib4 :sob:

[Notification Bot]

This topic was moved here from #lean4 > Find some theorem in lean. by Mario Carneiro.

[Ruben Van de Velde]

docs#order_dvd_exponent though I think the name should start with orderOf

[Yaël Dillies]

Really we should change orderOf to something like GroupTheory.order

[Ruben Van de Velde]

Oh, is it actually the case that the exponent is attained by an element?

[Yaël Dillies]

... or to torsion maybe

[Yury G. Kudryashov]

Isn't torsion too overloaded?

[Yaël Dillies]

Not in a group theory context I would think?

[Yaël Dillies]

It's definitely less overloaded than order

[Yury G. Kudryashov]

https://en.wikipedia.org/wiki/Torsion_group ?

[Yury G. Kudryashov]

@Hallon I renamed the thread so that it's less generic.

[Hallon]

Homework drives me crazy. Thank you all for your help!

[Yury G. Kudryashov]

See also docs#Monoid.exponent_eq_max'_orderOf

[Yaël Dillies]

Yury G. Kudryashov said:

https://en.wikipedia.org/wiki/Torsion_group ?

Thats not torsion though! That's torsionGroup or Subgroup.torsion.

[Yury G. Kudryashov]

The proof of docs#Monoid.exponent_eq_iSup_orderOf should contain a proof of existence of an element with orderOf _ = exponent _.

[Yury G. Kudryashov]

Moving this fact to a separate lemma before that proof would be a good short PR.

[Hallon]

The last question of homework: the following is one line of source code which is very clear. But how to prove?

show orderOf (max_order_element G) = max' (image orderOf univ) _

The order of the max_order_element of G is equal to the max value of the set consisted of the order of all element of G?

[Hallon]

It's intuitively obvious

[Yury G. Kudryashov]

This is a HW on which course?

[Yury G. Kudryashov]

And what do you know about max_order_element G?

[Hallon]

HW is given by my tutor to exercise our lean programming. 'The finite subgroup of field is cyclic'. The informal language to prove is not difficult.

[Hallon]

‘max_order_element G' is the element of G which has max order

[Yury G. Kudryashov]

docs#subgroup_units_cyclic

[Eric Rodriguez]

Yury G. Kudryashov said:

The proof of docs#Monoid.exponent_eq_iSup_orderOf should contain a proof of existence of an element with orderOf _ = exponent _.

I'm not sure if this is true? The proof basically constructs an element with maximal p-adic norm for each $p \mid \operatorname{exp} G$, and the max' statement only holds for cancellative monoids

[Hallon]

Crazy

[Kevin Buzzard]

The informal proof of the field result is quite difficult isn't it? I don't know a simple proof of this. There's a proof which looks simple but which assumes the classification of finite abelian groups...

[Hallon]

I misdescribed it. The question is 'The finite multiplicative group of a field is a cyclic group'. The proof is about constructing n+1 roots, which contradicts the fundamental theorem of algebra

[Hallon]

微信截图_20240124171915.png
This is the informal proof, if you can understand Chinese

[Kevin Buzzard]

Fundamental theorem of algebra: that's not the hard part. The hard part is "if a finite abelian group is not cyclic then there exists an n such that there are more than n solutions to x^n=1". From first principles this is very nontrivial

[Hallon]

yep

[Kevin Buzzard]

Hence the theorem which you claimed was "not difficult" is in fact a "not difficult corollary of a difficult theorem" which is very different in lean. Fortunately we have the difficult theorem

[Yury G. Kudryashov]

And the corollary

[Hallon]

This problem is a relatively simple one from our practice problems, using some familiar conclusions

[Kevin Buzzard]

There is a completely low-level way to go about proving the corollary directly using a delicate counting argument, which I would recommend as a route if we didn't have the difficult theorem

[Hallon]

"a delicate counting argument"?

[Kevin Buzzard]

Yes, the proof that Gauss and Euler (who didn't know about groups) knew.

[Hallon]

Could you find it in wiki?

[Kevin Buzzard]

I don't know, I read it when I was an undergraduate, I have notes in my office :-)

[Hallon]

Uh-Huh, are you PHD now? I am only senior :grinning:

[Kevin Buzzard]

I don't know what your teacher wants but you should probably stick to the proof that they suggest :-)

[Hallon]

OK. Now I only have the last step to formalize the proof

[Yury G. Kudryashov]

@Hallon It's easy to find out that Kevin has a PhD degree for quite some time. E.g., by reading his Wikipedia page.

[Hallon]

So, how to write this step using lean? :sob:

show orderOf (max_order_element G) = max' (image orderOf univ) _

[Kevin Buzzard]

I'm not sure I want to do your homework for you...

[Hallon]

wow, Imperial College London. :pleading_face: My research direction is analytic number theory.

[Hallon]

OK, I'll think it over myself

[Ruben Van de Velde]

Yury G. Kudryashov said:

Moving this fact to a separate lemma before that proof would be a good short PR.

Got this compiling locally, will push later

[Eric Rodriguez]

I assume you had to change the proof? I think you can then generalize the max'_orderOf one to non-cancellative monoids, no?

[Ruben Van de Velde]

I found two ways - either extract most of the proof into a technical lemma, or prove the existence first. Not sure which is best: https://github.com/leanprover-community/mathlib4/pull/new/wip-monoid-exponent

[Ruben Van de Velde]

Oh, I missed your point about max. It can already be generalized to non-cancellative monoids at the expense of an explicit ∀ g : G, 0 < orderOf g hypothesis

[Eric Rodriguez]

I guess the issue here is that obviously 0 is maximal in the divisibility poset, and what we're looking for is actually a sup in this order; it just turns out that that agrees with the max for all non-zero integers

[Yaël Dillies]

Ruben Van de Velde said:

[...] at the expense of an explicit ∀ g : G, 0 < orderOf g hypothesis

You mean docs#Monoid.IsTorsion ?

[Ruben Van de Velde]

Maybe, but that's not how docs#Monoid.exponent_eq_iSup_orderOf is stated (please don't go and refactor the entire file before I get my changes in)

[Yaël Dillies]

Uh, annoying. Tell me when you're done :smile:

[Patrick Massot]

Hallon said:

I misdescribed it. The question is 'The finite multiplicative group of a field is a cyclic group'. The proof is about constructing n+1 roots, which contradicts the fundamental theorem of algebra

No, this is not the fundamental theorem of algebra, at least not what people call the fundamental theorem of algebra. The fundamental theorem say that non-constant polynomials with complex coefficients have at least one complex root. And from there it is easy to get as many roots counted with multiplicity as the degree. This is deep. What you need is the much, much easier result that a degree d polynomial over a field has at most d roots. This is important but much easier. It only depends on the Euclidean division of polynomials.

[Patrick Massot]

Kevin Buzzard said:

The informal proof of the field result is quite difficult isn't it? I don't know a simple proof of this. There's a proof which looks simple but which assumes the classification of finite abelian groups...

No, you don't need the full force of the classification of finite abelian groups. You only need to know that in every finite abelian group there is an element whose order is the exponent of the group. This is much easier (and can be a step towards the classification theorem depending on how you prove that classification).

[Patrick Massot]

The easier result only relies on Lagrange's theorem saying the order of a subgroup divides the order of the group, and on unique decomposition of natural numbers into products of primes.

[Patrick Massot]

See Lemma 5.4.13 from https://www.imo.universite-paris-saclay.fr/~patrick.massot/enseignement/poly_alg.pdf for instance.

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/pull/9975 (cc @Yaël Dillies )