Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Kock-Lawvere axiom in a Boolean topos

Madeleine Birchfield (Mar 01 2024 at 14:50):

In a Boolean topos, is it consistent to assume a local ring object $R$ such that for every Weil $R$-algebra $W$, the canonical morphism $W \to R^{\mathrm{Spec}_R(W)}$ is an isomorphism?

Max New (Mar 01 2024 at 14:54):

First thing I would try is to make $R$ the trivial ring

Reid Barton (Mar 01 2024 at 17:07):

The trivial ring isn't local though.

Madeleine Birchfield (Mar 02 2024 at 16:09):

Max New said:

First thing I would try is to make $R$ the trivial ring

Reid Barton said:

The trivial ring isn't local though.

The other interpretation of Max New's sentence is to prove that for any local ring $R$ in a Boolean topos, if $R$ satisfies the Kock-Lawvere axiom, then $0 = 1$, yielding a contradiction since by definition of local ring, $0 \neq 1$.

Not sure if that's what really meant by Max New since I feel like it's easier to just directly show that the evaluation map is not an isomorphism for all local rings by constructing a non-polynomial function from the nilradical of $R$ to $R$.

Madeleine Birchfield (Mar 02 2024 at 16:24):

If $R$ has decidable equality, then the set of nilradicals $D$ of $R$ also has decidable equality. This means that one can define any indicator function $D \to \{0, 1\} \subseteq R$ by case analysis, which is a non-polynomial function if it is not the constant function to $0 \in R$ or $1 \in R$.

Madeleine Birchfield (Mar 03 2024 at 02:20):

In general, I don't think the local requirement is necessary for the commutative ring $R$, only that $R$ is non-trivial with decidable equality. If $R$ is any commutative ring, then a Weil algebra $W$ is equivalent to the quotient of a polynomial ring $R[X]$ with $n$ generators $x_i \in X$, where $0 \leq i \lt n$ by a finite set of polynomials $f_j \in R[X]$ with cardinality $m$, where $0 \leq j \lt m$. The formal spectrum $\mathrm{Spec}_R(W)$ is the solution set of the polynomials $f_j$, which is a subset of $R$ and thus has decidable equality if $R$ has decidable equality.

Madeleine Birchfield (Mar 03 2024 at 02:40):

As a result, if $R$ is non-trivial, then there are non-polynomial indicator functions $\mathrm{Spec}_R(W) \to \{0, 1\} \subseteq R$ and so the evaluation map from $W$ to $R^{\mathrm{Spec}_R(W)}$ is not an isomorphism.