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?
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:
- 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).
- 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.
- Both functors are full, faithful and essentially surjective, thus equivalences. Composing two equivalences gives an equivalence again.
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?