Dimension of Boolean valued lattices and rings (Q1080938)

This paper is giving a constructive proof of the fact that the Krull dimension of a ring of polynomials on a von Neumann regular ring is always one. The idea is to use Pierce's representation to reduce the problem to the case of a field in a topos of sheaves. Here constructive means ''without using the axiom of choice or the excluded middle''; the author concludes that this proves the result in an arbitrary topos. Before drawing this conclusion, the author should probably pay a more careful attention to the finiteness arguments which are involved: this is a point where constructive set theory differs from topos theory. In particular nothing indicates if ''finite'' means ''Kuratowski finite'' or ''image of a finite cardinal''; probably the existence of finite cardinals is implicitly assumed in the base topos since also the free Boolean algebra on a distributive lattice is considered (which requires the existence of a natural number object).