2019-01-06 11:28:45 8 Comments

# 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:

- 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 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?

### Related Questions

#### Sponsored Content

#### 4 Answered Questions

### [SOLVED] Mathematics without the principle of unique choice

**2018-06-05 04:34:30****Mike Shulman****982**View**20**Score**4**Answer- Tags: lo.logic foundations constructive-mathematics

#### 1 Answered Questions

### [SOLVED] In what ways is ZF (without Choice) "somewhat constructive"

**2018-04-13 09:38:03****Gro-Tsen****660**View**16**Score**1**Answer- Tags: set-theory lo.logic axiom-of-choice constructive-mathematics

#### 4 Answered Questions

### [SOLVED] Gödel's speed-up from constructive to classical logic?

**2018-02-28 18:00:11****Ganon****780**View**8**Score**4**Answer- Tags: lo.logic constructive-mathematics

#### 1 Answered Questions

### [SOLVED] The concept of convex foliation

**2017-12-30 10:38:21****Ali Taghavi****167**View**6**Score**1**Answer- Tags: dg.differential-geometry smooth-manifolds convex-geometry foliations

#### 1 Answered Questions

### [SOLVED] Is it possible for a theorem to be constructive only in a non-constructive metatheory?

**2014-04-29 08:31:25****Zhen Lin****673**View**13**Score**1**Answer- Tags: lo.logic topos-theory proof-theory constructive-mathematics categorical-logic

#### 0 Answered Questions

### Did Kleene constructively prove Brouwer's axioms?

**2016-12-22 14:46:56****Frank'a Waaldijk****319**View**5**Score**0**Answer- Tags: lo.logic foundations constructive-mathematics intuitionism realizability

#### 4 Answered Questions

### [SOLVED] Constructive proof that a kernel consists of nilpotent elements

**2016-09-16 15:42:45****HeinrichD****876**View**17**Score**4**Answer- Tags: ac.commutative-algebra lo.logic tensor-products constructive-mathematics prime-ideals

#### 2 Answered Questions

### [SOLVED] Do smooth manifolds admit linear atlases?

**2016-03-15 17:13:17****Alex M.****653**View**9**Score**2**Answer- Tags: dg.differential-geometry linear-algebra smooth-manifolds

#### 1 Answered Questions

### [SOLVED] Barr's theorem and constructivity?

**2013-09-15 14:18:43****Simon Henry****423**View**10**Score**1**Answer- Tags: lo.logic topos-theory constructive-mathematics

#### 4 Answered Questions

### [SOLVED] How can there be topological 4-manifolds with no differentiable structure?

**2011-03-10 12:02:34****gowers****9177**View**83**Score**4**Answer- Tags: differential-topology 4-manifolds

## 1 comments

## @Peter LeFanu Lumsdaine 2019-01-06 14:52:49

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

general formalities of how to set up the structures involved;

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

choiceof 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 quotienteverything.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 reallycantake 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 beRezk-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.)## @Mike Miller 2019-01-06 15:04:51

As an addition to your excellent answer more specific to this problem: it should probably be noted that if there is an equivalence of categories here, it is an equivalence of $\infty$-groupoids of PL homeomorphisms vs diffeomorphisms. It is unlikely that the corresponding 1-categories agree (asking for automorphism groups to be isomorphic, as opposed to mapping class groups). You similarly wouldn't expect an equivalence of categories between all continuous maps and all smooth maps, but would between the corresponding $(\infty,1)$-categories.

## @Peter LeFanu Lumsdaine 2019-01-06 15:15:01

@MikeMiller — absolutely, if you don’t quotient the smooth/pw-linear maps then you only get an equivalence of ∞-categories. I understood the original question to be implicitly speaking of the

homotopycategories, which is where you do classically get an equivalence of 1-categories.## @Nik Weaver 2019-01-06 15:44:36

I really like your formulation of "design principles". Well put.