Real numbers in the topos of sheaves over the category of filters (Q5939909)

The author considers the topos \(\mathcal N\) of sheaves for the finite-cover topology on the category of filter bases on arbitrary sets --- a constructive version of the category of filters, first proposed by A.~Blass, which may also be described as the full subcategory of the pro-completion of the category of sets on objects whose transition maps are inclusions. In this category, any constant sheaf \(\Delta A\) has a canonical `non-standard extension' \(\ast A\); the author's main result identifies the object of Dedekind real numbers in the topos with the quotient \(F/I\), where \(F\) is the subring of finite elements of \(\ast{\mathbf R}\) and \(I\) is the ideal of infinitesimals. He also shows that \(\mathcal N\) inherits the axiom of dependent choices from the category of sets, so that the Dedekind and Cauchy reals in \(\mathcal N\) coincide; and that the ring of real numbers in \(\mathcal N\) enjoys certain algebraic and order-theoretic properties (specifically, those of being an integral domain and of being totally ordered) which it does not possess in a general topos.