Formally real field Created 2026-10-06 Updated 2026-10-07
A field is formally real when is not a finite sum of squares. The Artin-Schreier ordering criterion says this is equivalent to the existence of an ordering compatible with the field operations. Such a field has characteristic zero and embeds into a real closed field.
A ring homomorphism is understood to preserve . Start with . Its map on spectra of rings is
Contraction gives a prime ideal, and . Thus is continuous for the Zariski topology. On each principal open subscheme, the structure sheaf map is the ring homomorphism
These maps commute with restrictions, so they define a sheaf morphism . At , with , its stalk map is . The inverse image of the maximal ideal is , so this is a local homomorphism. We have constructed a morphism of locally ringed spaces.
Conversely, let be a morphism of locally ringed spaces. Its map on global sections gives , using and . Fix and put . Compatibility with the stalk maps and the local homomorphism property give
Consequently , so the underlying map is forced. On , the sheaf morphism is forced as well: it extends and sends to a unit, hence agrees with the displayed map by the universal property of localization. The principal open subschemes form a basis, so the entire sheaf morphism is determined. Taking global sections of the construction recovers . The two constructions are inverse, proving the affine-target adjunction for schemes in the affine-source case:
To describe the real affine plane scheme points, write . It is a unique factorization domain of Krull dimension two. Its points are exactly the following prime ideals:
For completeness, any height-one prime ideal contains an irreducible polynomial ; since is already a height-one prime ideal, it must equal . Every remaining nonzero prime ideal has height two and is maximal, by Krull dimension. For a nonreal pair, evaluation generates all of over , so its kernel is maximal. Conversely, each residue field isomorphic to has exactly the two conjugate real-algebra embeddings into , proving the assertion about repetitions.
This describes the topology too: consists of the prime ideals containing , and the closure of a point is . In particular, the closure of is the whole affine plane, while the closure of contains precisely the closed points on , together with itself. The spectrum is much larger than the set . For example, is a height-one point although its curve has no real points. Its structure sheaf has and stalk at .
The induced morphism of schemes
is contraction of prime ideals, with the structure sheaf maps given above. On closed points, it sends to the kernel of real-polynomial evaluation at . A real closed point has one complex point above it; a nonreal closed point has two, interchanged by complex conjugation. The source generic point maps to the target generic point. The source height-one points are generated by irreducible complex polynomials . Their contractions are height-one prime ideals , and is a factor of over . An irreducible real either stays irreducible over or splits into two distinct conjugate irreducible factors. Indeed, complex conjugation acts transitively on its distinct factors, or a proper orbit product would give a real factor of ; every orbit has size at most two. Repeated factors are excluded by separability in characteristic zero. Thus one or two height-one points lie above .
The complexification fibres of a real scheme give a uniform description of all scheme-theoretic fibres, including the nonclosed points, is especially useful. The extension of coordinate rings is
a free -module with basis . At , with residue field , the scheme-theoretic fibre is
If is a square in , the Chinese remainder theorem gives , hence two points. Otherwise it is a quadratic field extension, hence one point. The polynomial has no repeated root in characteristic zero, so all these scheme-theoretic fibres are reduced schemes. This also proves surjectivity. Conjugation acts on each two-point fibre by exchanging its points and fixes each one-point fibre. As a finite morphism, is closed, so its underlying topological space is the quotient by complex conjugation. The fibre formula explains why a real closed point gives one complex point, whereas the generic point gives a single point with residue field .
A formally real field is a field in which is not a finite sum of squares. The theory of formally real fields consists of the field axioms and, for each , the sentence
A real closed field is a formally real field with no proper formally real algebraic extension. An equivalent first-order axiomatization of the Theory of real closed fields adds: every or its negative is a square, and every odd-degree polynomial has a root. Explicitly the square axiom is
and the polynomial axioms say that every monic polynomial of degree has a root, for each .
The Artin-Schreier ordering criterion says that every formally real field can be ordered, and the real closure theorem embeds each ordered field into an algebraic real closed field extension. Consequently every FRF model embeds into an RCF model. Conversely every RCF model is itself an FRF model, so the reverse embedding requirement is automatic.
It remains to establish model completeness. A real closed field has a unique order, definable in the field language by
Any field embedding between real closed fields preserves this order: positive elements are nonzero squares, and negative elements have positive negatives. The quantifier elimination for ordered real closed fields theorem makes every such ordered embedding elementary, by the preceding part. Restricting to formulas of the field language makes the original embedding elementary as well. Thus RCF is model-complete in the field language.
The embedding conditions and model completeness prove
The quantifier elimination invoked here is in the ordered language. In the unordered field language, model completeness still holds, but full quantifier elimination does not follow from forgetting the order.
The points of the real affine plane as a scheme are its prime ideals: the zero ideal, the principal ideals of irreducible real polynomials, and its maximal ideals. The latter have residue field or , by the Zariski lemma and the real closed field property. They correspond respectively to real coordinate pairs and conjugate pairs of nonreal complex coordinate pairs. Thus the scheme contains both nonclosed generic points and closed points absent from the real locus. Its topology is the Zariski topology, and its structure sheaf has sections on each principal open subscheme .
Real closure theorem 2026-10-06
Every ordered field has an ordered algebraic real closure. Combined with the Artin-Schreier ordering criterion, every formally real field embeds into a real closed field. This is one embedding direction in the model companion relation between their theories.
Theory of real closed fields Created 2026-09-28 Updated 2026-10-14
This is the complete first-order theory of real closed fields.
The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.