Is there a constructive proof that in four dimensions, the PL and the smooth category are equivalent?

Question

Summary

Famously, the categories of 4-dimensional smooth manifolds and 4-dimensional piecewise linear manifolds are equivalent. Is there a constructive proof for this theorem or does it depend on the axiom of choice?

Background

A smooth manifold is a manifold with a smooth atlas, that is, an atlas with smooth transition functions. These should be fairly well-known. Piecewise linear manifolds are a bit less familiar. One can define them as manifolds with piecewise linear transition functions.

The conventional proof

As far as I understand, the conventional proof of the theorem passes through a third category: The category of piecewise smooth manifolds. The proof then runs roughly as follows:

1. There are obvious faithful functors from smooth manifolds, and piecewise linear manifolds, into piecewise smooth manifolds. After all, every smooth function is piecewise smooth and every linear function is smooth (thus every piecewise linear function is piecewise smooth).
2. To show that the two functors are full and essentially surjective, one must show that every piecewise smooth function is globally smoothable, and piecewise linearisable, respectively.
3. Both functors are full, faithful and essentially surjective, thus equivalences. Composing two equivalences gives an equivalence again.

The question

The final, small, third step of the proof is not constructive. A constructive equivalence is given by a functor, a weak inverse, and natural isomorphisms witnessing the inverse laws. To define such a weak inverse for a full, faithful and essentially surjective functor, one typically needs the axiom of choice, which is not available in constructive mathematics.

Can one still prove the theorem constructively? This would be somewhat weird because it would, in the end, give you an algorithm (however convoluted) how to construct a PL structure from a smooth structure, and vice versa.

But the other option feels even more alarming: Is there maybe no constructive proof? Is the theorem maybe equivalent to the axiom of choice, or is it weaker? Are there constructive models of mathematics where the theorem is false?

Answer 1

In this, as in much constructive analysis/algebra, the issues fall into two aspects:

1. general formalities of how to set up the structures involved;

2. the specific constructive content of the problem at hand.

This is a half-answer, addressing just the first aspect. If you’re already experienced with constructive mathematics, then this is probably familiar and of less interest than the second side (which is addressed a bit in comments). On the other hand, if you are familiar with algorithmic/computational analysis, but less so with the general development of mathematics in constructive logic, this is probably helpful.

Essentially, in developing maths constructively, one almost always wants to follow the design principle Don’t take quotients, and don’t impose mere existence conditions; include extra data/witnesses in definitions, and then if necessary, explicitly carry around the equivalence relation which classically you would have quotiented by (or make sure it’s retained as e.g. isomorphisms in a category). If you follow this principle, then if you have algorithms for computing the constructions you have in mind, you will usually be able to put the algorithms together into functions/homomorphisms/functors as desired.

In your specific case, this occurs in e.g. the definitions of a smooth manifold. There are various classical definitions, but the key existence condition they all contain is that the atlas is covering, i.e. for every point, there is some chart around that point. If you use such a definition, then it will be difficult (probably impossible) to get a function taking such a smooth manifold to its piecewise-linearisation, since firstly you will need to choose some chart around each point, and secondly, different choices may produce different (even non-isomorphic) piecewise-linearisations.

However, if you take the definition of smooth manifold to include a choice of chart around each point (and similarly for the other notions of manifold, and similarly set up all prerequisite definitions in suitably constructive ways), then it seems likely that the algorithms mentioned in comments should assemble into the desired equivalence of categories. In particular, the “inverse” functors whose existence you worry about will be unproblematic, because the proof of “essential surjectivity” won’t just be an existence proof — it will be a construction of a piecewise linear manifold equivalent to a given piecewise smooth manifold.

Note that such definitions, with extra data included, are classically equivalent to the classical definitions, in the sense of producing equivalent categories of manifolds, since two manifolds-with-extra-data differing just in the extra data will end up isomorphic in the category of manifolds-with-extra-data.

(An entirely different approach, rather less well-established, would be to work in homotopy type theory/univalent foundations, where one can often use quotients while remaining constructive, essentially because you can quotient everything. The problem with quotients/existence in traditional constructive mathematics can be seen as the fact that you can’t “get out of a quotient” using AC, as you can in classical mathematics, and so if you take a quotient one set/class, you will need to take quotients of other sets/classes you intend to map it into — but then you can’t always do that, because often for the class of objects of a category, the quotient you need would a homotopy quotient, which doesn’t exist at the level of sets/classes. In the univalent setting, this is fixed because you really can take the homotopy quotient of a type — and so you really can take quotients everywhere. In your example, this would show up in the constructions of the homotopy categories of manifolds: they would be Rezk-completions, so equivalent manifolds would become equal as objects of these categories; more carefully said, equalities between objects of these categories would correspond to equivalences of manifolds. So since the piecewise-linearisation is (as classically) unique up to canonical equivalence, it would be literally unique in this setting, and so would give a well-defined map from (piecewise) smooth to piecewise linear manifolds.)