(combinatorial) surface classification theorem

Stream: maths

[Timothy Mou]

I'm wondering if there is a combinatorial proof of the surface classification theorem, presented in e.g. Munkres' Topology; that is, that every triangulated surface, represented by a "labelling scheme", can be normalized using a set of rewriting rules and shown to be equivalent one of the basic surface types.
This feels like something that wouldn't be too hard to formalize, but I'm not sure how one would write down some of the necessary definitions.

[Timothy Mou]

(deleted)

[Notification Bot]

This topic was moved here from #lean4 > (combinatorial) surface classification theorem by Mario Carneiro.

[Mario Carneiro]

(moved to #maths instead since we certainly don't already have it)

[Kevin Buzzard]

This would be a great project! I guess the hard part after that would be relating that combinatorial argument to a statement about topological spaces.

[Timothy Mou]

Yeah that would be probably more involved. To be clear, it's been a while since I studied topology and I wouldn't know how to write that stuff. But what motivated this question was just musing over how to write some of the basic definitions. For instance, a "labelling scheme" is just a word like $aba^{-1}b^{-1}$ where each label $a$ can appear as $a$ or "reversed" $a^{-1}$. A "proper labelling scheme" is a labelling scheme where each label appears exactly twice. Labelling schemes are also equivalent under cyclic rotation and some other rules.
So we could represent a labelling scheme as just a list, how would we define a proper labelling scheme?

[Yaël Dillies]

Can't you use docs#FreeGroup for this?

[Timothy Mou]

A "proper labelling scheme" is a labelling scheme where each label appears exactly twice.

For instance, $aba^{-1}b^{-1}$ is valid, but $abaab^{-1}$ is not. I don't see how free groups would enforce that.

[Kevin Buzzard]

Free groups would also not distinguish between $aa^{-1}$ and $1$, although maybe that's one of the rules?

[Junyan Xu]

Apparently, the combinatorial classification of surfaces has been attempted by Dehlinger and Dufourd in Coq:
Formalizing the Trading Theorem for the Classification of Surfaces (paywalled)
Formalizing the trading theorem in Coq
Formalizing generalized maps in Coq
Formal specification and proofs for the topology and classification of combinatorial surfaces (this paper was received in 2004 and published in 2014!)

Here are two excerpts from the last paper:
image.png
image.png

Apparently, they divide the classification into the normalization theorem (the first part, Section 8) and the trading theorem (the second part, Section 7), and from the earlier papers it seems they successfully accomplished the second part, but apparently they're not claiming they proved the whole theorem. Here are the description of the two sub-theorems from the second paper:
image.png
image.png
image.png

There's a link in the paper that is supposed to contain code, but it's dead now probably because J.-F. Dufourd has retired ...

They give five references other than the main reference (Griffiths' Surfaces, 1981), but Munkres isn't among them, so I'm not sure how well the argument translates (note that they work with open surfaces rather than closed). But they do say "the approach that we follow in this section is common to most textbooks on surfaces [35,23,43,28,25]".

Overall, I'd expect the combinatorial classification of surfaces to be easier than the combinatorial part of @Joseph Myers's proposed aperiodic monotile formalization.

See also some earlier discussion on Zulip in 2021.

[Kevin Buzzard]

Silvia De Toffoli talks specifically about the role which diagrams play in the classification of surfaces in her 2023 paper here, on the role of diagrams in mathematics. She points out that "removing the diagrams from the proof" (e.g. writing a diagram-free proof of the result in a textbook) would have epistemic and cognitive disadvantages. Formalisation perhaps solves the epistemic disadvantages; perhaps a more advanced theory of widgets would fix up the cognitive ones?

[Robert Maxton]

@Kevin Buzzard As it happens, I'm working on a Lean-compatible method of checking/generating diagrammatic proofs at the moment. Though it remains to be seen how long it'll take me... >.>;

(The primary use case is Penrose diagrammatic notation and tensor calculus, but on general principle I'm designing it to be compatible with any calculus that can be represented by a braided monoidal category, i.e. most string diagrams that don't assign data to the space between strings, though I'm leaving it open in case I do hit on a good way to represent such cases without massively adding to the technical scope of the project.)

[Kim Morrison]

@Robert Maxton, you know about homotopy.io, right?

[Robert Maxton]

Scott Morrison said:

Robert Maxton, you know about homotopy.io, right?

Nope, and thank you for the reference, it'll be very helpful when writing my other proofs!

However, when I play with it, I note quite quickly that it is very good at the thing it is designed for, and cannot be easily generalized to do other things, like, say, vector/tensor calculus. (At the least, the existing tensor calculus notation does not translate into string diagrams of this sort well; there probably is a way to create a new graphical calculus that does, but to some extent that would rather defeat the purpose.)

So I will have to continue with my original program... though I might borrow some ideas regarding implementing n-cells.

[Robert Maxton]

.... Hm. I take that back, I just didn't know how to use it right, I think. I'll have to play with it more.

[Kim Morrison]

Certainly all "Penrose" diagrams, calculus for monoidal/braided categories can be done in homotopy.io.

[Kim Morrison]

The big thing they are lacking is a way of saying "a functor consists of <a list of cells>", "a natural transformation consists of ..." and then to be able to say in a different file "let s be a natural transformation from F to G".

[Robert Maxton]

Yeah I tried to build a 3-cell in the way most obvious to me, saw that it didn't work, and assumed it was something fundamental ^.^;. But then I read the actual paper and saw they'd basically done Penrose in the appendix, so now I'm trying to figure out how to do that myself

[Robert Maxton]

Mm. Actually, upon playing with the model a bit more, I think I'm reverting to my original position, though now with a somewhat stronger basis lol

[Robert Maxton]

even setting up a ring structure is somewhat annoying, and the lack of an automatical 'dual' that isn't 'inverse' (in general, the fact that it has distinguished directions) makes it not ideal for a number of use cases
again, it's great for homotopy, and it's certainly possible to set it up for most of Penrose, but...
also, I don't see a great way of extending it to include e.g. derivatives

[Kim Morrison]

Could you say more about the type of diagrammatic proofs you're thinking about. I'm not sure how derivatives come in.

[Robert Maxton]

Well, for example, Maxwell's homogenous equations $\partial_\alpha \left(\eta^{\alpha\gamma}\eta^{\beta\delta}\partial_{[\gamma}A_{\delta]}\right) = J^{\beta}$ can be represented as
image.png
where the circles represent differentiation, circles with lines attached represent vector derivates (grad/div/curl), and square boxes represent $n$-tensors

[Robert Maxton]

and the thick horizontal bar represents antisymmetrization $x_{[\alpha} y_{\beta]} = x_\alpha y_\beta - x_\beta y_\alpha$