Is there a constructive proof that in four dimensions, the PL and the smooth category are equivalent?
$begingroup$
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?
lo.logic smooth-manifolds 4-manifolds constructive-mathematics pl-manifolds
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
$endgroup$
add a comment |
$begingroup$
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?
lo.logic smooth-manifolds 4-manifolds constructive-mathematics pl-manifolds
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
$endgroup$
4
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
4
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
5
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26
add a comment |
$begingroup$
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?
lo.logic smooth-manifolds 4-manifolds constructive-mathematics pl-manifolds
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
$endgroup$
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?
lo.logic smooth-manifolds 4-manifolds constructive-mathematics pl-manifolds
lo.logic smooth-manifolds 4-manifolds constructive-mathematics pl-manifolds
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
asked Jan 6 at 11:28
Manuel BärenzManuel Bärenz
2,5851138
2,5851138
4
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
4
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
5
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26
add a comment |
4
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
4
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
5
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26
4
4
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
4
4
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
5
5
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
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 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.)
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
$endgroup$
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "504"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f320205%2fis-there-a-constructive-proof-that-in-four-dimensions-the-pl-and-the-smooth-cat%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
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 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.)
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
$endgroup$
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
add a comment |
$begingroup$
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 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.)
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
$endgroup$
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
add a comment |
$begingroup$
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 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.)
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
$endgroup$
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 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.)
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
answered Jan 6 at 14:52
Peter LeFanu LumsdainePeter LeFanu Lumsdaine
8,72613871
8,72613871
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
add a comment |
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
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.
$endgroup$
– Mike Miller
Jan 6 at 15:04
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
@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 homotopy categories, which is where you do classically get an equivalence of 1-categories.
$endgroup$
– Peter LeFanu Lumsdaine
Jan 6 at 15:15
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
$begingroup$
I really like your formulation of "design principles". Well put.
$endgroup$
– Nik Weaver
Jan 6 at 15:44
add a comment |
Thanks for contributing an answer to MathOverflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f320205%2fis-there-a-constructive-proof-that-in-four-dimensions-the-pl-and-the-smooth-cat%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
4
$begingroup$
It is easy to construct such an algorithm with today's technology. Build a smooth triangulation (eg following Cairns 1961). This is necessarily a combinatorial triangulation (certainly true in dimension 4 as every triangulation is combinatorial following Perelman, but having never thought about it before it seems that smooth triangulations might always be combinatorial; it seems there should be problems making the maps immersions at the cone-point of the link otherwise). Now a PL structure is given by taking an atlas to be the collection of all PL homeomorphisms from Star(v) to $B^4$.
$endgroup$
– Mike Miller
Jan 6 at 13:06
4
$begingroup$
As for moving in the opposite direction, you need to talk about the homotopy theory of PL/O, as in the usual Hirsch-Mazur smoothing theory (conspicuously absent from the question, given that this is how the comparison goes...) I think this too is perfectly constructive, but feel free to look at their book and confirm for yourself.
$endgroup$
– Mike Miller
Jan 6 at 13:15
$begingroup$
Concerning the use of the word "constructive" in this question to denote the non use of Choice, it may be worth referring to this other question.
$endgroup$
– Gro-Tsen
Jan 6 at 15:17
$begingroup$
@Gro-Tsen, using Choice was the only thing I could spot as obviously non-constructive in the proof.
$endgroup$
– Manuel Bärenz
Jan 6 at 15:23
5
$begingroup$
I don't understand what is meant by a piecewise smooth manifold, since the composition of two piecewise smooth maps is not necessarily piecewise smooth. This has come up in MO before. Classically (in work of Whitehead) one uses the notion of piecewise smooth function to specify a useful compatibility condition between a smooth structure on M and a PL structure on M, then one shows that for every smooth structure there is a compatible PL structure, canonical up to a suitable equivalence relation. This is in any dimension.
$endgroup$
– Tom Goodwillie
Jan 6 at 15:26