-
Notifications
You must be signed in to change notification settings - Fork 160
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
Fix implication for IsSubsetLocallyFiniteGroup; and teach Units(GF(q)) its size #2220
Fix implication for IsSubsetLocallyFiniteGroup; and teach Units(GF(q)) its size #2220
Conversation
@ThomasBreuer suggested that instead of removing this implication, one could replace it by the correct implication InstallTrueMethod( IsSubsetLocallyFiniteGroup, IsFFECollection and IsMagmaWithInverses ); UPDATE: fixed to use |
@hulpke suggested that one should check why this implication was added in the first place. I did research this before making this PR, but did not add this in, as the result turned out to be not very helpful. It was added in this commit (not available in the public history):
Unfortunately, the commit message does not really explain why So, the only use of this property is via its implications, and the only relevant one (as far as I could tell) is this:
So, it ensures that finitely generated subgroups of permutation groups are marked as finite, which is great. The implication this PR removes presumable was meant to ensure that finitely generated subgroups of the unit group of a finite field would automatically be marked as finite. This is now gone. So the effect is that e.g. So, I guess this is useful, and we can follow @ThomasBreuer's suggestion to modify the true method instead (although I wonder if it is really that useful to justify a "true method"? I remember @hulpke being very concerned about their performance impact ;-). If we go that route, I'd also add some tests for the implications, e.g. the While we are at it, perhaps then one should also replace the current implication InstallTrueMethod( IsFinite, IsFFEMatrixGroup and IsFinitelyGeneratedGroup ); by this more general one? InstallTrueMethod( IsSubsetLocallyFiniteGroup, IsFFEMatrixGroup ); |
516570c
to
ad6bb49
Compare
@fingolfin (Answer will come in chunks to the several topics): I have no concern about My concern (past and now) is about Immediate methods which involve an explicit function call. They have epsilon cost but when called often (they might need to be called if the type of an object changes) that can sum up. Also the result of one immediate method can trigger other immediate methods. (In around ~1998 we observed such effects in concrete code.) |
@fingolfin Thanks for digging out the commit message (which I was unable to find in git). Let me describe what I recall these filters and the Many of the library routines (and in particular basic fallback routines) require finiteness, and thus it seems to be right to have them require A solution to both problems seemed to be to have the category of certain objects to imply (through true methods) finiteness. In some cases (e.g. PcGroups) this is easy and clear. In other cases (say permutation groups, if we assume I'm not insisting on this particular solution, but if we remove it we should be careful that the |
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.
With the changed implication I am happy with the PR.
Thanks @ThomasBreuer and @hulpke for taking the time to review this and lots of helpful remarks! |
64b8d93
to
355cfe7
Compare
IsFFECollection and IsMagma does *not* imply IsSubsetLocallyFiniteGroup, as e.g. any finite field GF(q) satisfies the former, but clearly not the latter (due to containing 0). However, using IsMagmaWithInverses fixes this.
... and this then automatically gives the implication IsFFEMatrixGroup and IsFinitelyGeneratedGroup => IsFinite
IsFFECollection and IsMagma does not imply IsSubsetLocallyFiniteGroup, as e.g. any finite field GF(q) satisfies the former, but clearly not the latter