Timeline for How to construct a constructive proof from a non-constructive proof using prime ideals?
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 22, 2016 at 0:20 | comment | added | Ingo Blechschmidt | @HeinrichD: I've been following this thread and your other one with much interest. I believe that the techniques explained in my notes indeed suffice to settle the other question; I'll try to write up an answer tomorrow. The key is to use that the structure sheaf of the spectrum of a reduced ring looks like a field from the internal point of view. Therefore finitely generated modules are not not free. | |
| Sep 19, 2016 at 12:57 | comment | added | HeinrichD | @IngoBlechschmidt: Your notes are very interesting. There you give a constructive proof of generic flatness for f.g. modules on reduced rings, which is "magically simple". What about f.g. algebras? This would answer mathoverflow.net/questions/250040 - thus I would appreciate if you answer there, if you have some ideas. | |
| Sep 16, 2016 at 11:11 | comment | added | Simon Henry | When you move to the constructive framework, the part involving Zorn lemma is somehow replaced by some 'topos theoretic magic' but the part involving algebra and localization of ring is still essentially the same. Unfortunately a complete treatement of the basic theory of the Zariski spectrum is in my opinion beyond the scope of my answer. that is why I was asking if someone have references. | |
| Sep 16, 2016 at 11:09 | comment | added | Simon Henry | @HeinrichD : I didn't say it was trivial ! basically what makes things work is the explicit construction of the structural sheaf in this constructive framework, which involve the same sort of work on localization of rings. It is not easy, but it is exactly the same kind of stuff as in the classical framework. If you think about it proving that an element of a ring is nilpotent if and only it belongs to all prime ideal is not a simple task (it involve manpulatin properties of localizations and Zorn lemma). (...) | |
| Sep 15, 2016 at 14:51 | comment | added | HeinrichD | ... or rather with radical ideals: $\sqrt{I^n+J^m}=\sqrt{I^n} \vee \sqrt{J^m} = \sqrt{I} \vee \sqrt{J} = \sqrt{I+J}=\sqrt{A}=A$. So the trick here seems to be that we do not work in the lattice of ideals, but rather in the lattice of radical ideals, where $\vee$ is not the sum of ideals, and the observation $\sqrt{I+J}=\sqrt{I} \vee \sqrt{J}$ (clear without calculation since left adjoints preserve colimits). | |
| Sep 15, 2016 at 14:43 | comment | added | HeinrichD | For a simple example, we can prove $I+J=A \Rightarrow I^n+J^m=A$ for finitely generated ideals $I,J$ (not for arbitrary ideals in this setting, right?) using the Zariski lattice: $D(I^n,J^m)=D(I^n) \vee D(J^m)=D(I) \vee D(J)=D(I,J)=D(1)=1$. Now it should be an exercise to produce from this a direct calculation with elements ... | |
| Sep 15, 2016 at 14:37 | comment | added | HeinrichD | ... assume that we didn't already know that these are ideals and pretend that they are just radical sets, we somehow have to prove the relation $D(a+b) \leq D(a) \vee D(b)$ for $D(a) := \sqrt{\langle a \rangle}$. For nilpotent $a,b$, this says exactly that $a+b$ is nilpotent. So it seems that this basic statement is necessary for the construction of the Zariski lattice (and probably, also in the construction of the Zariski locale), but with that lattice we can constructively prove more sophisticated statements. What do others think about this? | |
| Sep 15, 2016 at 14:35 | comment | added | HeinrichD | I haven't understood the localic or topos-theoretic point of view yet, but when we work with the Zariski lattice, the whole argument is circular, at least for my toy example. In a slide by Coquand, he defines the Zariski lattice of $A$ as the free distributive(?) lattice generated by symbols $D(a)$, $a \in A$ modulo the relations $D(0)=0$, $D(1)=1$, $D(ab)=D(a) \wedge D(b)$, $D(a+b) \leq D(a) \vee D(b)$. In order to prove that $D(a)=0$ holds iff $a$ is nilpotent, we need to realize this lattice more concretely, for example as the lattice of radical ideals of f.g. ideals of $A$. Even if we ... | |
| Sep 15, 2016 at 9:39 | comment | added | Simon Henry | @HeinrichD : You are correct. for the construction of spec A you should have a look to the reference to Makkai & Reyes given by Bas Spitters above and to Ingo's work. The details of the construction will answer all the questions of your first comment. Regarding how you extract concretely a low level proof with explicit algebraic manipulation for explicit example : It is theoretically possible by working internally in well chosen toposes, but it can become very tedious and I would not advise this method if this is the end goal ! | |
| Sep 15, 2016 at 9:27 | comment | added | Ingo Blechschmidt | Some more examples of the technique explained by Simon are in Section 11.4 of these rough notes of mine. | |
| Sep 15, 2016 at 8:17 | comment | added | HeinrichD | @SimonHenry And how to write down this proof concretely with elements for some given commutative ring? Do we get the equational proof (a)? What about the toy universal example $\mathbf{Z}[x,y]/(x^2,y^2)$? | |
| Sep 15, 2016 at 8:15 | comment | added | HeinrichD | @SimonHenry Thank you your comments. I now realize that you didn't mean "not in any $I$", but rather "nowhere in $I$" (which seems to refer to the language internal to the topos of sheaves on $\mathrm{Spec}(A)$). Can you give a precise definition of the locale $\mathrm{Spec}(A)$ and its structure sheaf (or a reference)? Is $I$ defined to be the sheaf of invertible sections? If yes, how to prove $x+y \in I \Rightarrow x \in I \vee y \in I$? (This seems to be the statement that the sheaf is a local ring object). How to prove that $x$ is nilpotent if and only if $x$ does nowhere lie in $I$? | |
| Sep 14, 2016 at 22:47 | comment | added | Simon Henry | So yes by using the universal example and the fact its operation are nice and computable you can get (basically by using the above argument internally in some form of effective topos) that $k$ will be a computable function of $n$ and $n$, but the proof being relatively high level it will be hard to compute this function (I have no idea of even the order of the result)... | |
| Sep 14, 2016 at 22:44 | comment | added | Simon Henry | well the only reason I saw such a proof produce $k$ as a function of $m$ and $n$ is because you can apply it to $\mathbb{Z}[x,y]/(x^n,y^m)$ and actually get a $k$ that work for all ring by universality. but as long as you don't apply it explicitly to that ring you are not going to get an explicit and "computable" value of $k$" : you get such a value if you start from a ring that is "computable" in some sense, which is the case of the ring $\mathbb{Z}[x,y]/(x^n,y^m)$ | |
| Sep 14, 2016 at 22:13 | comment | added | user44143 | Of course it depends on the ring and the element...but a constructive proof that x^m=y^n=0 implies (x+y)^k=0 can always be unwound to exhibit k as a function of m and n (and perhaps some other characteristics of the elements or the ambient ring which are classically less relevant). The simple proof gives k=m+n-1, what function does this proof give? | |
| Sep 14, 2016 at 21:38 | history | edited | Simon Henry | CC BY-SA 3.0 |
deleted 78 characters in body
|
| Sep 14, 2016 at 21:37 | comment | added | Simon Henry | @HeinrichD : the relation with the works of Lombardi & others is as follows: what they call the Zariski lattice is the lattice of quasi-compact open subspace of the Zariski locale. now there is a duality (similar to stone duality) between distributive lattice and coherent locale given by associated to a coherent locale the distributive of quasi-compact open. The construction of Lombardi and the one I'm talking about are related by this duality and hence essentially equivalent. | |
| Sep 14, 2016 at 21:32 | comment | added | Simon Henry | @HeinrichD : the trick is that you don't prove it for any $I$ that you can construct in the topos of sets, but for the "universal I" that lives in the topos of sheaves over the Zariski spectrum, or equivalently of any $I$ in any topos. | |
| Sep 14, 2016 at 21:29 | comment | added | Simon Henry | @Matt F. : It doesn't produce any explicite value of $n$ (the proof don't show that the value of $n$ does not depends on the ring and the element...) | |
| Sep 14, 2016 at 21:12 | comment | added | HeinrichD | This seems to be the kind of answer I am looking for, but I don't understand it fully yet. You seem to say that $x$ is nilpotent iff $x$ is not contained in any $I$, but I cannot prove this constructively. Probably I have misunderstood something here. I don't understand the proof at the end, but hopefully I can when I have read the basics on the localic Zariski spectrum. I assume that this is the same as the Zariski lattice studied by Lombardi and others? Also, I second Matt's question. | |
| Sep 14, 2016 at 20:55 | comment | added | Bas Spitters | There is at least an explanation of these ideas in Makkai and Reyes, First Order Categorical logic Ch 9.3. | |
| Sep 14, 2016 at 19:47 | comment | added | user44143 | What value of n does this proof produce for which (x+y)^n=0? | |
| Sep 14, 2016 at 19:43 | history | answered | Simon Henry | CC BY-SA 3.0 |