Is it ok to say 'characteristic 0'?

[felixwellen]

There is one way to ask our base ring R to be of characteristic 0: Define the map $\iota:\mathbb{N}\to R$ and then ask that $\prod_{n:\mathbb{N}}\neg(\iota(n+1)=0)$ holds.

But this is a bit suspicious in light of this excerpt from @iblech 's thesis:

this might be problematic. So one concrete question is: Can we show that $R$ is not of characteristic 0 as defined above?

[dwarn]

$R$ is of characteristic 0 if and only if non-zero integers are invertible in $R$. Semantically, in the Zariski topos of a ring $k$, this is validated if $k$ contains $\mathbb Q$. So it can happen; we cannot disprove it. Constructively you cannot show that there are more functions $R \to R$ than elements of $R$ (I guess you would need a surjection $R \to 2$ to replay Cantor's argument), nor can you show that $R[T]$ bijects with $R$. The excerpt just demonstrates that classical logic is incompatible with the synthetic axioms.

[felixwellen]

The excerpt just demonstrates that classical logic is incompatible with

Ah - thanks! I misunderstood that.

[felixwellen]

Closing (don't think we have to write this anywhere - we make the assumption already in diffgeo)