Stream: new members

Topic: Chris M : Starting to contribute to mathlib

Chris M (Aug 17 2020 at 03:55):

Is there a way that Junyan Xu's thread can be split from this one? It was intended specifically for me to find a theorem to prove in mathlib.

Notification Bot (Aug 17 2020 at 03:55):

This topic was moved by Scott Morrison to #general > exists_nat_pow_near

Chris M (Aug 22 2020 at 04:21):

Cross-posting this: I'd like to do Cayley's theorem or "characterization of conjugacy classes of a symmetric group as partitions of n". I've searched mathlib for "Cayley" and Cayley's theorem doesn't seem to be there. Can I just start doing this?

Scott Morrison (Aug 22 2020 at 05:35):

Sounds good! To my knowledge this isn't in mathlib, but others, e.g. @Chris Hughes, would be much more likely to know what's been done.

Chris M (Aug 22 2020 at 06:04):

By the way, I feel like this process of finding a theorem to work on was somewhat slow. Is this normal? For example it happened twice now I think, that I thought II had a topic but then someone said that actually it already exists or requires something that isn't in mathlib yet. Also, when I searched "symmetric group" in mathlib nothing popped up, yet someone said that symmetric groups were treated, so I'm not sure how to know from a mathlib search whether something exists. I hope I can make this process go faster from now on.

Kevin Buzzard (Aug 22 2020 at 07:28):

The question of whether "mathlib has symmetric groups" is a lot more subtle than one night think. I was surprised by this.

Kevin Buzzard (Aug 22 2020 at 07:30):

There's a type of bijections from a type to itself. Feed in fin n and you have the symmetric group. There's also all the stuff in data.list.perm which implicitly proves that symmetric groups are generated by adjacent transpositions. So in some sense there's already a lot there, and different parts are implemented in two completely different ways!

Chris M (Aug 22 2020 at 07:32):

Hmm, that does make it harder to know whether something is in there I guess

Kevin Buzzard (Aug 22 2020 at 07:33):

On the other hand there is no function in mathlib which eats n and spits out a model for S_n. For note that there is no canonical symmetric group, the object is just defined up to nonunique isomorphism (in fact it is defined up to inner automorphism, which is why theorems about it are statements about how it is generated by conjugacy classes or the classification of conjugacy classes)

Kevin Buzzard (Aug 22 2020 at 07:34):

Some people might even say that defining the model is not needed because definitions weigh mathlib down, especially definitions which nobody particularly wants for any fancy projects they're working on

Kevin Buzzard (Aug 22 2020 at 07:35):

This results in confused answers when people say "have we got the symmetric group". When people say "have we got definition X" they often mean "have we got an API for definition X" anyway

Kevin Buzzard (Aug 22 2020 at 07:37):

There's no particularly exciting API for symmetric groups, they're just a little mini project parts of which have been essentially done already in incompatible ways in other places in mathlib

Patrick Massot (Aug 22 2020 at 07:38):

I don't see what is confusing. The main entry point to answer questions like "does mathlib know about this or this topic?" is https://leanprover-community.github.io/mathlib-overview.html. Go there, search for permutation. It's here in plain sight.

Kevin Buzzard (Aug 22 2020 at 07:39):

But I would imagine these things are on Patrick's list and if we could prove that the alternating groups A_n are simple for n>=5 that would be a cool result to have

Patrick Massot (Aug 22 2020 at 07:41):

Sure, if you want to see missing stuff you can also follow the link from the previous cited page to https://leanprover-community.github.io/undergrad_todo.html and look under "group theory/permutation group".

Patrick Massot (Aug 22 2020 at 07:44):

Note that browsing the directory structure of mathlib is also an option, especially on https://leanprover-community.github.io/mathlib_docs. There is group_theory/perm that look pretty promising.

Kyle Miller (Aug 22 2020 at 08:14):

In group_theory/perm you find decompositions into transpositions and decomposition into cycles with disjoint support, at least that's what I thought I saw when I checked last night when Chris was asking about this topic. So does mathlib have these things for permutation groups or not?

Kyle Miller (Aug 22 2020 at 08:18):

Kevin Buzzard said:

There's a type of bijections from a type to itself. Feed in fin n and you have the symmetric group. There's also all the stuff in data.list.perm which implicitly proves that symmetric groups are generated by adjacent transpositions. So in some sense there's already a lot there, and different parts are implemented in two completely different ways!

One difference is that perm lets you have the full symmetric group on arbitrary possibly infinite sets, where data.list.perm doesn't because it's only for (finite) lists. But, for the finite case it looks like no one's proved that there's a group isomorphism as best I can tell.

Chris Hughes (Aug 22 2020 at 10:28):

This is something that's sorely missing from mathlib. It's probably quite a challenging project, but for different reasons. The gap between the informal proof and the formal proof is quite large; expect it to be a couple of thousand lines or more if done well. I did think a lot about how to do this at some point, and have a loose roadmap in my head, but never wrote this down. I can certainly have a go at writing it down if you want. It will probably involve developing the theory of morphisms of $G$-sets, and sub $G$-sets. You probably want to define the cycle shape of $\sigma$ in terms of the orbits of the action of the subgroups generated by $\sigma$, rather than the length of the factors, and also develop a library about the "shape" of an equivalence relation, in terms of the sizes of its equivalence classes.

Kyle Miller (Aug 22 2020 at 18:17):

@Chris Hughes Along these lines, I've thought it would be kind of cool if there were a formalization that the Todd-Coxeter algorithm terminates if the number of cosets is finite. The input to the algorithm is a finitely presented group $G$ and a finitely generated subgroup $H$, and the output (if it terminates) is the Schreier graph of $G/H$ as a $G$-set, where there is one vertex per element of the coset space $G/H$, and for every vertex $gH\in G/H$ and group generator $g_i\in G$ there is a $g_i$-labeled directed arrow from $gH$ to $g_igH$. (When $H=1$, such a graph is known as a Cayley graph.)

For $G=F_n/R$, where $F_n$ is a free group and $R$ is the normal subgroup generated by finitely many relations, then the way the algorithm works (abstractly speaking) is to construct a sequence of (not necessarily normal) subgroups $1 = R_0 \sub R_1 \sub R_2 \cdots \sub R$ by looking at properties of the $F_n/R_i$ action on $(F_n/R_i)/H_i$, where $H_i$ is the group in $F_n/R_i$ generated by the same words as $H$ in $G$. From the Scheier graph point of view, the way these are constructed is that you keep track of "visited" cosets, then choose any unvisited coset neighboring a visited coset, add just enough relators from $R$ to $R_i$ so that $G$'s relations form closed loops there in the Scheier graph, and then you add the coset to the visited set.

You can argue that the Scheier graph eventually stabilizes for every large enough radius (though I'm pretty sure figuring out how long to run it is an uncomputable problem!), so the limit of the process, in a suitable sense, gives the Scheier graph. Thus, if $G/H$ were finite the graph would completely stabilize after finitely many steps.

I've used a Todd-Coxeter calculator (with its implementation described here) a number of times for some covering space theory, but it would be nice to know it's correct!

Chris Hughes (Aug 22 2020 at 19:12):

It sounds like a fun project. I've actually been working on something not entirely unrelated. I've just implemented an algorithm for solving the word problem on a group presented by a single relation. link. I haven't proved the correctness of the algorithm, but instead I compute a certificate of the result, which can then be turned into a Lean proof. As an example, a certificate of the fact $aba^{-1}b^{-1}=1 \implies a^2ba^{-2}b^{-1} = 1$ would be $a^2ba^{-2}b^{-1} = [(a^2 b a^{-2} b^{-1}) (aba^{-1}b^{-1})(a^2 b a^{-2} b^{-1})^{-1}][a (aba^{-1}b^{-1}) a^{-1}] = 1$. It may well be a lot easier to compute some certificate than verify the whole algorithm

Kyle Miller (Aug 22 2020 at 20:12):

Every finitely presented group has a semidecidable word problem, in that you can give a certificate of that form if the words are related, but telling whether two words aren't equal seems to be the hard part. Is what's going on here that one-relator groups are HNN extensions, and you can use this to create a word-normalization procedure, and then two words are equal iff their normalizations are equal?

Chris Hughes (Aug 22 2020 at 20:23):

Something pretty close to that yes. The normal form is not unique, but it is unique for 1, so you just normalise $ab^{-1}$ rather than normalising both a and b.

Chris Hughes (Aug 22 2020 at 21:33):

The semidecidability result isn't a practical result though right? It doesn't compute it in any sort of reasonable time, is it more or less by completeness of first order logic, and countability of the set of proofs, so the algorithm is just a search through the countable set of proofs?

Kyle Miller (Aug 22 2020 at 22:27):

Indeed, if two words are equal, there is a (finite) sequence of rewrites connecting them, so enumerating all reachable words from a given word gives a semidecision procedure, since there's no way in general to know how much of this graph you have to search before you should give up. No claims that this is practical except for simple examples :smile:

With the 1-relator groups, is it sort of like Dehn's algorithm for surface groups where you pull a word tight in the group presentation complex? There's some ambiguity with Dehn's algorithm when words go antipodally across a face -- is this sort of where the ambiguity comes from? (And what's the complexity class? I want to say it's in NP and co-NP, but maybe certificates can be exponentially long.)

(And sorry Chris for going somewhat off-topic here.)

Chris Hughes (Aug 22 2020 at 22:41):

I have heard about Dehn's algorithm but I don't know anything about it, so I can't answer that question. The complexity is worse than any finite tower of exponents, but I think this seems to be in rare edge cases, and it's still practical it seems.

Kyle Miller (Aug 22 2020 at 22:56):

My understanding from a geometric group theorist: a surface group (the fundamental group of a surface, usually genus>=2) is a 1-relator group, and you can think of the universal cover as being a tiling of the hyperbolic plane by a regular polygon, the 1-skeleton being the Cayley graph. If you have a word in the fundamental group, you can draw it as a path upstairs, pull it tight as a hyperbolic geodesic, and then homotope it back onto the 1-skeleton to read off a normalized word, up to some ambiguities. You can do this purely symbolically by taking all cyclic shifts of the relator and its inverse, cutting them into two parts where the first part is bigger than the second, and turning this into a list of rewrite rules where you rewrite the first part into the inverse of the second. Each of these rewrites corresponds to pushing part of the word's path across a polygon in a way that makes the resulting length a bit shorter.

The complexity is worse than any finite tower of exponents

So you're saying it's not elementary recursive? Is it primitive recursive? (I don't know much about these classes. They've just come up recently in 3-manifold topology regarding algorithms for 3-manifold recognition.)

Chris Hughes (Aug 22 2020 at 23:29):

It's not much like Dehn's algorithm in that case, although that method is complete for groups where the relation was of the form $r^n$ for $|n|>1$. I don't know what either of elementary recursive or primitive recursive mean. I just Googled both, and I guess it's probably not elementary recursive, and I think it probably is primitive recursive because every termination proof is just some natural number decreasing, usually the length of a word.

Last updated: May 08 2021 at 03:17 UTC