Construction du hensélisé d’un corps valué

F.-V. Kuhlmann (^{1}), Henri Lombardi (^{2})

Mars 2000

Abstract

Nous donnons une construction explicite, et constructivement prouvée, du hensélisé d’un corps valué. Cette construction peut être considérée comme l’analogue, dans le cas valué, de la construction de la cloture réelle d’un corps ordonné.

Classification AMS : 12J10, 12F05, 13J15, 12Y05, 03F65

Mots clés : Corps valué, Hensélisation, Mathématiques constructives.

Introduction

Il est connu que le hensélisé d’un corps valué est unique à isomorphisme unique près. Cette situation est analogue à celle de la cloture réelle d’un corps ordonné. Dans ce dernier cas, non seulement on sait calculer dans la cloture réelle en utilisant des algorithmes dérivés de l’algorithme de Sturm, mais en plus on peut prouver constructivement que ces calculs forment un tout cohérent, ce qui donne en fin de compte une construction entièrement satisfaisante de la cloture réelle (cf. [5, 9, 7, 4, 10]).

Il est naturel que le hensélisé d’un corps valué puisse lui aussi être construit de manière explicite. Du point de vue technique, les algorithmes du type Sturm basés sur des divisions successives sont remplacés, en théorie des corps valués, par l’usage systématique des polygones de Newton.

Dans cette note, nous utilisons des résultats de l’article [1] pour certifier constructivement la construction que nous donnons du hensélisé d’un corps valué.

Signalons également un article en préparation [6] concernant les calculs dans les extensions algébriques arbitraires d’un corps valué.

1 Department of Mathematics and Statistics University of Saskatchewan 106 Wiggins Road, Saskatoon, SK, S7N 5E6, Canada. E-mail: fvk@math.usask.ca. Home Page: http://math.usask.ca/ fvk/index.html

2 Laboratoire de Mathématiques, (UMR CNRS 6623), UFR des Sciences et Techniques, Université de Franche-Comté, 25 030 BESANÇON cedex, FRANCE. E-mail:lombardi@math.univ-fcomte.fr

1 Extensions algébriques d’un corps valué

Nous précisons tout d’abord quelques notations. Un corps valué est donné par un couple (K, V) où K est un corps et V un anneau de valuation de ce corps, c.-à-d. un anneau qui vérifie l’axiome de Krull

∀x ∈ K^{×} ( x ∈ V ou 1/x ∈ V )

On notera v_{K} : K^{×} → K^{×}/V^{×} la valuation correspondante. On étend v_{K} à K tout entier en posant v_{K}(0) = ∞. Les non unités de V, qui sont aussi les x ∈ K tels que v_{K}(x) > v_{K}(1), forment son idéal maximal que nous noterons M_{V}. Le groupe ordonné Γ_{K} := K^{×}/V^{×} est appelé le groupe de valuation, et le corps \overline{K} := V/M_{V} le corps résiduel du corps valué (K, V). Nous notons Γ̃_{K} := Γ_{K} ∪{∞}. Lorsque (L, W) est une extension valuée de (K, V) (i.e., K ∩W = V), Γ_{K} s’identifie à un sous-goupe de Γ_{L} et \overline{K} à un sous corps de \overline{L}. Si en outre L est une cloture algébrique de K alors Γ_{L} s’identifie à la cloture divisible de Γ_{K}.

D’un point de vue calculatoire, pour traiter un corps valué (K, V), on peut partir d’un anneau intègre A, dont le corps des fractions est K, dans lequel les opérations de base de l’anneau sont explicites, et à l’intérieur duquel on dispose des prédicats v_{K}(x) ≥ v_{K}(y) et x = 0 .

Les algorithmes utilisés dans nos constructions prennent en entrée une liste a = (a_{1}, …, a_{n}) d’éléments de A, utilisent des polynomes P_{1}, …, P_{r} de ZZ[x_{1}, …, x_{n}] et selon la réponse à certains tests

P_{i}(a) = 0 ? ou v_{K}(P_{h}(a)) ≥ v_{K}(P_{k}(a)) ?

produisent une sortie convenable. Nous appellerons de tels algorithmes des algorithmes uniformes dans (K, V) et les calculs correspondants des calculs uniformes dans (K, V).

Un théorème classique affirme que tout corps valué (K, V) peut être étendu en un corps valué algébriquement clos (K^{ac}, V^{ac}) (V^{ac} ∩ K = V). Ce théorème ne peut pas être prouvé constructivement (en particulier il n’existe pas de méthode constructive générale pour obtenir une cloture algébrique d’un corps.)

Il existe néanmoins des versions constructives de ce théorème classique. En voici une.

Notons T_{cvac} la théorie formelle des corps valués algébriquement clos basée sur le langage des anneaux, avec en outre un prédicat Av(x) pour l’appartenance à l’anneau de valuation. Si (K, V) est un corps valué, on considère la théorie formelle T_{cvac}(K, V) qui est la théorie formelle construite à partir de T_{cvac} dans laquelle on a introduit comme constantes et relations le diagramme de (K, V).

Le théorème classique que nous venons d’évoquer est équivalent, modulo le théorème de complétude de Gödel (qui est une variante faible de l’axiome du choix^{1}), au théorème concret suivant :

Théorème 1 Avec les notations ci-dessus, la théorie formelle T_{cvac}(K, V) est cohérente.

1 Il est surprenant que dans presque tous les livres de logique mathématique, le théorème de complétude de Gödel soit affirmé comme une vérité de caratère absolu, avec le même degré de certitude par exemple que le théorème d’incomplétude, ou que le théorème sur la transcendance de π. Alors que le théorème de complétude n’est, du point de vue classique lui-même, qu’une variante faible de l’axiome du choix. Ce contre-sens manifeste commis dans les livres de logique (par les professionnels de la chose, donc) est sans doute dû au grand réconfort moral que le théorème de complétude apporte aux adeptes de la théorie des ensembles classique : notre logique est la bonne puisque le théorème de complétude dit qu’elle est adéquate à la théorie naïve des ensembles. Eh non, c’est d’une théorie (pas si naïve que cela) des ensembles avec axiome du choix et principe du tiers exclu qu’il s’agit.

Une preuve constructive de ce théorème concret peut être trouvée par exemple dans [1] (en mettant bout à bout les théorèmes 1.1 et 4.3).

Rappelons maintenant quelques résultats de la théorie classique (a priori non constructive) du hensélisé d’un corps valué. À l’intérieur d’une cloture algébrique valuée (K^{ac}, V^{ac}) de (K, V) se trouve le hensélisé (K^{H}, V^{H}) de (K, V) (avec V^{H} = V^{ac} ∩ K^{H}). Ce corps est défini comme le corps fixe du groupe des K–automorphismes de K^{sep} (la cloture séparable de K) qui fixent V^{sep} = V^{ac} ∩ K^{sep}. Le corps K^{H} peut être caractérisé de manière plus terre à terre comme la plus petite sous extension de (K^{ac}, V^{ac}) qui soit stable par le processus de rajout d’un zéro à la Hensel. Un zéro à la Hensel codé par un couple (P, a) ∈ V [X] × V, sous la condition que P (a) ∈ M_{V} et P′(a) ∈ V^{×}, est l’unique élément α ∈ K^{ac} qui vérifie

P (α) = 0 et α − a ∈ M_{V}

L’extension (K^{H}, V^{H}) est immédiate en ce sens que ni le groupe de valuation, ni le corps résiduel ne changent. Tout élément de K^{H} possède alors une description immédiate dans K au sens suivant :

Définition 1.1 Soit ξ un élément de K^{ac}. Soit (L, W) := (K[ξ], V^{ac} ∩ L). Alors ξ est dit immédiat au dessus de (K, V) s’il existe un x ∈ K et μ ∈ M_{W} avec ξ = x(1 + μ). Nous disons que x est une description immédiate de ξ dans (K, V).

2 Calculs dans le hensélisé

Dans cette section, nous faisons comme si la théorie classique du hensélisé d’un corps valué assurait l’existence de (K^{ac}, V^{ac}) et de (K^{H}, V^{H}) et nous montrons comment il est alors possible de calculer au sein du hensélisé.

Puisque Γ_{K^{ac}} s’identifie à la cloture divisible de Γ_{K}, on peut considérer la valuation v_{K^{ac}} comme un prolongement de v_{K}, et nous les noterons toutes deux, pour simplifier, tout simplement v.

Un élément du hensélisé est obtenu par extensions successives de (K, V), en rajoutant des zéros à la Hensel l’un après l’autre. Lors de la première étape, ξ_{1} est un zéro à la Hensel codé par (P_{1}, a_{1}) ∈ V [X] × V. Ceci fournit le corps valué (K_{1}, V_{1}) avec K_{1} = K[ξ_{1}] et V_{1} = K_{1} ∩ V^{ac}. Un élément arbitraire de K_{1} est donné sous la forme R(ξ_{1}) avec R ∈ K[X]. On poursuit ensuite de manière récursive. Pour le zéro ξ_{2}, (K_{1}, V_{1}) remplace (K, V) et ainsi de suite.

Si nous savons dans chacune de ces extensions successives, calculer pour n’importe quel élément ξ une description immédiate x(ξ) dans K, alors nous savons donner une réponse aux tests ξ = 0 ? et v(ξ) ≥ v(ξ′) ? (il suffit de faire le test sur des descriptions immédiates de ξ et ξ′). D’autre part, si ξ est obtenu comme élément d’une extension K[ξ_{1}, …, ξ_{n}] et ζ est obtenu comme élément d’une extension K[ζ_{1}, …, ζ_{m}], alors on peut les considérer tous deux comme éléments de K[ξ_{1}, …, ξ_{n}, ζ_{1}, …, ζ_{m}], de sorte que l’on a bien la possibilité de faire tous les calculs et tous les tests correspondants à la structure de corps valué (K^{H}, V^{H}).

Rappelons que le polygone de Newton d’une polynome P (X) = ∑_{i=0,...,d} p_{i}X^{i} ∈ K[X] (avec p_{d} ≠ 0) est formé à partir de la liste de couples dans IN × Γ̃_{K}

[(0, v(p_{0})), (1, v(p_{1})), …, (d, v(p_{d}))]

Le polygone de Newton est “l’enveloppe convexe inférieure” de cette liste. Formellement on peut le définir comme la liste extraite qui vérifie la condition suivante : les couples (i, v(p_{i})) et (j, v(p_{j})) sont consécutifs dans la liste extraite si et seulement si on a :

si 0 ≤ k < i (v(p_{i}) − v(p_{k}))/(i − k) < (v(p_{i}) − v(p_{j}))/(i − j)
si i < k < j (v(p_{i}) − v(p_{k}))/(i − k) ≥ (v(p_{i}) − v(p_{j}))/(i − j)
si j < k ≤ d (v(p_{i}) − v(p_{j}))/(i − j) < (v(p_{j}) − v(p_{k}))/(j − k)

On montre facilement que si (i, v(p_{i})) et (j, v(p_{j})) sont deux sommets consécutifs du polygone de Newton du polynome P, celui-ci admet exactement j − i zéros dans K^{ac} dont la valuation soit égale à (v(p_{i}) − v(p_{j}))/(j − i) . En particulier, si j = i + 1, le zéro correspondant est nécessairement dans le hensélisé K^{H}. La proposition suivante, dont la preuve ressort d’un calcul immédiat, donne quelques précisions sur ce cas. Remarquons aussi que, vues nos hypothèses sur (K, V), nous pouvons déduire du polygone de Newton de P la liste ordonnée des valuations des zéros de P dans Γ̃_{K^{ac}} = Γ_{K^{ac}} ∪ {∞}. Notons aussi que si 0 est un zéro de P de multiplicité h, cela correspond à une pente infinie du segment initial de largeur h dans le polygone de Newton.

Introduisons une terminologie :

Définition 2.1 Un polynome T ∈ V [X] est dit spécial s’il est de la forme X^{d} − X^{d−1} + t_{d−2}X^{d−2} + ⋯ + t_{1}X + t_{0} avec les t_{i} ∈ M_{V}. Le zéro de T codé à la Hensel par (T, 1) est appelé le zéro spécial de T.

Notez que les autres zéros de T dans K^{ac} sont dans M_{V^{ac}}.

Proposition 2.2 (Lemme de Hensel, version polygone de Newton) Soit (K, V) un corps valué et P ∈ V [X] un polynome : P (X) = ∑_{i=0,...,d} p_{i}X^{i}. Supposons que le polygone de Newton de P admette une pente “isolée” de (k, v(p_{k})) à (k + 1, v(p_{k+1})).

1) Alors l’unique zéro α de P tel que v(α) = v(p_{k})−v(p_{k+1}) admet −p_{k}/p_{k+1} pour description immédiate :

α = −\frac{p_{k}}{p_{k+1}} (1 + μ) avec μ ∈ M_{V^{ac}}

2) En outre ν = 1 + μ est un zéro à la Hensel codé par (Q, 1) où Q ∈ V [Y] est donné par

Q(Y) = \frac{p_{k+1}^{k}}{p_{k}^{k+1}} P (−\frac{p_{k}}{p_{k+1}} Y)

(ν est l’unique zéro de Q dans V^{ac}^{×}).

3) Si on pose ∑_{i=0,...,d} r_{i}X^{i} := R(X) := Q(1 + X) , on a v(r_{0}) > 0 et v(r_{1}) = 0 . Si r_{0} = 0 alors μ = 0. Si r_{0} ≠ 0 on pose S(X) := (1/r_{0})R(−r_{0}X/r_{1}) et T (X) = X^{d}S(1/X) et on obtient que T ∈ V [X] est un polynome spécial, de sorte que tous les zéros de T, sauf celui correspondant au zéro α de P sont dans M_{V^{ac}}. En résumé, un zéro α correspondant à une pente isolée d’un polygone de Newton peut toujours être explicité soit comme un élément de K, soit sous une forme (aβ + b)/(cβ + d) où β est le zéro spécial d’un polynome spécial T, a, b, c, d ∈ V, (cβ + d) ≠ 0 et (ad − bc) ≠ 0.

Notons qu’un zéro à la Hensel α codé par (R, f) correspond à une pente isolée, de (0, v(p_{0})) à (1, v(p_{1})), du polygone de Newton de P (X) = R(X + f). On a donc, de manière explicite, pour tout zéro à la Hensel α, K[α] = K[β] où β est le zéro spécial d’un polynome spécial.

Vu ce dernier résultat, et vus les commentaires précédents, la possibilité de calculer explicitement dans (K^{H}, V^{H}) est ramenée à la proposition suivante.

Proposition 2.3 Soit T un polynome spécial, β son zéro spécial dans K^{H} et Q ∈ K[X], alors une description immédiate de Q(β) peut être obtenue par des calculs uniformes dans (K, V).

Preuve Si β = 1 il n’y a rien à faire. On supposera donc β ≠ 1 (remarquons qu’on n’a pas en général de test permettant de savoir si β ∈ K ou β ∉ K). Appelons β_{1} = β, β_{2}, …, β_{d} les zéros de T dans K^{ac} (on peut les supposer tous non nuls). Tout d’abord, nous donnons un algorithme qui permet de calculer v(Q(β)) ∈ Γ̃_{K^{ac}}, sans pour autant arriver nécessairement à l’expliciter comme élément de Γ̃_{K} (ceci sera fait, à coup sûr, dans un deuxième temps). Nous remarquons que v((1−β)Q(β)) > v(Q(β)) , sauf si Q(β) = 0, tandis que v((1 − β_{i})Q(β_{i})) = v(Q(β_{i})) pour i > 1. Soit Q_{1} et Q_{2} les deux polynomes dans K[X] définis par

Q_{1} = ∏_{i=0,...,d}(X − Q(β_{i})) et Q_{2} = ∏_{i=0,...,d}(X − (1 − β_{i})Q(β_{i}))

(ces deux polynomes sont faciles à calculer^{2}). Il suffit d’établir la liste ordonnée des valuations des zéros de Q_{1} dans Γ̃_{K^{ac}} et de la comparer à la liste ordonnée des valuations des zéros de Q_{2} dans Γ̃_{K^{ac}} pour tester si Q(β) = 0, et dans le cas où Q(β) ≠ 0, pour donner v(Q(β)) dans la cloture divisible de Γ_{K} comme égal à la pente finie d’un segment bien déterminé du polygone de Newton de Q_{1}. Si nous sommes dans le cas où Q(β) ≠ 0, nous allons maintenant utiliser notre connaissance de v(Q(β)) en tant qu’élément de la cloture divisible de Γ_{K} pour calculer une description immédiate de Q(β). Pour cela on remarque que v(β^{m}Q(β)) = v(Q(β)) tandis que v(β_{i}^{m}Q(β_{i})) = v(Q(β_{i})) + mv(β_{i}) > v(Q(β_{i})) pour i > 1 (sauf si Q(β_{i})) = 0). Il existe un entier m tel que mv(β_{i}) ≠ v(Q(β)) − v(Q(β_{i})) pour tous les entiers i = 2, …, d. Un tel entier peut être calculé de la manière suivante : il suffit que mv(β_{i}) ≠ v(Q(β_{j})) − v(Q(β_{k})) pour tous j, k et tout i > 1 (en se restreignant aux valuations finies). Comme le second membre ne prend qu’un nombre fini de valeurs et comme les v(β_{i}) (i > 1) sont > 0, on trouve m après un nombre fini de tests concernant la liste des v(β_{i}) (i > 1) et celle des v(Q(β_{j})). Pour un tel m on calcule le polynome Q_{3} = ∏_{i=0,...,d}(X − β_{i}^{m}Q(β_{i})). On sait que le zéro β^{m}Q(β)) de Q_{3} correspond à une pente isolée de son polygone de Newton et comme on connait la valeur de v(β^{m}Q(β)) = v(Q(β)) dans Γ_{K^{ac}} on sait de quelle pente isolée il s’agit. On utilise enfin la proposition 2.2 pour obtenir une description immédiate de β^{m}Q(β) dans K, qui est aussi une description immédiate de Q(β). □

3 La construction du hensélisé

Du point de vue des mathématiques classiques, pour lesquelles l’existence de (K^{ac}, V^{ac}) est assurée, la section 2 donne une construction du hensélisé (K^{H}, V^{H}) au sens suivant : (K^{H}, V^{H}) est la limite inductive filtrante des extensions finies (K[α_{1}, α_{2}, …, α_{n}], V_{n}) (V_{n} est l’unique anneau de valuation de K[α_{1}, α_{2}, …, α_{n}] qui étend V) où chaque α_{i} est un zéro à la Hensel (ou à la Newton-Hensel comme dans la proposition 2.2) sur le corps valué (K[(α_{j})_{j<i}], V_{i−1}). Cette limite inductive est bien filtrante, car si on a deux extensions K[α_{1}, α_{2}, …, α_{n}] et K[β_{1}, β_{2}, …, β_{m}], on a aussi l’extension

K[α_{1}, α_{2}, …, α_{n}][β_{1}, β_{2}, …, β_{m}] = K[β_{1}, β_{2}, …, β_{m}][α_{1}, α_{2}, …, α_{n}].

Enfin, il s’agit bien d’une construction car nous savons expliciter la structure de chacune de ces extensions finies par des calculs uniformes qui n’utilisent que la structure de (K, V) et la description de chaque générateur successif α_{i} par un code à la Hensel (ou à la Newton-Hensel).

2 Par exemple si M est la matrice compagnon du poynome T ayant pour racines des β_{i}, le polynome caracteristique de M est egal au produit des (X − β_{i}), et le polynome caracteristique de Q(M) est egal au produit des (X − Q(β_{i})).

Pour que cette construction soit certifiée en mathématiques constructives, il faut démontrer constructivement que les calculs de la section 2 ne conduisent à aucune contradiction. Si cette preuve est faite, alors on peut voir (K^{H}, V^{H}) comme l’objet construit par ces calculs, et non plus, comme c’était le cas (intuitivement) dans la section 2, comme un objet déjà construit a priori par une méthode abstraite. Le théorème 1 (tel qu’il est prouvé dans [1]) nous donne la preuve constructive de la cohérence des calculs dans la section 2 : il suffit de vérifier que tous les raisonnements qui certifient ces calculs du point de vue des mathématiques classiques sont en fait des raisonnements qui peuvent être développés au sein de la théorie formelle T_{cvac}(K, V). Ainsi nous avons obtenu la preuve constructive du théorème suivant.

Théorème 2 Étant donné un corps valué (K, V) dans lequel l’égalité et la divisibilité sont testables, il existe une extension valuée (K^{H}, V^{H}) qui contient un zéro à la Hensel pour tout code à la Hensel (P, a) dans V^{H}[X] × V^{H}. Cette extension est unique à (K,V)–isomorphisme unique près si on réclame qu’elle soit engendrée par le processus de rajout de zéros à la Hensel. C’est une extension immédiate explicite de (K, V) : tout élément de K^{H} possède une description immédiate dans K. Enfin l’égalité et la divisibilité sont testables dans (K^{H}, V^{H}).

Signalons que la preuve que nous venons de donner (pour l’existence du hensélisé d’un corps valué) est l’analogue de celles développées pour la cloture réelle d’un corps ordonné dans [4] et [7] plutôt que de celles données dans [5], [10] ou [9].

Le raisonnement précédent peut être rendu plus agréable et plus intuitif si on adopte le point de vue de l’évaluation dynamique, tel qu’il est développé dans [1] ou [8] à partir de l’intuition donnée par le système de calcul formel D5 (cf. [2] et [3]). On constate que les axiomes des corps valués (et ceux des corps valués algébriquement clos) peuvent être mis sous une forme structurellement simple, ce que nous appelons des règles dynamiques. Une évaluation dynamique d’une structure algébrique incomplétement spécifiée revient alors à appliquer ces règles dynamiques à la structure incomplètement spécifiée. Par exemple un corps valué peut être compris comme un corps valué algébriquement clos incomplètement spécifié. Les calculs uniformes de la section 2 se situent naturellement dans ce cadre : ils fournissent une évaluation dynamique du corps valué (K, V) lorsqu’on le considère comme un corps valué algébriquement clos incomplètement spécifié. Une évaluation dynamique est un calcul arborescent recelant parfois des ambiguités incontournables (dans la cloture algébrique d’un corps “général” par exemple, les zéros d’un polynome sont jusqu’à un certain point indiscernables et cela crée une telle ambiguité, qui est la source de l’impossibilité d’exhiber constructivement la cloture algébrique comme un objet global parfaitement controlé). L’important est cependant, pour une structure dynamique, qu’elle ne s’effondre pas sous le coup d’une preuve de 1 = 0 par exemple. Le théorème 4.3 dans [1] certifie que l’évaluation dynamique d’un corps valué comme corps valué algébriquement clos ne produit pas de contradiction. Au sein des évaluations dynamiques du corps valué (K, V), la partie “hensélisé” ne recèle pas d’ambiguité, et c’est ce qui fait que le hensélisé peut être en toute généralité construit comme un objet global parfaitement controlé, contrairement à la cloture algébrique valuée.

Nous terminons en remarquant que la définition abstraite du hensélisé K^{H} comme corps fixe d’un certain groupe d’automorphismes de K^{ac} possède une version “dynamique” qui lui est classiquement équivalente via le théorème de complétude de Gödel, et qui constitue donc une version constructivement satisfaisante du théorème classique correspondant. Le théorème classique dit que la définition abstraite “par le haut” de K^{H} comme corps fixe d’un certain groupe coïncide avec une définition terre à terre “par le bas” (le plus petit corps stable par rajout de racines à la Hensel). Le théorème dynamique correspondant en caractéristique nulle est le suivant (nous ne savons pas pour le moment en donner une preuve constructive) :

Théorème 3 Considérons une présentation (K, V) de corps valué de caractéristique nulle et évaluons là dynamiquement en tant que corps algébriquement clos valué. Soit t un terme apparaissant dans un tel arbre. Alors les deux propriétés suivantes sont équivalentes :

— t est égal (au sens de l’évaluation dynamique) à un élément de K[ξ_{1}, …, ξ_{n}] où les ξ_{j} sont des zéros à la Hensel rajoutés en cascade les uns après les autres.

— si on introduit un symbole de fonction φ soumis aux règles dynamiques spécifiant que φ est un automorphisme de K^{ac} qui fixe K point par point et V^{ac} globalement, alors t est égal à φ(t) (au sens de l’évaluation dynamique).

References

[1] Coste M., Lombardi H., Roy M.-F.: Dynamical method in algebra : Effective Nullstellensätze preprint 1996.

[2] Della Dora J., Dicrescenzo C., Duval D.: About a new method for computing in algebraic number fields. Proceedings Eurocal’85. Lecture Notes in Computer Science n^{o}204, p 289– 290 (1985). (Springer)

[3] Dicrescenzo C., Duval D.: Algebraic extensions and algebraic closure in Scratchpad. Symbolic and algebraic computation (ISSAC 88). Lecture Notes in Computer Science n^{o}358, p 440–446 (1989). (Springer)

[4] Delzell, C.: Kreisel’s Unwinding of Artin’s Proof. p. 113–246 dans Kreiseliana (ed. P. Odifreddi). A. K. Peters, Wellesley, Massachussets, USA, 1996.

[5] Holkott, A.: Finite Konstruktion geordneter algebraischer Erweiterungen von geordneten Grundkörpen. Dissertation. Hamburg, 1941, 65 pages.

[6] Kuhlmann, F.-V., Lombardi H., Perdry H.: Computations in algebraic extensions of a valued field. En préparation.

[7] Lombardi H.: Théorème effectif des zéros réel et variantes Publications Mathématiques de Besançon, Théorie des Nombres, 1988–89. Fascicule 1.

[8] Lombardi H.: Relecture constructive de la théorie d’Artin-Schreier Annals of Pure and Applied Logic 91, (1998), 59–92.

[9] Lombardi H., Roy M.-F.: Constructive elementary theory of ordered fields. p. 249–262, in Effective Methods in Algebraic Geometry. Ed. Mora T., Traverso C. Birkhäuser 1991. Progress in Math. n^{o}94.

[10] Sander T.: Existence and uniqueness of the real closure of an ordered field without Zorn’s lemma. J. Pure Appl. Algebra 73, 2, (1991), 165–180