Timeline for Alternate proofs of Hilberts Basis Theorem
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 11, 2016 at 21:26 | answer | added | Manny Reyes | timeline score: 3 | |
| Feb 10, 2016 at 14:09 | answer | added | Ingo Blechschmidt | timeline score: 10 | |
| Nov 7, 2015 at 22:52 | answer | added | eric | timeline score: 5 | |
| Nov 7, 2015 at 22:19 | comment | added | Georg Lehner | @ToddTrimble : Yes that was exactly what I was wondering about. | |
| Nov 7, 2015 at 22:01 | comment | added | Todd Trimble | Thanks, Georg, for that lead -- I'll see if I can get a hold of it. I'm sorry, though, I'm not clear what you're asking; literally the answer is yes, take any non-Noetherian ring in the topos $Set$. Did you mean to ask whether I knew of a topos where the Hilbert basis theorem fails? (I don't; the question might be very interesting for toposes satisfying the Presentation Axiom or some other weak choice principle some constructive mathematicians find acceptable. Toby Bartels might know more.) | |
| Nov 7, 2015 at 21:53 | comment | added | Georg Lehner | @ToddTrimble : That's pretty interesting. Are you aware of any toposes in which the posets of ideals of a ring is not wellfounded? As to your question of a constructive proof, there's Jon Tennenbaums dissertation. Sadly, I can't access it. | |
| Nov 7, 2015 at 21:46 | comment | added | Todd Trimble | @QiaochuYuan Of course the notion of 'Noetherian' is closely connected with the notion of well-foundedness (the poset of ideals under reverse inclusion is well-founded), and the good notion of 'well-founded' from a constructive viewpoint is that it permits structural induction (as set out here: ncatlab.org/nlab/show/well-founded+relation#definition). So I'd be interested in 'constructive' proofs that take the working definition to be the structural induction one. | |
| Nov 7, 2015 at 19:41 | comment | added | eric | That's the reason I was slightly coy when I claimed my proof was constructive. For example in the proof I know I define an increasing sequence of ideals in $R$ and argue that the union is finitely generated because my definition of "Noetherian" is "all ideals are finitely generated". If you use another one then already there are issues with dependent choice. In fact the point I guess I'm making here is that there issues with DC even in the equivalence of the standard definitions of Noetherian so one might initially have to be careful as to exactly what question is being asked. | |
| Nov 7, 2015 at 18:28 | comment | added | Qiaochu Yuan | One problem is that the definition of Noetherian is itself not very constructive... there's some previous discussion of this on MO and math.SE but I can't find the one I had in mind. | |
| Nov 7, 2015 at 16:50 | comment | added | Todd Trimble | Could someone link to a proof that they feel is 'constructive'? The standard proof I know of I would consider non-constructive (proof of existence by contradiction, axiom of dependent choice in one form or another). I was trying to think about this a couple of months ago and found it quite bedeviling. | |
| Nov 7, 2015 at 16:39 | history | edited | Georg Lehner | CC BY-SA 3.0 |
added 1 character in body
|
| Nov 7, 2015 at 16:38 | comment | added | Georg Lehner | You are right. It does not follow immediatly. I wrote that thinking an ideal in $R[X]$ is also an ideal in $R[[X]]$ under the inclusion, but this is wrong. | |
| Nov 7, 2015 at 16:15 | comment | added | eric | The proof I teach in class is what I thought was "the standard proof" but it's also constructive (for some interpretation of the word). You look at the increasing sequence of ideals generated by leading terms of polys of degree n in your ideal I of R[x] as n goes to infinity and then follow your nose. Why is the second assertion stronger than the first, by the way? Clearly each implies the other in the stupid sense that each one is true, but is there an easy way of deducing the first from the second? | |
| Nov 7, 2015 at 12:16 | history | made wiki | Post Made Community Wiki by Todd Trimble | ||
| Nov 7, 2015 at 11:56 | history | asked | Georg Lehner | CC BY-SA 3.0 |