Skip to main content
44 events
when toggle format what by license comment
Feb 25, 2019 at 12:34 comment added Andrej Bauer @user2357112: sorry, my brain insists that all usernames of the form userXYZ represent the same generic "internet user". It was meant for the other user, yes.
Feb 25, 2019 at 1:25 comment added Michael Hardy To what extent might answers to this question be relevant to bijections in settings other than those we would normally call combinatorics?
Feb 23, 2019 at 20:05 comment added user2357112 @AndrejBauer: Did you mean to reply to me or to user36212 there? Your reply sounds more applicable to user36212's comments.
Feb 23, 2019 at 19:26 comment added Andrej Bauer I don't understand what you mean. What do I want to say about what?
Feb 23, 2019 at 12:07 comment added Monroe Eskew Say you wrote something like, “let us call a bijection explicit if it is blah. Theorem: for all explicit bijections $f$, blah.” Then I’d have no objection. So what do you want to say about them?
Feb 23, 2019 at 11:17 comment added Andrej Bauer In any case. You are providing criteria for what an explicit bijection is or is not. You are not providing any arguments why we should not attempt to formalize the notion. In fact, I don’t see how a mathematician could ever object to making mathematical practice more precise.
Feb 23, 2019 at 11:15 comment added Andrej Bauer @user2357112 that is very weak indeed. By that reasoning we shouldn’t have formalized the notion of continuous map. Or homomorphism. Or anything of which there can be several instances.
Feb 23, 2019 at 10:53 comment added user36212 And maybe another (weak) argument against formalising the notion is the following: often it's interesting to have several different explicit bijections between the same sets, which are useful for different things - so at least, any formalism should be something which explains this.
Feb 23, 2019 at 10:51 comment added user36212 I don't think 'explicit bijection', any more than 'explicit construction', is or should be well defined; usually when people publish an 'explicit bijection' they mean something which is useful for some specific purpose. It might well be that to actually compute the bijection one needs to solve some hard problem, but nevertheless we agree to call it an 'explicit bijection' because it is useful. On the other hand, a bijection or construction involving brute-force search on a log-sized set (which is polynomial-time) might not count.
Feb 23, 2019 at 9:49 comment added Andrej Bauer Sure, there might be several. Are you suggesting I ask the question several times? :-)
Feb 23, 2019 at 9:06 comment added Monroe Eskew So it could be, as in the above mentioned case, that there’s no single satisfactory formalization of an intuitive notion, but several options having different mathematical applications.
Feb 23, 2019 at 9:00 comment added Monroe Eskew The more general term “explicit function” has been used more widely and for a longer time. Eventually we thought about what this really means, and it wasn’t so clear. There were different formalizations that had different uses. On the one hand, we had things that could be generated by some ad-hoc but traditional collection of “elementary functions.” Then there is the contrast with “implicit functions,” and the useful theorem of analysis, which nonetheless has little to do with things being “explicit” in the natural language sense of “fully and clearly expressed.”
Feb 22, 2019 at 21:51 answer added Timothy Chow timeline score: 7
Feb 22, 2019 at 17:16 comment added Andrej Bauer @MonroeEskew: It looks like you are dead set on disputing the usefulness of the notion, but I would argue that it is always worthwhile formalizing a notion which is widely used, mostly agreed upon and recognized as important by a community. People publish papers in which the main result is to give an explicit bijection where it was already known that a bijection exists. Even only a partially satisfying answer might bring a new insight. Of course, I can't guarantee that it will, but history is on my side.
Feb 22, 2019 at 16:53 comment added Monroe Eskew @JohnColeman, This phrase “explicit bijection” strikes me as akin to “direct proof” or “geometric argument.” The OP even includes a link to homework exercises as an example of usage. So while it may have some heuristic or pedagogical import, I don’t see the motivation for formalization without an application in mind.
Feb 22, 2019 at 14:22 comment added YCor I added the logic and category tags. I don't mean that the question ought to be tackled within either context, but in both model theory and category this is a natural question where contributors can help.
Feb 22, 2019 at 14:19 history edited YCor
edited tags
Feb 22, 2019 at 13:57 answer added Andreas Blass timeline score: 12
Feb 22, 2019 at 12:43 comment added John Coleman @MonroeEskew But this isn't "just for fun" -- explicit bijection is an important albeit informal notion in combinatorics. There very well might be mathematical significance in formalizing such a notion, in much the same way that e.g. defining elementary functions as (one possible) formalization of "closed form" function definitions is manifestly a mathematically fruitful definition.
Feb 22, 2019 at 12:37 comment added Monroe Eskew @JohnColeman I disagree with the idea of coming up with definitions “just for fun.” When I write mathematics, I feel quite wrong if I define something new and the definition doesn’t cause any ink to be saved in a proof.
Feb 22, 2019 at 12:34 comment added David Roberts Devil's advocate: Godel proved that if we accept the axiom of constructibility in ZFC, then we can create an explicit formula that well-orders the real numbers mathoverflow.net/q/6593/4177
Feb 22, 2019 at 12:33 comment added John Coleman @MonroeEskew Mathematicians like to formalize informal notions. A pay-off could be that (perhaps) down the line someone could use a formal definition to e.g. show that for some combinatorial objects of the same cardinality an explicit bijection can't be found. Who knows? I see no reason to censor the question itself.
Feb 22, 2019 at 12:25 comment added Monroe Eskew I’m sorry, but I don’t see what is the mathematical content of this question. You want a precise definition of something which is used a lot but probably just for rhetorical emphasis (exPLIcit!). Why?
Feb 22, 2019 at 12:06 answer added Peter LeFanu Lumsdaine timeline score: 21
Feb 22, 2019 at 11:34 answer added Martin Rubey timeline score: 9
Feb 22, 2019 at 11:30 answer added Adam P. Goucher timeline score: 15
Feb 22, 2019 at 9:41 history edited Monroe Eskew
Added tag
Feb 22, 2019 at 8:46 answer added Christian Stump timeline score: 2
Feb 22, 2019 at 8:43 comment added Dima Pasechnik it might be better to take different to the classical bit-wise computational complexities, e.g. the "real RAM model": en.wikipedia.org/wiki/Blum%E2%80%93Shub%E2%80%93Smale_machine
Feb 22, 2019 at 7:48 history edited Andrej Bauer CC BY-SA 4.0
added 440 characters in body
Feb 22, 2019 at 5:21 comment added user2357112 For example, if I show an injection from A to B and an injection from B to A, then invoke the Schröder–Bernstein theorem to prove the cardinalities are equal, I am not using an explicit bijection. I've just shown that a bijection must exist. On the other hand, Schröder–Bernstein can be proved by constructing a bijection, and if I embed the construction into my proof directly and point to the resulting bijection, then I am using an explicit bijection. This bijection is explicit in the second proof, and it may be considered implicit in the first proof, but it's the same bijection either way.
Feb 22, 2019 at 5:21 comment added user2357112 I think this question makes a mistake about what the terminology means. Specifically, the "explicit" in "explicit bijection" isn't a property of the bijection itself. It's more like the "explicit" in "explicit nudity"; a bijection (or nudity) is explicit if we show it, rather than implying that a bijection (or nudity) must exist. The same bijection may be explicit in one proof or left implicit in another.
Feb 22, 2019 at 4:20 comment added user2357112 Why would you reject bit-sequence-based bijections? Those seem pretty explicit to me.
Feb 22, 2019 at 2:25 comment added Dylan Wilson Species do seem to be relevant. Presumably one would first ask to work with a family of combinatorial objects A_S for finite sets S and be tasked to find bijections A_S—>B_S functorial under automorphisms of S (ie permutations). Maybe the families have further structure amongst the sets of different sizes, eg maps A_S \times A_T—->A_{S+T}, in which case you might ask your bijections to respect this structure too.
Feb 22, 2019 at 0:32 comment added Steven Gubkin I have always wanted to learn about combinatorial species, but have never taken the time. My impression is that this theory could provide one answer to your question. Are you already familiar with it?
Feb 21, 2019 at 23:14 comment added Sam Hopkins Sounds like a good topic for a FPSAC talk :)
Feb 21, 2019 at 22:55 comment added Dima Pasechnik Pak's paper I cited argues that an algorithm that computes a bijection as in 1) has to be "fast" in a well-defined sense.
Feb 21, 2019 at 22:29 comment added Michael Albert My feeling is that when one writes "We define an explicit bijection ..." one means a bijection whose computation depends only on the description of an individual object in the domain -- in particular the main dichotomy for me is between explicit and recursively defined bijections. Having said all that I'll also say that I'd be happier if "explicit bijection" were left as an informal notion! Especially since I suspect that I've been entirely inconsistent in its use.
Feb 21, 2019 at 22:18 answer added gowers timeline score: 28
Feb 21, 2019 at 22:11 comment added Dima Pasechnik in math.ucla.edu/~pak/papers/ICM-paper9.pdf one finds some studies on the subject.
Feb 21, 2019 at 21:59 comment added Andrej Bauer You know how they are, forcing things left and right.
Feb 21, 2019 at 21:57 history edited Andrej Bauer CC BY-SA 4.0
added 2 characters in body
Feb 21, 2019 at 21:52 comment added Andrés E. Caicedo That is one silly set theorist.
Feb 21, 2019 at 21:44 history asked Andrej Bauer CC BY-SA 4.0