knot theory

Stream: new members

[Monica]

is it a good idea to do work on knot theory?

[Kyle Miller]

Do you have any knot theory in mind that you'd want to formalize?

I've been meaning to formalize knot diagrams via a variation on PD codes, but I haven't gotten around to it yet...

[Kyle Miller]

I think it should be fairly doable to formalize many of the sorts of things that you might find in virtual knot theory -- things that are diagrammatic.

It seem like it would be a lot of work to formalize the geometric topology side of knot theory. For example, the basic (but nontrivial) fact that a knot is the unknot iff the fundamental group of its complement is isomorphic to $\mathbb{Z}$.

[Monica]

yeah, that sounds about right. what about formalising the Alexander polynomial and the Jones polynomial, though?

[Monica]

or even the colouring invariant?

[Kyle Miller]

I think I know how to formalize the Jones polynomial, with the caveat that there might be some hidden surprises when formalizing a certain operad (edit: not sure actually what kind of object what I have in mind is; it's more some disks with arbitrary gluing data).

The Alexander polynomial has a nice presentation by Kauffman using determinants (based on Alexander's original definition via the Dehn presentation), and if I'm remembering it correctly it's not so hard to show it's a knot invariant.

[Kyle Miller]

docs#quandle is sitting there (and in particular docs#quandle.dihedral), waiting for its use in coloring invariants.

[Kyle Miller]

That depends on defining the fundamental quandle and showing Reidemeister moves correspond to quandle isomorphisms.

[Monica]

hmm, I'll give it a go tomorrow and create a new file called knot_theory then! this sounds exciting!

[Kyle Miller]

If we can do that, then we can do the same for fundamental groups of knot complements and give another definition of the (un-normalized) Alexander polynomial as the GCD of the 0th Fitting ideal of the abelianization of the commutator subgroup of $\pi_1(S^3-K)$ as a $\pi_1(S^3-K)$-module. (Not sure how much work that would be! But it would be nice because the higher Fitting ideals give higher Alexander invariants.)

[Kyle Miller]

The Seifert surface definition I'm going to say is completely out of reach. Doing a skein-theoretic definition (for either the Jones, Alexander-Conway polynomials, or even HOMFLY) might be fun

[Kyle Miller]

Probably the way to formulate the main theorem in those cases is that if $\mathcal{D}$ is the set of all knot diagrams and $R\cdot\mathcal{D}$ is free $R$-module generated by diagrams, then if $\mathcal{R}$ is the submodule generated by Reidemeister moves and the skein relation (where the ring $R$ might be, for example, $\mathbb{Z}[q^{\pm 1/2}]$ for the Jones polynomial), $(R\cdot\mathcal{D})/\mathcal{R}$ is generated by the unknot and is isomorphic to $R$, with the isomorphism sending the image of the unknot to $1$.

[Monica]

Kyle Miller said:

Do you have any knot theory in mind that you'd want to formalize?

I've been meaning to formalize knot diagrams via a variation on PD codes, but I haven't gotten around to it yet...

So @Siddharth Bhat and I are currently working on this, but we aren't quite sure what the best way to define knot is. Did you have a particular thought in mind defining it via a variation of PD codes?

[Kyle Miller]

I've been also doing some things with knots in the meantime, writing some code (in Lean 4) to calculate generalizations of Jones polynomials. What I've done is not very good for proving things about the invariants, though -- I just had a lot of polynomials to calculate and wanted a language I was more confident I wouldn't make a mistake in.

The first ingredient is the Node type:

inductive Node (α : Type _)
| Xp (a b c d : α)
| Xm (a b c d : α)
| P (a b : α)

/- Xp: Represents a right-handed oriented crossing like

  c ^ ^ b
     /
  d / \ a

  where a, b, c, and d are edge ids. -/

/- Xm: Represents a left-handed oriented crossing like

  d ^ ^ c
     \
  a / \ b

  where a, b, c, and d are edge ids. -/

and then a PD is

def PD α := List (Node α)

A PD should have the constraint that every index appears at most twice. A "complete" PD would be one where every index appears exactly 0 or 2 times.

[Siddharth Bhat]

@Kyle Miller So, we don't start with the geometric definition of a knot? We rather directly encode the combinatorial information about the crossings via PD?

[Kyle Miller]

What's your goal? If you start with the geometric definition, there's a whole lot of work ahead of you.

[Kyle Miller]

By the way, this was just the version of PD codes that was useful for me for calculating these Jones-like polynomials.

[Siddharth Bhat]

We'd like to work through the first four chapters of the "knots knotes" text (https://mathweb.ucsd.edu/~justin/Papers/knotes.pdf), which culminates with defining the Jones polynomial

[Kyle Miller]

There's another version, that could be useful, where indices appear exactly once, there is a fixed-point-free involution on the indices to connect them up, and there is some way to tell orientation information from the indices themselves.

[Kyle Miller]

For example, negative vs positive integers, the involution being negation, and positive integers are used for where you're coming from

[Kyle Miller]

That way it's easier to keep track of where you are in a knot. You just need the index itself.

[Kyle Miller]

That should make describing things like Reidemeister moves easier, since there's a way to explain how to trace out faces in the knot diagram as a sequence of moves of the type "go clockwise/counterclockwise around the current node" and "flip to other index"

[Monica]

what about defining braids? and defining the Jones polynomial via braids? any thoughts on that?

[Kyle Miller]

Yeah, you could do that -- define the Artin braid group, define a trace on it, and show it's a "Markov trace," as Jones called it.

There's some code for braid groups on the zulip somewhere, if I remember correctly.

[Kyle Miller]

It's less clearly about knots, though, since you need Markov's theorem (every knot is the closure of a braid, and two braids represent the same knot iff they're related by Markov moves)

[Kyle Miller]

I haven't looked whether it already exists in some form in mathlib, but there's also a braided monoidal category for tangles, braids being a special case. (@Scott Morrison Is there the free braided monoidal category generated by a single dualizable object? Hopefully I'm calling it the right thing here.)

[Junyan Xu]

I wasn't aware of PD codes, so I googled and found the KnotAtlas page which looks like a nice reference. It also mentions Conway and DT notations and braid representatives which I was aware of but have no idea how easy they're to work with. Let me also mention that there are grid diagrams that are amenable to computation of Heegaard--Floer homology.

[Junyan Xu]

if we can work with knots maybe we could also unlock Kirby calculus. I've always wondered about formalizing of geometric topology which is so much connected to spatial intuition that seems hard to formalize. (And I suspect AI might be able to develop superhuman higher-dimensional (>3D) intuition.) There's the sphere eversion project, but it's more on the differential geometry side.

I wonder whether people have thought about what it takes to formalize the loop theorem and the sphere theorem (which probably haven't been formalized elsewhere, and would be a real demonstration of the capability of Lean IMO). Of course we don't even have Jordan's curve theorem yet, but I assume it won't be hard as it's been formalized in other theorem provers and we already have developed homological algebra library. We have simply connected spaces in the PRs (#12788) now and hopefully some covering space theory soon.

[Junyan Xu]

Of course, "it's essential to do all the ways", as is well said by Kevin, so I don't think we should discourage anyone from working on their favorite definition! We want to have all definitions used by mathematicians and build API freely convert between them, not just a single preferred definition. Here's a recent exchange on the agda-unimath Discord which seems also appropriate here:

Boarders: Kevin Buzzard algebraic geometers love doing functor of points and not worrying about the underlying space, and in fact one could do the definition purely in terms of functors and grothendieck topologies

Kevin: It is true that we like functor of points when doing some things (moduli spaces) but we also really need the topological space sometimes. You're saying "we can do one way" but maths is not like that -- it's essential to do all the ways.
Or at least offer the API for every way of thinking about schemes
On top of this there is the danger that if you tell an algebraic geometer "I defined schemes" and they say "where's the topological space" it's not an acceptable answer to say "we don't have it because you don't need it" because you don't know what they need
I have a PhD student formalising GAGA in Lean and here you need some kind of topological space because on the analytic side you can't get away with abstract nonsense, you need to do it the old fashioned way as far as I know

[Scott Morrison]

May I suggest that if you use PD codes, you do oriented PD codes instead. I wrote a significant fraction of the in the KnotTheory package for mathematica (which is what underlies the KnotAtlas), and unoriented PD codes are just asking for trouble. :-) They cannot cope properly with hopf link connect summands to knots.

[Kyle Miller]

@Scott Morrison The code I posted above is for oriented PD codes

[Scott Morrison]

Excellent!

[Scott Morrison]

I would love love to see some geometric topology done in mathlib, as it feels like a very hard subject for formalisation. :-)

[Scott Morrison]

Starting with some combinatorial aspects (e.g. knot diagrams and calculating invariants from them) sounds good.

[Scott Morrison]

I did spend a while trying to formalise either the Temperley-Lieb algebra, the Jones polynomial, or Jones' planar algebras, or Kuperberg's spiders ... and I don't have any PRs to show for it. :-)

[Scott Morrison]

Answering the question above, no, we do not yet have any free braided categories.

[Scott Morrison]

Starting off just by defining the braid groups via Artin's presentations would be a good exercise.

[Kyle Miller]

I have some Lean 4 code for calculating a generalization of the Kauffman bracket for virtual knots up to 45 crossings, but I wouldn't call it a formalization

[Scott Morrison]

Cool!

[Kyle Miller]

It uses fake "nonplanar" algebras. I say "fake" because I don't bother to encode the boundary in the type or anything like that

[Kyle Miller]

(it's like the Temperley-Lieb planar algebra, but strands also have a $\mathbb{Z}$-valued disorientation, which is what I think you called them for su2. It's for the arrow polynomial, if you're familiar with it.)

[Kyle Miller]

I wrote it all in Javascript a while back, and I wasn't too confident that the code was bug-free, so I did a from-scratch rewrite in Lean 4, and I'm happy to say I got the same results!

[Scott Morrison]

I once had a massive computer calculation in code that I wasn't super confident in (written in scala), and a helpful grad student did a clean room re-implementation. I never attempted to read her code (it was written in C, commented in Persian), but was very very happy when it gave all the same results.

[Scott Morrison]

Yes: I think encoding the boundary in the type is generally asking for dependent-type-theory-hell style trouble. Much better to fake it for the data and operations, and then have theorems keeping track of the boundary.

[Kyle Miller]

What I was thinking was having the type record how many boundary strands there are, or rather what the signature of the boundary is (in/out), and then the data is a PD along with a list of edge indices that are supposed to match up with that boundary data. For my purposes, that was too much dependent type theory to be worth it in the short term, but compatibility guarantees would be nice.

Likely, to get around some DTT hell, the signature should be represented in a tree structure where you need to do explicit reassociation operations.

[Kyle Miller]

There are probably good data structures from work on higher category theory -- this reminds me a little of what I understand of opetopes.

[Kyle Miller]

Starting off just by defining the braid groups via Artin's presentations would be a good exercise.

Here's some code from Zulip:

import data.zmod.basic
import group_theory.presented_group
import group_theory.free_group
import data.equiv.mul_add
import algebra.group_power

def alt {S : Type*} : ℕ → S → S → free_group S
| 0 _ _ := 1
| (n+1) s t := free_group.of s * alt n t s

def artin_tits_rels (S : Type*) (m : S → S → ℕ) :
  set (free_group S) :=
{g | ∃ s t, g = (alt (m s t) s t)⁻¹ * (alt (m t s) t s)}

/-- Artin-Tits groups.  Traditionally we require that
`∀ s t, m s t = m t s` but the hypothesis isn't used in the definition. -/
abbreviation artin_tits (S : Type*) (m : S → S → ℕ) :=
presented_group (artin_tits_rels S m)

abbreviation braid_group (n : ℕ) :=
artin_tits (fin (n - 1))
  (λ i j, if abs ((i : ℤ) - j) = 1 then 3 else 2)

[Scott Morrison]

Nice! I hadn't realised just how compact that could be. In fact Michael Howes, who started group_theory.presented_group, wrote it with exactly this application in mind, but didn't PR the braid groups.

[Scott Morrison]

Someone should define the Burau representation, to exercise our new Rep k G. :-)

[Kyle Miller]

@Monica Here's a variant on PDs I had in mind, more fleshed out. It's a translation of the knot representation I used in https://kmill.github.io/knotfolio/ (source code). I think this would need more research&development for the Lean implementation, but it's something I think is worth thinking about. The benefit of it is that you can use a dart α as a pointer into a particular place on the knot, and then it's relatively easy to walk around the knot in different ways. This way of representing the knot is essentially a combinatorial map along with some vertex data for crossing information.

inductive dart (α : Type*)
| src : α → dart
| tgt : α → dart
-- this could also be a structure with a bool for whether it's the src

def dart.opp {α : Type*} : dart α → dart α
| (dart.src x) := dart.tgt x
| (dart.tgt x) := dart.src x

def dart.opp_ori {α : Type*} : dart α → dart α → Prop
| (dart.src _) (dart.tgt _) := true
| (dart.tgt _) (dart.src _) := true
| _ _ := false

def dart.arc {α : Type*} : dart α → α
| (dart.src x) := x
| (dart.tgt x) := x

/--

X:

  c   b
   \ /
    /
   / \
  d   a

P:

  a ---- b

-/
inductive node (α : Type*)
| X (a b c d : dart α) : node
| P (a b : dart α) : node

/- darts across node have opposite orientations -/
def node.valid_ori {α : Type*} : node α → Prop
| (node.X a b c d) := a.opp_ori c ∧ b.opp_ori d
| (node.P a b) := a.opp_ori b

def node.darts {α : Type*} : node α → multiset (dart α)
| (node.X a b c d) := {a, b, c, d}
| (node.P a b) := {a, b}

structure arc (κ : Type*) :=
(fst : κ)
(snd : κ)

structure link (κ α : Type*) [fintype κ] :=
(nodes : κ → node α)
(arcs : α → arc κ)
-- orientations are valid
(valid_oris : ∀ (v : κ), (nodes v).valid_ori)
-- the fst of each arc appears as a dart.src
(fst_is_src : ∀ (x : α), dart.src x ∈ (nodes (arcs x).fst).darts)
-- the snd of each arc appears as a dart.tgt
(snd_is_tgt : ∀ (x : α), dart.tgt x ∈ (nodes (arcs x).snd).darts)
-- every dart appears at most once
(darts_unique : multiset.nodup ((finset.univ : finset κ).val.bind (λ v, (nodes v).darts)))

[Kyle Miller]

In knotfolio, there's also some data for 2D positions of nodes, used for drawing the knot. These aren't needed for the isotopy class of the knot diagram.

[Patrick Massot]

Junyan Xu said:

There's the sphere eversion project, but it's more on the differential geometry side. I wonder whether people have thought about what it takes to formalize the loop theorem and the sphere theorem (which probably haven't been formalized elsewhere, and would be a real demonstration of the capability of Lean IMO).

There is no geometry at all in the sphere eversion project, in the sense that all manifolds are plain differentiable manifolds without any extra structure (riemannian, symplectic...). This is clearly topology. However it is crucially differential topology. Derivatives explicitly play a prominent role. The loop and sphere theorems can be stated in a purely $C^0$ world and I agree that their proof will be much more challenging to formalize. They would make an extremely nice project.

[Patrick Massot]

All the combinatorial knot theory (encoding knots with PD, grid diagrams etc.) is an interesting target because we could get certified knot atlases, and those atlases are well known to be useful tools. But this is completely orthogonal to discussing whether a proof assistant can do the geometric side of geometric topology.

[Monica]

Scott Morrison said:

I did spend a while trying to formalise either the Temperley-Lieb algebra, the Jones polynomial, or Jones' planar algebras, or Kuperberg's spiders ... and I don't have any PRs to show for it. :-)

I don't think it should be too difficult to formalise the representation of braid groups onto the Temperley-Lieb algebras tho. We can define the TL-algebras diagrammatically or via vN algebras (which I think is already in mathlib?). We can also then introduce a lot of quantum algebra like the Jones-Wenzl idempotents and other useful results. I haven't tried doing this yet tho, this is just off of the top of my head

[Monica]

Kyle Miller said:

Starting off just by defining the braid groups via Artin's presentations would be a good exercise.

Here's some code from Zulip:

import data.zmod.basic
import group_theory.presented_group
import group_theory.free_group
import data.equiv.mul_add
import algebra.group_power

def alt {S : Type*} : ℕ → S → S → free_group S
| 0 _ _ := 1
| (n+1) s t := free_group.of s * alt n t s

def artin_tits_rels (S : Type*) (m : S → S → ℕ) :
  set (free_group S) :=
{g | ∃ s t, g = (alt (m s t) s t)⁻¹ * (alt (m t s) t s)}

/-- Artin-Tits groups.  Traditionally we require that
`∀ s t, m s t = m t s` but the hypothesis isn't used in the definition. -/
abbreviation artin_tits (S : Type*) (m : S → S → ℕ) :=
presented_group (artin_tits_rels S m)

abbreviation braid_group (n : ℕ) :=
artin_tits (fin (n - 1))
  (λ i j, if abs ((i : ℤ) - j) = 1 then 3 else 2)

I like the definitions from here more: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/braid.20group/near/249146660

[Monica]

Kyle Miller said:

It's less clearly about knots, though, since you need Markov's theorem (every knot is the closure of a braid, and two braids represent the same knot iff they're related by Markov moves)

it should be easy to prove Alexander's theorem (i.e., every link is ambient isotopic to a braid closure). As for Markov's theorem, proving that every braid is Markov equivalent if their braid closures are Reidemeister equivalent is a lot less clear how to formalise. It would be a lot of work, but it seems worth it

[Monica]

Also, @Scott Morrison / @Kyle Miller, can I get write access to mathlib. Github username is @themathqueen

[Scott Morrison]

@Monica, invited!

[Scott Morrison]

"Defining the TL-algebra diagrammatically" is unfortunately harder than it sounds. :-)

[Scott Morrison]

We can certainly define the TL-algebras by generators and relations, and we should start with that. Getting them as a monoidal category would be really lovely, however.

[Kevin Buzzard]

@Monica Omar this looks like a super project. It's certainly in scope for mathlib, there are people in the community who know enough about it to help out, there's plenty to do and it's mathematically interesting. Please feel free to ask here any questions you may run into, people are very happy to help out with questions, however basic.

[Kevin Buzzard]

One observation is that if you write a ton of code with definition X and only then start showing it to people, you might get a comment of the form "well yes, the Lean issues you're running into here are well-known to the experts and we now know that the best way to get around them is to actually make mathematically equivalent definition X' instead, meaning that you will have to refactor everything". So run key definitions past the community early before building an API for them.

[Jireh Loreaux]

@Monica Omar von Neumann algebras are defined in mathlib thanks to Scott, but there is no theory developed yet. We have a lot of work to do before we can do anything interesting with von Neumann algebras.

[Kyle Miller]

Scott Morrison said:

"Defining the TL-algebra diagrammatically" is unfortunately harder than it sounds. :-)

At least it's not so hard to define the TL-category diagrammatically in Mathematica ("diagrammatically" as in elements are linear combinations of the combinatorial data of diagrams). https://github.com/kmill/planalg/blob/master/Planalg/Planalg.wl#L338

image.png

(That's following the convention in https://arxiv.org/abs/1503.00384)

[Miguel Marco]

I just run into this conversation, and it got me interested. What is the status of this project?

I am interested in low dimensional topology in general, and I found that there is very little done in the "pure topological flavour" (in this case, it would be to see the knots as isotopy classes of embeddings of $\mathbb{S}^1$ in $\mathbb{S}^3$). I couldn't even find Seifert-VanKampen theorem. Do you think it could be doable? The general idea of the proof is easy, but I fear there would be a lot of devil in the details.

[Chinmaya Nagpal]

Miguel Marco said:

I couldn't even find Seifert-VanKampen theorem.

I'd be happy to help if someone decides to work on this.

[Miguel Marco]

I could be interested, but I have no experience contriburtng to mathlib whatsoever. And also, I cannot dedicate much time.

[Patrick Massot]

We don' t have Seifert-van Kampen yet. We do have the fundamental groupoid (and the fundamental group). People are working on covering space theory, see eg https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/winding.20number.

[Patrick Massot]

One difficulty is that Bourbaki's algebraic topology book is not yet translated into English, so we don't have a good formalization source that everybody can read.

[Ruben Van de Velde]

Step 1: learn French

[Miguel Marco]

Is there a reason to follow precisely Bourbaki instead of any other reference?

[Ruben Van de Velde]

I don't know about this case in particular, but I understand Bourbaki's style is halfway to formalized mathematics already, and as such tends it tends to be one of the better sources

[Suryansh Shrivastava]

(deleted)