Racks and Quandles

Stream: maths

[Aaron Anderson]

I've started a branch on racks and quandles at mathlib:quandle. The coolest applications of quandles are in knot theory, which unfortunately seems long-off for mathlib, but it still might make a nice student project to flesh out the basic theory.

[Aaron Anderson]

I have a handout here with some exercises that could be formalized https://circles.math.ucla.edu/circles/lib/data/Handout-2325-2008.pdf

[Scott Morrison]

I have to admit my erstwhile-knot-theorist background (I'm somewhat embarrassed to admit I have a paper about a specific knot) never stirred much excitement in me about racks and quandles. Sure, they give knot invariants, but knot invariants are two-a-penny. I've never heard much interesting (i.e. connected to other things in topology and/or algebra) said about quandles except for the mere fact that they give knot invariants.

More interesting, if someone wanted to get started on some knot theory but still postponing getting hands dirty with embeddings and isotopy, might be trying to set up one of the nice combinatorial models (grid diagrams? braid closures?) and prove the first thing about an interesting knot polynomial (Alexander or Jones?) starting from one of those.

[Aaron Anderson]

I agree that sounds more interesting to have in Mathlib, but noodling around with esoteric first-order structures sounds easier out the starting gate if you've just finished, say, NNG

[Kevin Buzzard]

Where is the website which archives these Zulip posts? I could tweet about this -- there are people out there who will be interested, but I don't want to link to the Zulip chat because of the login

[Bryan Gin-ge Chen]

Here's the link you're looking for: https://leanprover-community.github.io/archive/stream/116395-maths/topic/Racks.20and.20Quandles.html

It seems to get to the archive, you have to first click on "Meet us" in the menu on the top right, and then find the archive link under The Lean Zulip chat.

[Kyle Miller]

I was thinking about formalizing quandles this summer but never got around to it... I was thinking of formalizing knots using, essentially, PD codes, since that gives virtual knots too, and quandle people like virtual knots. Then I'd show there are at least three knots (the unknot, trefoil, and figure-eight). Way off in the future would be proving every oriented link (embedded oriented 1-manifold in $S^3$) has a diagram and Reidemeister's theorem, that every isotopy corresponds to a sequence of Reidemeister moves.

@Scott Morrison The fundamental quandle is a complete invariant of a non-split oriented link, up to orientation-reversing mirror image, so it's definitely unlike other invariants in this respect. The cool thing about them is that they are an algebraic object that combines the fundamental group of the link exterior with the peripheral system -- so an algebraic object that lets you apply Waldhausen's theorem. It seems like people have done some interesting things with quandle cohomology, but I haven't really looked into that yet. More generally, a quandle can be thought of as being a set with a group action on itself with a distributivity property (a symmetric space forms a quandle, for instance), but I don't if anyone's done anything with this observation.

Regarding the Jones polynomial, ideally it would involve defining the Temperley-Lieb planar algebra, then you can get the Kauffman bracket from composing all the crossings' corresponding elements. (This is how I compute it in https://kmill.github.io/knotfolio/, a paint program that helps you identify knots and calculate invariants.)

[Kyle Miller]

Regarding the Alexander polynomial, do we have Fitting ideals in mathlib yet? or (twisted) homology groups? Given a group G and a map f : G -> Z, its kth Alexander polynomial could be defined to be the GCD of the kth Fitting ideal of the first homology of G twisted by f. Then for knots/links, this would be for the fundamental group of the complement with f being the map sending each meridian curve to 1.

[Alex J. Best]

your knotfolio link is broken (wrong way round)

[Kyle Miller]

@Alex J. Best Thanks, still down have markdown down even after using it for years.

[Kyle Miller]

There's another definition of Alexander polynomials that comes from the determinant of the matrix of a bilinear form that comes from a connected Seifert surface. This happens to normalize the Alexander polynomial; the classical definition is only defined up to multiplication by a unit in the ring of Laurent polynomials over Z. This second one gives an evaluation of the single-variable Conway potential.

[Kyle Miller]

I've written code to generate a Seifert surface from a knot diagram to calculate this matrix, but writing the same thing in Lean seems daunting and would require a number of graph theory algorithms to be implemented. (And then proving that the determinant of this matrix did not depend on the original diagram would be an enormous undertaking!)

[Scott Morrison]

I would love to do some planar algebras! I think our development of manifolds is not quite up to doing actual planar tangles and isotopies of them, so for now we'd need to give a purely combinatorial version. (Perhaps Kuperberg's axiomatization of a spider would be best?)

[Kevin Buzzard]

I have an MSc student who did group cohomology but it's one of those things where by doing it I learnt a lot about how we should have done it.

[Kevin Buzzard]

The day before he was going to hand it in he realised that he had only defined H^n for n>=1 because he didn't have (-1)-cochains

[Jacques Carette]

One of the things I like most about Racks and Quandles is how nicely they fit in the algebra hierarchy. From a purely "universal algebra" point of view (and thus from a structuralist point of view), they fit in well. As such, I wouldn't be surprised if a formalization of them would lead to some 'transportable' theorems, if one is on the lookout for such things.