A^1 does not satisfy plain choice

[MatthiasHu]

We could formalize that not every surjection X -->> A^1 admits a section. Namely, for every element x of A^1 = R, x is invertible or 1 - x is invertible (because R is local), but there does not exist a function A^1 --> Bool choosing between the two options.

Proof sketch: Given such a choice function, A^1 is a disjoint sum of two subsets, one containing 1 and the other 0. This means that in R[X] = (A^1 --> A^1), there are orthogonal idempotents p and q, that is p + q = 1, pq = 0, such that p(0) = 0, q(1) = 0. So p = X r and p^2 = p, so X r^2 = r, but then by induction r = 0. This contradicts q(1) = 0.

[felixwellen]

Yes!
We could start by formalizing "p(0)=0 => p=Xr" - that should not be hard with the coefficient representation. Other than that, I don't see any new algebra lemmas we need.

[MatthiasHu]

As a corollary, we can show that any function f : A^1 --> Bool is constant! The above proof sketch shows that f(0) = f(1), and for any two different points p, q of A^1, there is an automorphism of A^1 sending 0 to p and 1 to q. And finally, every point of A^1 is different from 0 or different from 1, so f(p) = f(0) for every p.

[MatthiasHu]

It is probably better to prove first that every function A^1 --> Bool is constant: If the polynomial p is idempotent and p(0) = 0, then p = X r and by induction p is divisible by X^n for every n, so p = 0. Then from this it follows that A^1 does not satisfy choice.