Chris M : Starting to contribute to mathlib

Stream: new members

[Chris M]

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]

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

[Chris M]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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]

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]

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]

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]

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.