Analogue of Kock-Lawvere axiom for power series rings?

Question

The Kock-Lawvere axiom for a topos $\mathcal{E}$ states that given a specified commutative ring object $R \in \mathcal{E}$, for all local Artinian $R$-algebra objects $A \in \mathcal{E}$, the morphism

$$A \to R^{\mathrm{Spec}_R(A)}$$

is an isomorphism.

Now, we don't assume that the Kock-Lawvere axiom holds for the topos $\mathcal{E}$. Assuming that in the topos $\mathcal{E}$ one could define the power series ring $R[[\epsilon]]$ of $R$ as the inverse limit of the local Artinian $R$-algebras $R[\epsilon]/(\epsilon^n)$ and the formal spectrum $\mathrm{Spf}(R[[x]])$ of $R[[\epsilon]]$ as the inductive limit of the spectra $\mathrm{Spec}(R[\epsilon]/(\epsilon^n))$, is it consistent to assume that the morphism

$$R[[\epsilon]] \to R^{\mathrm{Spf}(R[[\epsilon]])}$$

is an isomorphism?

Answer 1

Yes, it is consistent, it even follows from the Kock-Lawvere axiom, as follows.

We defined $\mathrm{Spf}(R[[\epsilon]]) := \mathrm{colim}_n \mathrm{Spec}(R[\epsilon]/(\epsilon^n))$, so we have $$R^{\mathrm{Spf}(R[[\epsilon]])} = R^{\mathrm{colim}_n \mathrm{Spec}(R[\epsilon]/(\epsilon^n))} = \mathrm{lim}_n R^{\mathrm{Spec}(R[\epsilon]/(\epsilon^n))}$$ by the universal property of the colimit. By the Kock-Lawvere axiom we have $R^{\mathrm{Spec}(R[\epsilon]/(\epsilon^n))} = R[\epsilon]/(\epsilon^n)$, so we get exactly $\mathrm{lim}_n R[\epsilon]/(\epsilon^n)$, which is how we defined $R[[\epsilon]]$.

(However, I might misunderstand you question. Do you ask for a topos where the Kock-Lawvere axiom does not hold but the morphism in question is still an isomorphism?)