Separably real closed local rings (Q1083520)

In topos theory several different constructions of ''variable reals'' (Dedekind reals using cuts, Cauchy reals using sequences) can be performed, giving in some well chosen toposes various sheaves of real functions (continuous, \(C^{\infty}\) analytic, etc...). These sheaves of functions are not real closed fields (in fact they are not fields). This fact is discussed in the introduction of the paper. A. Kock introduced the definition of separably real closed local ring (i.e. local Henselian with real closed residue field) and conjectured that the Dedekind reals in any elementary topos is always a separably real local ring. The paper is devoted to the proof of that conjecture, which was known in particular cases, and of other related results. The proof relies on a coherent axiomatization of separably real closed local rings, which uses the finiteness theorem of semi-algebraic geometry (a topological refinement of Tarski-Seidenberg elimination of quantifiers for real closed fields). The paper is clearly written; I regret that it does not include any precise references to the construction of ''variable reals'' in elementary toposes.