Timeline for Constructive approach to complete intersections
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 24, 2017 at 10:45 | comment | added | Franka Waaldijk | For discrete fields and finitely generated polynomial rings, my (very non-expert) picture is that existence of prime ideals, injective envelopes etc. (the stuff that implies the ultrafilter lemma or AC when stated in full generality) is basically constructive. Gröbner bases help me to understand this, since essentially we only have to test finitely many candidates (don't quote me on this, it is a mental picture :-) ). | |
| May 24, 2017 at 10:32 | comment | added | Franka Waaldijk | Fred Richman might be the person to ask. His paper The regular element property seems to touch on your question, and it also refers to the useful book 'A course in constructive algebra' by Mines, Richman and Ruitenburg. (You'll notice the same preference for starting with discrete fields, you probably can disregard the less important constructive 'issues' such as not always knowing whether $k$ equals $\mathbb{Q}$ or perhaps $k=(\mathbb{Q},i)$ (with $i^2=-1$). | |
| May 23, 2017 at 22:50 | comment | added | Franka Waaldijk | If that is so, then for discrete fields you may already have a constructive proof, no? Because the Buchberger algorithm is finite with decidable output, and (since it cannot contradict classical theory) it is impossible that this output will not fulfill your theorem, so therefore it must fulfill your theorem... Not very elegant perhaps, but constructive nonetheless. | |
| May 23, 2017 at 21:33 | comment | added | Neil Strickland | @FrankWaaldijk For any given sequence $f_1,\dotsc,f_n$, I can in principle find a Groebner basis and use it to compute everything. However, I would like a proof that works for all possible sequences, and I do not see any way to use Groebner bases for that. | |
| May 23, 2017 at 19:38 | comment | added | Franka Waaldijk | Also, your question calls to mind the wonderful effectivity of Gröbner bases, when dealing with equations and polynomial elimination. But I'm quite unsure if that is what you could mean (can't hurt to mention it I hope). | |
| May 23, 2017 at 19:32 | comment | added | Franka Waaldijk | [A lot of what you write is unfamiliar to me...but in principle there is much constructivity in algebra.] For my Master's thesis I wrote up how one can construct the complex $p$-adic numbers $\mathbb{C}_p$, by first extending the $p$-adic valuation on $\mathbb{Q}$ to the algebraic numbers (result is called $ \mathbb{A}_p$), and then forming $\mathbb{C}_p$ as the metric completion of $ \mathbb{A}_p$. This illustrates a possible strategy: first restrict your question to discrete fields (decidable equality of elements), and then try to lift answers to the completion field. | |
| May 22, 2017 at 20:42 | comment | added | Mohan | May be an alternate procedure is as follows. Your condition says $R/I$ is a finite dimensional $k$-vector space. First, you have to find a basis of this constructively. Then an argument used to prove Weierstrass preparation theorem will show that this basis can be lifted (this is not quite constructive, but at least successively improving the basis upto higher and higher oreder) to a basis of $R$ over $S=k[[u_1,\ldots,u_n]], u_i\mapsto f_i$. This gives the exactness of the Koszul. | |
| May 22, 2017 at 9:12 | comment | added | Neil Strickland | @AndrejBauer I looked at that book before, and did not find anything directly useful. I just looked again more closely and I now think that the discussion of the Bezout matrix on pages 337 and 366 is potentially relevant. However, I think that a substantial amount of additional work would be needed to answer my question. | |
| May 22, 2017 at 8:41 | comment | added | Andrej Bauer | Did you look at Lombardi and Quitté's book on constructive algebra (arXiv version here)? Your question sounds like something they may have done. | |
| May 22, 2017 at 8:11 | history | asked | Neil Strickland | CC BY-SA 3.0 |