search

felixwellen / synthetic-zariski

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos
MIT License
51 stars 6 forks source link

Do basic open propositions have choice? #34

Open felixwellen opened 4 months ago

felixwellen commented 4 months ago

A type $X$ has choice if $\prod{x:X}||B(x)||\to ||\prod{x:X}B(x)||$. We know that closed propositions and more generally every spectrum of a finitely presented local algebra has choice (and finite coproducts thereof). Open propositions should not have choice in general. I tend more to believing that basic open propositions do not satisfy choice, but I don't know if we have a result in either direction.

dwarn commented 4 months ago

Somehow the only obstruction to choice over affine schemes is the locality axiom, so I would look for a counterexample there. Specifically, let $x ,y : R$ be arbitrary ring elements, let $X$ be the basic open proposition $\mathrm{inv}(x+y)$, and let $B$ be the type $\mathrm{inv}(x) + \mathrm{inv}(y)$. Then we do have $X \to \lVert B \rVert$, but I'd expect we can show it's not true that $\lVert X \to B \rVert$ for all $x,y : R$.