Henri Lombardi
email: henri.lombardi@univ-fcomte.fr

Stefan Neuwirth
email: stefan.neuwirth@univ-fcomte.fr

Ihsen Yengui
email: ihsen.yengui@fss.rnu.tn

Valuative dimension, constructive points of view

Keywords: Constructive mathematics, valuative dimension of a commutative ring, algorithms, Hilbert programme for abstract algebra. MSC: 13B40, 13J15, 03F65

There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics.

Introduction

This article is written in Bishop's style of constructive mathematics [START_REF] Bishop | Foundations of constructive analysis[END_REF][START_REF] Bishop | Constructive analysis[END_REF], Bridges and Richman 1987, Lombardi and Quitté 2021, Mines, Richman, and Ruitenburg 1988, Yengui 2015).

The vocabulary and notation of dynamical algebraic structures will be used when necessary: see Coste, Lombardi, and Roy 2001, Coquand and Lombardi 2006, Lombardi 2006, 2020. In this paper we compare the different constructive versions of the valuative dimension found in Coquand 2009, Kemper and Yengui 2020, Lombardi and Quitté 2015, 2021, as well as a constructive version which extends that of Coquand 2009 to the case of a not necessarily integral ring.

The reader who does not know about constructive mathematics in Bishop's style may look up Chapters 1 and 2 of [START_REF] Bishop | Foundations of constructive analysis[END_REF], its reviews Stolzenberg 1970, Myhill 1972, and the paper Coquand and Lombardi 2006. When a classical definition or a classical theorem uses abstract notions without computational content, constructive mathematicians try to find what they call a constructive version of this definition or theorem. This version has to be equivalent within classical mathematics to the classical one. Moreover, it is necessary that basic classical examples can be dealt with for the constructive version. E.g., the constructive version of a local ring is simply a ring in which, each time the sum of finitely many elements is invertible, one of these elements is invertible.

Definition and characterisations of the valuative dimension in classical mathematics

In classical mathematics, the valuative dimension of an integral ring R is the maximal length n of a chain of valuation rings V 0

• • • V n = K in the field of fractions K = Frac R which contain R.

The valuative dimension of an arbitrary ring is defined as the upper bound of the valuative dimension of its integral quotients (Cahen 1990).

In classical mathematics, the following equivalences are well known (Kdim(R) denotes the Krull dimension of the ring R).

Note that these definitions use the law of excluded middle (LEM) and Zorn's lemma (a weak form of choice).

Let us recall that a discrete field is of Krull dimension 0; the dimension of the trivial ring, which has no integral quotient, is by convention equal to -1.

Theorem 1.1. Let R be a nontrivial commutative integral ring with K = Frac(R). The following properties are equivalent.

1. R is of valuative dimension n.

2. For any integer k and all x 1 , . . . , x k ∈ K, Kdim(R[x 1 , . . . , x k ]) n.

3. For any integer k, Kdim(R[X 1 , . . . , X k ]) n + k.

4. Kdim(R[X 1 , . . . , X n ]) 2n.

Introduction

Moreover, without supposing R to be integral, but supposing it to be nontrivial, Items 1, 3, and 4 are still equivalent.

The paper Kemper and Yengui 2020, which follows Kemper and Viet Trung 2014, proposes a new further characterisation of the valuative dimension of a commutative ring, inspired by the constructive characterisation of Krull dimension given in Lombardi 2006. The characterisation in Kemper and Yengui 2020 is fully constructive.

We are thus in possession of at least three possible constructive approaches to the valuative dimension of a commutative ring defined within classical mathematics: the one corresponding to Item 1 above, the one corresponding to Items 3 and 4, and the one proposed by Kemper and Yengui. We propose in Section 2 to recall the precise constructive definitions concerning these three approaches.

We denote by Vdim(R) a constructive definition corresponding to the characterisation given in Item 1 of Theorem 1.1.

We denote by vdim(R) a constructive definition corresponding to the characterisation given in Item 3 of Theorem 1.1.

We denote by dimv(R) the constructive definition given by Kemper and Yengui. These constructive definitions have already been shown to be equivalent to the classical definition within classical mathematics, at least in the case of an integral domain.

In Section 3 we prove constructively the equivalence of these three definitions in all generality.

Basic constructive terminology

A subset P of a set E is said to be detachable when the property x ∈ P is decidable for x ∈ E. In other words, the following rule is satisfied:

• ⊢ x ∈ P or x / ∈ P

In order to describe this situation, it is therefore necessary to introduce both the membership predicate and the opposite predicate. We say that a ring is integral (or that it is an integral domain) when any element is zero or regular, and that a ring is a discrete field when any element is zero or invertible. This does not exclude the trivial ring.

A ring is said to be without zerodivisor when the rule

• xy = 0 ⊢ x = 0 or y = 0 is satisfied. An integral ring has no zerodivisor. The converse, valid within classical mathematics, is not guaranteed constructively. 1Some local versions of the notions of integral ring and ring without zerodivisor are discernible even within classical mathematics.

A ring R is said to be locally without zerodivisor (or a pf-ring: "principal ideals are flat") when the following rule is satisfied:

• ab = 0 ⊢ ∃s, t (sa = 0, tb = 0, s + t = 1)

Then in R[1/s] the element a is zero, and in R[1/t] the element b is zero. 2A ring R is said to be a pp-ring ("principal ideals are projective") if the annihilator Ann R (a) of any element a is generated by a (necessarily unique) idempotent, denoted by 1e a . We have R ≃ R[1/e a ] × R/ e a . In the ring R[1/e a ], the element a is regular; in R/ e a , a is zero.3 A pp-ring is locally without zerodivisor, but the converse does not hold. Note that we have e ab = e a e b , e a a = a, and e 0 = 0. Pp-rings have a purely equational definition. Suppose indeed that a commutative ring is endowed with a unary law a → a • which satisfies the following three axioms:

a • a = a, (ab) • = a • b • , 0 • = 0. (1)
Then, for all a ∈ R, Ann R (a) = 1a • and a • is idempotent, so that R is a pp-ring.

Lemma 1.2 (pp-ring splitting lemma). Consider n elements x 1 , . . . , x n in a pp-ring R.

There exists a fundamental system of orthogonal idempotents (e j ) of cardinal 2 n such that in each of the components R[1/e j ], each x i is zero or regular.

The fact that a pp-ring can be systematically split into two components leads to the following general method. The essential difference with the previous splitting lemma is that we do not know a priori the finite family of elements that will cause the splitting.

Elementary local-global machinery No. 1. Most algorithms that work with nontrivial integral rings can be modified to work with pp-rings by splitting the ring into two components whenever the algorithm written for integral rings uses the test "is this element zero or regular?". In the first component the element in question is zero, in the second one it is regular.

We say that an ideal is prime if it produces a quotient ring without zerodivisor. This does not exclude the ideal 1 . These conventions (adopted in Lombardi and Quitté 2015) do not use negation and avoid some constructively offensive case-by-case reasonings.

Valuation rings

A valuation ring V is a subring of a discrete field K satisfying the axiom

• xy = 1 ⊢ x ∈ V or y ∈ V (x, y ∈ K)
We then say that V is a valuation ring of the discrete field K and that (K, V) is a valued field.

A valuation ring is the same as a local Bézout domain, or as an integral ring whose divisibility group is totally ordered.

In a valued field (K, V), we say that x divides y and we write x | y if there exists a z ∈ V such that xz = y. We denote by Γ(V) (or by Γ if the context is clear) the group K × /V × (noted additively), with the order relation induced by the relation | on K × . We let Γ ∞ = Γ ∪ {∞} (where ∞ is introduced as a maximal element). Under these conditions, the natural application v : K → Γ ∞ is called the valuation of the valued field. We have

v(xy) = v(x) + v(y), and v(x + y) min(v(x), v(y)) with equality if v(x) = v(y).
We also have

V = { x ∈ K ; v(x) 0 } and V × = { x ∈ K ; v(x) = 0 }.

Dimension of a distributive lattice

In this paragraph, we explain the constructive definition for the dimension of a distributive lattice. A distributive lattice T can be seen as the set of compact open subsets of a spectral space, which is called the dual space of T. The definition of this dimension agrees within classical mathematics with the dimension of the dual spectral space, which is also the maximal length of chains of prime ideals in T: see Theorem 1.5.

An ideal b of a distributive lattice (T, ∧, ∨, 0, 1) is a subset that satisfies the conditions

0 ∈ b x, y ∈ b =⇒ x ∨ y ∈ b x ∈ b, z ∈ T =⇒ x ∧ z ∈ b.    (2)
Let us denote by T/(b = 0) the quotient lattice obtained by forcing the elements of b to be zero. We can also define the ideals as the kernels of morphisms.

A principal ideal is an ideal generated by a single element a: it is denoted by ↓a and we have ↓a = { x ∈ T ; x a }. This ideal, endowed with the laws ∧ and ∨ from T, is a distributive lattice in which the maximal element is a. The canonical injection ↓a → T is not a morphism of distributive lattices because the image of a is not equal to 1. On the other hand, the application T → ↓a, x → x ∧ a is a surjective morphism which endows ↓a with the quotient structure of T/(a = 1).

The notion of filter is the opposite notion (i.e. obtained by reversing the order relation) to that of ideal.

The following rule, called cut, is particularly important for distributive lattices:

(x ∧ a b) ∧ (a x ∨ b) =⇒ (a b). (3)
If A ∈ P fe (T) (the set of finitely enumerated subsets of T), we let

A := x∈A x and A := x∈A x.
We denote by A ⊢ T B the relation defined as follows on the set P fe (T):

A ⊢ T B def ⇐⇒ A B.
This relation satisfies the following axioms, in which we write x for {x} and A, B for A ∪ B:

x

⊢ x (R) if A ⊢ B then A, A ′ ⊢ B, B ′ (M) if (A, x ⊢ B) and (A ⊢ B, x) then A ⊢ B. (T )
The relation is said to be reflexive, monotone, and transitive. The third axiom (transitivity) can be seen as a generalisation of Rule (3) and is also called cut.

Definition 1.3. For an arbitrary set S, a relation on P fe (S) that is reflexive, monotone, and transitive is called an entailment relation.

The following theorem is fundamental. It states that the three axioms of entailment relations are exactly what is needed for the distributive-lattice interpretation to work. Theorem 1.4 (fundamental theorem of entailment relations, Lorenzen 1951, Cederquist and[START_REF] Cederquist | Entailment relations and distributive lattices[END_REF]. Let S be a set with an entailment relation ⊢ on P fe (S). Consider the distributive lattice T defined by generators and relations as follows: the generators are the elements of S and the relations are

A ⊢ T B each time A ⊢ B.
Then, for all A, B in P fe (S), we have

A ⊢ T B =⇒ A ⊢ B.
In classical mathematics, a prime ideal p of a distributive lattice T = 1 is an ideal whose complement v is a filter (which is then a prime filter). We then have T/(p = 0, v = 1) ≃ 2. It is the same to give a prime ideal of T or a morphism of distributive lattices T → 2. Theorem 1.5 (dimension of a distributive lattice, see Coquand and Lombardi 2003[START_REF] Lombardi | Dimension de Krull, Nullstellensätze et évaluation dynamique[END_REF], 2020, Lombardi and Quitté 2015, chapter XIII). In classical mathematics, the following properties are equivalent for a nontrivial distributive lattice and for n 0.

1. The lattice is of dimension n, i.e. by definition the length of any chain of prime ideals is n.

2. For any x ∈ T, the quotient lattice T/(x = 0,

I x = 0) is of dimension n -1, where I x = { y ; x ∧ y = 0 }. 4
3. For any sequence (x 0 , . . . , x n ) in T there exists a sequence (y 0 , . . . , y n ) that is complementary in the following sense

1 ⊢ y n , x n y n , x n ⊢ y n-1 , x n-1 . . . . . . . . . y 1 , x 1 ⊢ y 0 , x 0 y 0 , x 0 ⊢ 0.              (4)
For example, for n = 2, the inequalities in (4) correspond to the following diagram in T.

1

✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ x 2 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ y 2 q q q q q q q q • • x 1 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ q q q q q q q q y 1 q q q q q q q q ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ • • x 0 q q q q q q q q y 0 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ 0 ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐
Important definition and remark. Items 2 and 3 are equivalent in constructive mathematics and are used for defining the dimension of T, denoted by Kdim(T) and called Krull dimension of the distributive lattice. Note however that from a constructive point of view, only the assertion "Kdim(T) n" has been clearly defined. In order to settle "Kdim(T) = n" it would be necessary to prove furthermore ¬(Kdim(T) n + 1). Fortunately, most classical theorems have an assumption of the form Kdim(T)

n. We also have the following constructive result which simplifies the use of Item 3. Lemma 1.6. Let S be a subset of a distributive lattice T which generates T as a distributive lattice. In constructive mathematics, for n 0, the following properties are equivalent.

1. For any sequence (x 0 , . . . , x n ) in T there exists a complementary sequence (y 0 , . . . , y n ) in T.

2. For any sequence (x 0 , . . . , x n ) in S there exists a complementary sequence (y 0 , . . . , y n ) in T.

In the two final paragraphs of this section, we explain how spectra of distributive lattices give rise to spectral spaces in abstract algebra. The duality between distributive lattices and spectral spaces has been established by Stone (1937). Hochster (1969) introduces the terminology of spectral spaces and has popularised their use, but neither cites Stone 1937 nor indicates the link between spectral spaces and distributive lattices.

Krull dimension of a commutative ring

We now recall the main idea of the constructive approach of [START_REF] Joyal | Spectral spaces and distributive lattices[END_REF][START_REF] Joyal | Les théorèmes de Chevalley-Tarski et remarques sur l'algèbre constructive[END_REF] to the spectrum of a commutative ring.

If a is an ideal of R, we denote by D R (a) (or D(a) if the context is clear) the nilradical of the ideal A:

D R (a) = R √ a = { x ∈ R ; ∃m ∈ N x m ∈ a } . ( 5
)
When a = x 1 , . . . , x n , we denote D R (a) by D R (x 1 , . . . , x n ). If the context is clear, we also write x for D R (x). By definition, the Zariski lattice of R, denoted by Zar(R), is the set of D R (x 1 , . . . , x n )'s with the order relation of inclusion. The greatest lower bound and least upper bound are given by

D R (a 1 ) ∧ D R (a 2 ) = D R (a 1 a 2 ) and D R (a 1 ) ∨ D R (a 2 ) = D R (a 1 + a 2 ). The Zariski lattice of R is a distributive lattice and D R (x 1 , . . . , x n ) = x 1 ∨ • • • ∨ x n .
The elements x form a system of generators (stable under ∧) of Zar(R).

If M is the multiplicative monoid in R generated by U = {u 1 , . . . , u m } and a = a 1 , . . . , a n is a finitely generated ideal, we have the equivalences i∈{1,...,m}

u i Zar(R) j∈{1,...,n} a j ⇐⇒ u∈{1,...,m} u i ∈ R √ a ⇐⇒ M ∩ a = ∅. (6)
This describes completely the distributive lattice Zar(R). In fact, the first formula in (6) defines an entailment relation on R which gives another description of Zar(R).

We also get the following characterisation (see Cederquist and[START_REF] Cederquist | Entailment relations and distributive lattices[END_REF]Lombardi 2003).

Proposition 1.7 (Joyal's definition of the spectrum of a commutative ring). The lattice Zar(R) is (up to unique isomorphism) the lattice generated by the symbols D R (a) for a ∈ R subject to the following relations:

D R (0 R ) = 0, D R (1 R ) = 1, D R (x + y) D R (x) ∨ D R (y), D R (xy) = D R (x) ∧ D R (y).
The construction R → Zar(R) yields a functor from the category of commutative rings to the category of distributive lattices. Via this functor the projection R → R/D R (0 R ) gives an isomorphism Zar(R) → Zar(R/D R (0 R )). We have Zar(R) = 1 if and only if 1 R = 0 R .

In classical mathematics there is an easy proof that the dimension of the distributive lattice Zar(R) is the usual Krull dimension of the ring R.

The Zariski lattice of a ring is the paradigmatic example of a distributive lattice generated by a dynamical algebraic structure. We explain the general method in the following paragraph.

Dynamical algebraic structures

References: Coste, Lombardi, and Roy 2001, Lombardi 1998, 2006, 2020[START_REF] Bezem | Automating coherent logic[END_REF], Coquand 2005. The (finitary) dynamical algebraic structures are explicitly named in Lombardi 1998, 2006. In Coste, Lombardi, and Roy 2001 they are implicit, but described in the form of their presentations. They are also implicit in [START_REF] Lombardi | Dimension de Krull, Nullstellensätze et évaluation dynamique[END_REF], last but not least, in Della Dora, Dicrescenzo, andDuval 1985 (D5), which has been an essential inspiration: one can compute safely in the algebraic closure of a discrete field even when it is not possible to construct this algebraic closure. It is therefore appropriate to consider the algebraic closure as a dynamical algebraic structure à la D5 rather than as a usual algebraic structure: lazy evaluation à la D5 provides a constructive semantics for the algebraic closure of a discrete field.

A more detailed study can be found in Lombardi 2023 (in progress); see also Lombardi and Mahboubi 2023.

A (finitary) dynamical theory T = (L, A) is a purely computational version, without logic, of a coherent theory. The language L is given by a signature; the axioms (elements of A) are dynamical rules.

A dynamical algebraic structure D for a dynamical theory T is given by generators and relations: D = (G, R), T . If (G, R) is the positive diagram of a usual algebraic structure R, we denote this by D = T (R).

Let us consider a dynamical algebraic structure D = (G, R), T for a dynamical theory T = (L, A). Let S be a set of closed atomic formulas of D. We define the entailment relation ⊢ on S associated with D as follows for A i and B j ∈ S:

A 1 , . . . , A n ⊢ B 1 , . . . , B m def ⇐⇒ A 1 , . . . , A n ⊢ D B 1 or . . . or B m . ( 7
)
We denote by Zar(D, S) the distributive lattice generated by this entailment relation.

Intuitively, this lattice is the lattice of truth values of the formulas of S in the dynamical algebraic structure D. The (complete) Zariski lattice of a dynamical algebraic structure D is defined by taking for S the set Clat(D) of all closed atomic formulas of D. It is denoted by Zar(D, T ), or by Zar(D), or by a particular name corresponding to the theory T .

The dual spectral space is called the Zariski spectrum of the dynamical algebraic structure D, or it can also be given a special name.

Finally, the Krull dimension of D is by definition equal to Kdim(Zar(D)). The definition of Vdim(R) in the second constructive approach to valuative dimension (page E12) is given according to this scheme.

Three constructive definitions of the valuative dimension

Minimal pp-closure of a reduced ring

We recall here some essential results given in Lombardi and Quitté 2015. If the context is clear, we denote by a ⊥ the annihilator of the element a in R. We also use the notation a ⊥ for the annihilator of an ideal a.

Lemma 2.1. Let R be a reduced ring and a ∈ R. We define

R {a} def = R a ⊥ × R (a ⊥ ) ⊥
and we denote by ψ a : R → R {a} the canonical homomorphism.

1. ψ a (a) ⊥ is generated by the idempotent (0, 1); therefore ψ a (a

) ⊥ = (1, 0) ⊥ .
2. ψ a is injective (we hence identify R with a subring of R {a} ).

3. Let b be an ideal in R {a} ; then the ideal

ψ -1 a (b ⊥ ) = b ⊥ ∩ R is an annihilator in R. 4. The ring R {a} is reduced.
Lemma 2.2. Let R be reduced and a, b ∈ R. Then, with the notation of Lemma 2.1, the two rings (R {a} ) {b} and (R {b} ) {a} are canonically isomorphic.

Note. The case where ab = 0 is typical: when we meet it, we should like to split the ring into components where things are "clear". The previous construction then gives the three components

R (ab ⊥ ) ⊥ , R (a ⊥ b) ⊥ and R (a ⊥ b ⊥ ) ⊥ .
In the first one, a is regular and b = 0; in the second one, b is regular and a = 0; in the third one, a = b = 0. Let us denote by R red = R/ R 0 the reduced ring generated by R.

Theorem and definition 2.4 (minimal pp-closure).

Let R be a reduced ring. We can define a ring R min as a filtered colimit by iterating the basic construction of replacing E (the ring "in progress", which contains R) by

E {a} def = E a ⊥ × E (a ⊥ ) ⊥ = E/Ann E (a) × E/Ann E (Ann E (a))
when a runs through R.

1. This ring R min is a pp-ring, it contains R and it is integral over R.

For any

x ∈ R min , x ⊥ ∩ R is an annihilating ideal in R.
This ring R min is called the minimal pp-closure of R. When R is not necessarily reduced, one takes R min def = (R red ) min .

We denote by P n the set of finite subsets of {1, . . . , n}. Here is a description of each ring obtained at a finite level of the R min construction. Lemma 2.5. Let R be a reduced ring and (a) = (a 1 , . . . , a n ) a sequence of n elements of R. For I ∈ P n , we denote by a I the ideal

a I = i∈I a i ⊥ j / ∈I a j ⊥ = a i ; i ∈ I ⊥ j / ∈I a j ⊥ .
Then R min contains the following ring: the product

R {a} = I∈Pn R/a I of 2 n quotient rings of R (some possibly zero).
We denote by B(R) the Boolean algebra of idempotents of the ring R.

Lemma 2.6.

1. Let R be a pp-ring. (a) R min = R. (b) R[X] is a pp-ring, and B(R) = B(R[X]).
2. For any ring R we have a canonical isomorphism

R min [X 1 , . . . , X n ] ≃ (R[X 1 , . . . , X n ]) min .
Our suggestion is that the proper generalisation of the notion of the field of fractions of a ring R is not the ring Frac R but the reduced zero-dimensional ring Frac R min .

First constructive approach to the valuative dimension: vdim

In the book Lombardi and Quitté 2015, the authors use the notation Vdim(R) instead of vdim(R). In this article, we prefer to reserve this notation for the notion defined by Coquand. So we use vdim for the definition given in the book.

The following definition is constructive because we have a constructive definition of Krull dimension. The subsequent Theorem 2.8 is furthermore proved constructively. So, for the case of an integral domain, it provides a constructive proof for the equivalence of Items 2, 3 and 4 in the classical Theorem 1.1. 1. If R is a pp-ring, the valuative dimension is defined as follows. If n ∈ N and K = Frac R, we say that the valuative dimension of R is less than or equal to n and we write vdim R n if for any sequence

(x 1 , . . . , x m ) in K we have Kdim R[x 1 , . . . , x m ] n. By convention vdim R = -1 if R is trivial.
2. In the general case we define "vdim R n" by "vdim R min n". 5

For n = 0, -1, we have vdim R = n ⇐⇒ Kdim R = n. We note that, as with the Krull dimension, we have not really defined vdim R as an element of N ∪ {∞}: only the property "vdim R n" is well defined, constructively, for any integer n -1.

Theorem 2.8 (Lombardi and Quitté 2015, Theorem XIII-8.19). The following equivalences are valid.

1. If n 1 and k -1, then vdim R k ⇐⇒ vdim R[X 1 , . . . , X n ] n + k. ( 8
)
If R is nontrivial and vdim R < ∞, this means intuitively that we have an equality

vdim R[X 1 , . . . , X n ] = n + vdim R. 2. If n 0, then vdim R n ⇐⇒ Kdim R[X 1 , . . . , X n ] 2n. (9)
3. In the case where R is a pp-ring, we also have the equivalence (for n 0)

vdim R n ⇐⇒ Kdim R[x 1 , . . . , x n ] n for all x 1 , . . . , x n ∈ Frac R.
Item 2 is correct within classical mathematics for the valuative dimension Vdim as defined in Cahen 1990.

Second approach: valuative lattice and valuative spectrum, Vdim

First of all let us recall that concerning the dimension of a distributive lattice or of the dual spectral space, there are three constructively equivalent approaches. The historically first one is the one defined by [START_REF] Joyal | Les théorèmes de Chevalley-Tarski et remarques sur l'algèbre constructive[END_REF], taken up in Coquand andPersson 2001 andCoquand 2009. The second one comes from the notion of potential chain of prime ideals of a commutative ring introduced by Lombardi (2006). The third one is based on the notion of "boundary" ideal (or "boundary" filter) and gives rise to a definition by induction. The equivalence of these notions is essentially proven in Coquand and Lombardi 2003 and treated in great detail in Coquand and Lombardi 2018. In the case of a subring R of a discrete field K, Coquand (2009) defines the valuative lattice Val(K, R) as the distributive lattice which translates the valid rules for the predicate Vr (introduced below) in the dynamical theory Val (K, R) of valuation rings of the field K with subring R. 6 Finally Val(R) is an abbreviated notation for the lattice Val(Frac R, R).

5 Consider in this footnote Vdim R as defined in Cahen 1990 and recalled in the introduction. Lombardi and Quitté (2015) show that within classical mathematics vdim R d ⇐⇒ Vdim R d. Hence this proves that Vdim R = Vdim R min within classical mathematics. This is a way to reduce the general case to the integral case without using prime ideals.

6 Without however using as such the language of dynamical theories.

The dynamical algebraic structure Val (K, R) can be described as the dynamical theory built on the signature

(• = 0, Vr(•); 0, 1, • + •, -•, • × •, (a) a∈K )
in which the elements of K are constants of the theory. 7 First there are the axioms of nontrivial discrete fields on the language of commutative rings.

• ⊢ 0 = 0

• x = 0, y = 0 ⊢ x + y = 0 • 1 = 0 ⊢ ⊥ • x = 0 ⊢ xy = 0 • ⊢ x = 0 or ∃y xy = 1
Then we add the diagram of K:

• ⊢ 0 K = 0 • ⊢ 1 K = 1 • ⊢ a + b = c (if a + b = K c) • ⊢ ab = c (if ab = K c)
Finally there are the axioms describing the properties of the predicate Vr(x) which means that x belongs to the potential valuation ring of the field K.

• ⊢ Vr(a) (if a ∈ R) • Vr(x), Vr(y) ⊢ Vr(x + y) • Vr(x), Vr(y) ⊢ Vr(xy) • xy = 1 ⊢ Vr(x) or Vr(y)
The lattice Val(K, R) is then the distributive lattice generated by the entailment relation ⊢ Val,K,R on K × defined by the equivalence

x 1 , . . . , x n ⊢ Val,K,R y 1 , . . . , y m def ⇐⇒ Vr(x 1 ), . . . , Vr(x n ) ⊢ Val (K,R) Vr(y 1 ) or . . . or Vr(y m ). ( 10
)
Finally we denote Val(Frac R, R) by Val(R).

In this framework, the valuative dimension of R, which we shall denote by Vdim R, is defined as Kdim(Val(R)). Coquand (2009, Theorem 8) gives a Valuativstellensatz in the form of the following equivalence (for y i and x j ∈ K × ):

Vr(x 1 ), . . . , Vr(x n ) ⊢ Val (K,R) Vr(y 1 ) or . . . or Vr(y m ) ⇐⇒ 1 ∈ y -1 1 , . . . , y -1 m R[x 1 , . . . , x n , y -1 1 , . . . , y -1 m ].
Chasing the denominators gives the following equivalent formulation:

y p 1 1 • • • y pm m = Q(x 1 , . . . , x n , y 1 , . . . , y m ) with Q ∈ R[X 1 , . . . , X n , Y 1 , . . . , Y m ] a polynomial whose monomials have a degree in (Y 1 , . . . , Y m ) strictly less than (p 1 , . . . , p m ). (11)
What happens if we accept that some x j 's or y i 's are possibly zero? Since the rule ⊢ Vr(0) is valid, the rule

• Vr(x 1 ), . . . , Vr(x n ) ⊢ Vr(y 1 ) or . . . or Vr(y m )
is always satisfied if one of the y i 's is zero; and if one of the x j 's is zero, it is equivalent to the same rule where we have deleted the corresponding Vr(x j )'s to the left of ⊢. The same facts can be observed for the Valuativstellensatz expressed in the form [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF]: if one of the y i 's is zero, we take Q = 0; if one of the x j 's is zero, then it plays no part in [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF]. Thus the Valuativstellensatz in the form [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF] is always valid, which avoids reasoning case by case.

The lattice Val R can thus be characterised as the distributive lattice generated by the entailment relation ⊢ Val R on K defined by the equivalence

x 1 , . . . , x n ⊢ Val R y 1 , . . . , y m def ⇐⇒ ∃p 1 , . . . , p m 0 ∃Q ∈ R[X, Y ] y p 1 1 • • • y pm m = Q(x 1 , . . . , x n , y 1 , . . . , y m ), the monomials of Q of degree in Y strictly less than (p 1 , . . . , p m ). (12)
To make the calculations to come more readable, we introduce the predicate

V ′ (x) def ⇐⇒ ∃u(ux = 1, Vr(u)).
In other words, we add a predicate V ′ (x) to the signature with the two axioms

• ux = 1, Vr(u) ⊢ V ′ (x) • V ′ (x) ⊢ ∃u (ux = 1, Vr(u))
The new theory is a conservative extension of the former one. Moreover we have the following valid rules which allow to compute Vr from V ′

• ⊢ Vr(0)

• Vr(x) ⊢ x = 0 or ∃u (ux = 1, V ′ (u)) • ux = 1, V ′ (u) ⊢ Vr(x)
We can read V ′ (x) as Vr(1/x), where Vr(1/0) ⊢ ⊥ (collapse of the theory). The predicate V ′ (x) means that the element x of K is not a residually zero element of V. In particular, this predicate satisfies the following axioms in the dynamical theory considered:

• ⊢ V ′ (a) (if a ∈ R × ) • V ′ (x + y) ⊢ V ′ (x) or V ′ (y) • V ′ (x), V ′ (y) ⊢ V ′ (xy) • V ′ (0) ⊢ ⊥ • xy = 1 ⊢ V ′ (x) or V ′ (y)
The Valuativstellensatz becomes, this time without restriction on x j and y i ∈ K,

V ′ (y 1 ), . . . , V ′ (y m ) ⊢ V ′ (x 1 ) or . . . or V ′ (x n ) ⇐⇒ 1 ∈ x 1 , . . . , x n R[x 1 , . . . , x n , y -1 1 , . . . , y -1 m ],
where the right-hand side must be rewritten in the following form to avoid 0 -1 :

∃p 1 , . . . , p m ∃P 1 , . . . , P n ∈ R[X, Y ] y p 1 1 . . . y pm m = x 1 P 1 (x, y) + • • • + x n P n (x, y)
, where the multiexponents of Y in the P j 's are all (p 1 , . . . , p m ). (13) If one of the y i 's is zero, the equality is automatically satisfied by taking the P j 's identically zero.

This predicate V ′ is the predicate denoted by Nrn in the article Lombardi 2000 which gives a very general Valuativstellensatz. Remark 2.9. A lattice Val ′ R associated to the predicate V ′ can be introduced. We can then show that Val ′ R is isomorphic to the lattice opposite to Val R. This is because x → x -1 is a bijection of K × onto itself. In this article, we only use the fact that the characterisations ( 11) and ( 13) are equivalent.

We shall introduce the valuative lattice of an arbitrary ring in our very last subsection on page E22.

Third approach: graded monomial order, dimv

We denote by < lex the monomial order on Z n corresponding to the lexicographic order.

A rational monomial graded order < M on Z n or, equivalently, on the monomials of

R[X ±1 1 , . . . , X ±1 1 ]
, is defined by means of a matrix M ∈ Mat n (N) invertible in Mat n (Q) with the coefficients of the first row all > 0, as follows:

(e 1 , . . . , e n ) < M (f 1 , . . . , f n ) def ⇐⇒ M •    e 1 . . . e n    < lex    f 1 . . . f n    .
When the coefficients of the first row of M are equal to 1, the monomial order < M is an order subordinate to total degree. The monomial graded lexicographic order < grlex is the one defined by the matrix

       1 1 . . . 1 1 0 0 . . . 0 0 1 0 0 . . . . . . 0 0 . . . 1 0       
. Lombardi (2006) characterises constructively the Krull dimension of an arbitrary ring R by the equivalence between Kdim R n and the fact that for all x 0 , . . . , x n ∈ R we have a polynomial P ∈ R[X 0 , . . . , X n ] which vanishes at (x 0 , . . . , x n ) and whose trailing coefficient for the lexicographic order is equal to 1. For example, Kdim R 1 if and only if, for all x 0 , x 1 ∈ R we can find an equality 0 = x e 0 0 (x e 1 1 (1 + c 1 x 1 ) + c 0 x 0 ): here the c i 's are elements of R or just as well elements of R[x 0 , x 1 ]. Kemper and Viet Trung (2014) show, within classical mathematics, that for a noetherian ring one can characterise the Krull dimension in the same way using an arbitrary monomial order. Kemper and Yengui (2020) show, within classical mathematics, that for an arbitrary ring one can characterise the valuative dimension in the same way, provided one uses a graded rational monomial order instead of the lexicographic order.

In other words, we can paraphrase them by the following definition.

Definition 2.10. We say that dimv R n if, considering a graded rational monomial order < M , we have for all x 0 , . . . , x n ∈ R a polynomial P ∈ R[X 0 , . . . , X n ] which vanishes at (x 0 , . . . , x n ) and whose trailing coefficient for the order < M is equal to 1.

The result in Kemper and Yengui 2020 is then the following.

Theorem 2.11.

This definition of dimv R

n does not depend on the matrix M considered.

2. It is equivalent within classical mathematics to the fact that the valuative dimension of R is n.

By convention dimv R = -1 means that the ring is trivial.

In fact, the proof of Theorem 2.11 in Kemper and Yengui 2020 is clearly constructive for the case of an integral ring R: for all n 0 we have constructively the equivalence vdim R n (Definition 2.7.1) ⇐⇒ dimv R n (Definition 2.10). ( 14)

3 Constructive equivalence of the three constructive definitions

vdim = dimv
Let us state a first lemma which extends ( 14) to the pp-case.

Lemma 3.1. For a pp-ring R we have the equivalence

vdim R d ⇐⇒ dimv R d. (15)
Proof. We take the constructive proof of ( 14) given in the integral case and use the elementary local-global machinery No. 1.

To extend the constructive equivalence (14) from the case of an integral ring to the case of an arbitrary ring, given that in the general case we have defined vdim R d as meaning vdim R min d, and given Lemma 3.1, we need only prove constructively the equivalence

dimv R d ⇐⇒ dimv R min d. (16)
In particular, this implies constructively the analogue of Equivalence ( 9) for dimv.

Equivalence ( 16) reduces to the following two lemmas.

Lemma 3.2. We always have

dimv R d ⇐⇒ dimv R red d. ( 17
)
Proof. The proof is left to the reader.

Lemma 3.3. Let R be a reduced ring and a ∈ R. Then we have

dimv R d ⇐⇒ dimv R {a} d. ( 18
)
Proof. The implication =⇒ is quite simple. On the one hand, the implication

dimv R d =⇒ dimv(R/a) d
is clear for any quotient R/a. And on the other hand we see that

dimv B d and dimv C d =⇒ dimv(B × C) d.
Let us consider the converse implication. Consider x 0 , . . . , x d ∈ R. We have first of all a polynomial P 1 (X 0 , . . . , X d ) ∈ R[X] with trailing coefficient equal to c 1 = 1 + y 1 and such that P 1 (x 0 , . . . , x d ) = z 1 with y 1 , z 1 ∈ a ⊥ . We have moreover a polynomial P 2 (X) with trailing coefficient c 2 = 1 + y 2 and such that P 2 (x) = z 2 , with y 2 , z 2 ∈ (a ⊥ ) ⊥ . We then have

y 1 y 2 = y 1 z 2 = z 1 y 2 = z 1 z 2 = 0.
If we multiply P 1 and P 2 by suitable monomials, we can assume that their trailing monomials coincide. Then

Q 2 = P 2 -y 2 P 1 has trailing coefficient (1+y 2 )-y 2 (1 + y 1 ) = 1 and satisfies Q 2 (x) = z 2 . Similarly Q 1 = P 1 -y 1 P 2 has trailing coefficient (1 + y 1 ) - y 1 (1 + y 2 ) = 1 and satisfies Q 1 (x) = z 1 . So the polynomial Q 1 Q 2 suits.
vdim = Vdim in the integral case Lemma 3.4. For an integral ring R, and for an integer n -1, the following applies

Vdim R n =⇒ vdim R n.
Proof. The article Coquand 2009 shows on the one hand that

Vdim R n =⇒ Kdim R n and on the other hand that Vdim R n =⇒ Vdim R[X] n + 1. Therefore Vdim R n =⇒ Kdim R[X 1 , . . . , X n ] 2n. In Lombardi and Quitté 2015 it is shown that Kdim R[X 1 , . . . , X n ] 2n =⇒ vdim R n.

Proof of the converse inequality

We shall prove vdim n =⇒ Vdim n by constructing complementary sequences. In order to understand the proof, we shall treat first the cases n = 2, 3, 4: when n = 2, the complementary sequence consists of elements of the form V ′ (y), whereas the cases n = 3 and n = 4 provide successive hints for constructing it in the distributive lattice generated by such elements. vdim 2 =⇒ Vdim 2 Suppose that we have x 0 , x 1 , x 2 nonzero in the field of fractions K of R. We are looking for y 0 , y 1 , y 2 ∈ K (we know that y 2 is zero) such that:

V ′ (x 0 ) ∨ V ′ (y 0 ) = 1, (19) V ′ (x 0 ) ∧ V ′ (y 0 ) V ′ (x 1 ) ∨ V ′ (y 1 ), (20) V ′ (x 1 ) ∧ V ′ (y 1 ) V ′ (x 2 ) ∨ V ′ (y 2 ) = V ′ (x 2 ) (since y 2 = 0), (21) V ′ (x 2 ) ∧ V ′ (y 2 ) = 0 (this is guaranteed by y 2 = 0). (19) amounts to saying that 1 = x 0 , y 0 in R[x 0 , y 0 ]. (20) amounts to saying that 1 = x 1 , y 1 in R[x -1 0 , y -1 0 , x 1 , y 1 ]. (21) amounts to saying that 1 = x 2 in R[x -1 1 , y -1 1 , x 2 ]. We use the fact that Kdim(R[x 0 , x 1 , x 2 ]) 2.
We have a polynomial P ∈ R[X 0 , X 1 , X 2 ] with trailing coefficient 1 (for the lexicographic monomial order with X 2 > X 1 > X 0 ) which vanishes at (x 0 , x 1 , x 2 ). Let X n 2 X m 1 X ℓ 0 be the trailing monomial of P . Dividing P (x 0 , x 1 , x 2 ) by x n 2 x m 1 x ℓ 0 , we obtain an equality

1 + x 0 f 0 (x 0 ) + x 1 f 1 (x 1 , x ±1 0 ) + x 2 f 2 (x 2 , x ±1 1 , x ±1 0 ) = 0, where f 0 ∈ R[X 0 ], f 1 ∈ R[X 1 , X ±1 0 ] and f 2 ∈ R[X 2 , X ±1 1 , X ±1 0 ]
(the x 0 f 0 (x 0 ) comes from monomials of P other than M whose degree in X 2 is equal to n and the degree in

X 1 is equal to m, x 1 f 1 (x 1 , x ±1
0 ) comes from the other monomials of P whose degree in X 2 is equal to n, while x 2 f 2 (x 2 , x ±1

1 , x ±1 0 ) comes from monomials of P whose degree in X 2 is > n). For some r 0 , r 1 ∈ N, we have:

1 + x 0 f 0 (x 0 ) + x r 0 0 x 1 g 1 (x 1 , x -1 0 ) + x 2 x r 1 1 g 2 (x 2 , x 1 , x -1 0 ) = 0, where g 1 ∈ R[X 1 , X -1 0 ] and g 2 ∈ R[X 2 , X 1 , X -1 0 ]. We see that y 0 = 1 + x 0 f (x 0 )
x r 0 0 and

y 1 = x 2 x r 1 1 suit (note that x 2 = x r 1 1 y 1 ∈ R[x 1 , y 1 ] ⊆ R[x -1 0 , y -1 0 , x 1 , y 1 ]
). Let us consider an example of collapse:

x 0 x 2 1 x 2 2 + 2x 2 0 x 2 1 x 2 2 + 3x 4 1 x 2 2 + x 2 0 x 5 1 x 2 2 + 3x 3 2 + 2x 1 x 3 2 + x 2 0 x 3 1 x 4 2 = 0. Dividing by x 0 x 2 1 x 2 2
, we obtain an equality

1 + 2x 2 0 + x 0 x 1 3x 1 x 2 0 + x 2 1 + x 2 x 2 1 3 x 2 0 + 2x 1 x 2 0 + x 2 x 3 1 = 0.
We see that y 0 = 1 + 2x 2 0

x 0 and

y 1 = x 2 x 2 1 suit. vdim 3 =⇒ Vdim 3 Let x 0 , x 1 , x 2 ,
x 3 be nonzero in the field of fractions K of R. We look for u 0 , u 1 , u 2 , u 3 in the distributive lattice generated by the V ′ (x) which form a complementary sequence of x 0 , x 1 , x 2 , x 3 (see the inequalities in (4)). In other words:

1 = V ′ (x 0 ) ∨ u 0 , V ′ (x 0 ) ∧ u 0 V ′ (x 1 ) ∨ u 1 , . . . , V ′ (x 2 ) ∧ u 2 V ′ (x 3 ) ∨ u 3 , V ′ (x 3 ) ∧ u 3 = 0.
We propose to find the u i in the form

u 0 = V ′ (y 0 ), u 1 = V ′ (y 1 ) ∧ V ′ (x 0 ), u 2 = V ′ (y 2 ), u 3 = 0 with y 0 , y 1 , y 2 ∈ K such that V ′ (x 0 ) ∨ V ′ (y 0 ) = 1, (22)
V ′ (x 0 ) ∧ V ′ (y 0 ) V ′ (x 1 ) ∨ u 1 = V ′ (x 1 ) ∨ V ′ (y 1 ) ∧ V ′ (x 1 ) ∨ V ′ (x 0 ) or also V ′ (x 0 ) ∧ V ′ (y 0 ) V ′ (x 1 ) ∨ V ′ (y 1 ) and (23) V ′ (x 0 ) ∧ V ′ (y 0 ) V ′ (x 1 ) ∨ V ′ (x 0 ), ( 24
) V ′ (x 1 ) ∧ u 1 V ′ (x 2 ) ∨ V ′ (y 2 ), (25) V ′ (x 2 ) ∧ V ′ (y 2 ) V ′ (x 3 ) ∨ u 3 = V ′ (x 3 ), ( 26
) V ′ (x 3 ) ∧ u 3 = 0 (this is guaranteed by u 3 = 0). (22) amounts to saying that 1 ∈ x 0 , y 0 in R[x 0 , y 0 ]. (23) amounts to saying that 1 ∈ x 1 , y 1 in R[x -1 0 , y -1 0 , x 1 , y 1 ]. (24) is always satisfied since V ′ (x 0 ) ∧ V ′ (y 0 ) V ′ (x 0 ) V ′ (x 1 ) ∨ V ′ (x 0 ). (25) amounts to saying that 1 ∈ x 2 , y 2 in R[x -1 1 , y -1 1 , x -1 0 , x 2 , y 2 ]. (26) amounts to saying that 1 ∈ x 3 in R[x -1 2 , y -1 2 , x 3 ]. We use the fact that Kdim(R[x 0 , x 1 , x 2 , x 3 ])
3. We have a polynomial P ∈ R[X 0 , X 1 , X 2 , X 3 ] with trailing coefficient 1 (for the lexicographic monomial order with X 3 > X 2 > X 1 > X 0 ) which vanishes at (x 0 , x 1 , x 2 , x 3 ). Let X n 3 X m 2 X p 1 X q 0 be the trailing monomial of P . Dividing P (x 0 , x 1 , x 2 , x 3 ) by x m 3 x n 2 x p 1 x q 0 , we obtain an equality

1 + x 0 f 0 (x 0 ) + x 1 f 1 (x 1 , x ±1 0 ) + x 2 f 2 (x 2 , x ±1 1 , x ±1 0 ) + x 3 f 3 (x 3 , x ±1 2 , x ±1 1 , x ±1 0 ) = 0, where f 0 ∈ R[X 0 ], f 1 ∈ R[X 1 , X ±1 0 ], f 2 ∈ R[X 2 , X ±1 1 , X ±1 0 ] and f 3 ∈ R[X 3 , X ±1 2 , X ±1 1 , X ±1 0 ]: • x 0 f 0 (x 0 )
comes from monomials of P other than M whose degree in X 3 is equal to m, the degree in X 2 is equal to n and the degree in X 1 is equal to p;

• x 1 f 1 (x 1 , x ±1
0 ) comes from the other monomials of P whose degree in X 3 is equal to m and whose degree in X 2 is equal to n;

• x 2 f 2 (x 2 , x ±1
1 , x ±1 0 ) comes from the other monomials of P whose degree in X 3 is equal to m;

• x 3 f 3 (x 3 , x ±1 2 , x ±1 1 , x ±1
0 ) comes from the monomials of P whose degree in X 3 is > m. For some r 0 , r 1 ∈ N, we have

1 + x 0 f 0 (x 0 ) + x r 0 0 x 1 g 1 (x 1 , x -1 0 ) + x r 1 1 x 2 g 2 (x 2 , x -1 1 , x -1 0 ) + x 3 x r 2 2 g 3 (x 3 , x 2 , x -1 1 , x -1 0 ) = 0, ( 27
) where g 1 ∈ R[X 1 , X -1 0 ], g 2 ∈ R[X 2 , X -1 1 , X -1 0 ], and g 3 ∈ R[X 3 , X 2 , X -1 1 , X -1 0 ]. Let y 0 = 1 + x 0 f 0 (x 0 ) x r 0 0 , y 1 = y 0 + x 1 g 1 (x 1 , x -1 0 ) x r 1 1 , y 2 = x 3 x r 2 2 . Condition (22): 1 = x r 0 0 y 0 -x 0 f 0 (x 0 ) ∈ x 0 , y 0 in R[x 0 , y 0 ] (even if r 0 = 0). Condition (23): y 0 = y 1 x r 1 1 -x 1 g 1 (x 1 , x -1 0 )
; if y 0 = 0 we divide by y 0 and we obtain

1 ∈ x 1 , y 1 in R[x 1 , y 1 , x -1 0 , y -1 0 ]. Condition (26): y 2 x r 2 2 =
x 3 (and we divide by y 2 x r 2 2 if y 2 = 0). Condition (25): Equality ( 27) may be rewritten as follows:

x 2 g 2 (x 2 , x -1 1 , x -1 0 ) + y 2 g 3 (y 2 x r 2 2 , x 2 , x -1 1 , x -1 0 ) = -y 1 .
If y 1 = 0 we divide by y 1 . Moreover, we may also conclude if y 0 = 0 or y 1 = 0 (see the comment after Equality (13)).

vdim 4 =⇒ Vdim 4 Let x 0 , x 1 , x 2 , x 3 , x 4 be nonzero in the field of fractions K of R. We look for u 0 , u 1 , u 2 , u 3 , u 4 in the distributive lattice generated by the V ′ (x) which form a complementary sequence of x 0 , x 1 , x 2 , x 3 , x 4 (see the inequalities in (4)). In other words:

1 = V ′ (x 0 ) ∨u 0 , V ′ (x 0 ) ∧u 0 V ′ (x 1 ) ∨u 1 , . . . , V ′ (x 3 ) ∧u 3 V ′ (x 4 ) ∨u 4 , V ′ (x 4 ) ∧u 4 = 0. 1 + x 0 f 0 (x 0 ) + x 1 f 1 (x 1 , x ±1 0 ) + x 2 f 2 (x 2 , x ±1 1 , x ±1 0 ) + x 3 f 3 (x 3 , x ±1 2 , x ±1 1 , x ±1 0 ) + x 4 f 4 (x 4 , x ±1 3 , x ±1 2 , x ±1 1 , x ±1 0 ) = 0, where f 0 ∈ R[X 0 ], f 1 ∈ R[X 1 , X ±1 0 ], f 2 ∈ R[X 2 , X ±1 1 , X ±1 0 ], f 3 ∈ R[X 3 , X ±1 2 , X ±1 1 , X ±1 0 ], and f 4 ∈ R[X 4 , X ±1 3 , X ±1 2 , X ±1 1 , X ±1 0 ]:
• x 0 f 0 (x 0 ) comes from monomials of P other than M whose degree in X 4 is equal to ℓ, the degree in X 3 is equal to m, the degree in X 2 is equal to n and the degree in X 1 is equal to p,

• x 1 f 1 (x 1 , x ±1
0 ) comes from the other monomials of P whose degree in X 4 is equal to ℓ, the degree in X 3 is equal to m, the degree in X 2 is equal to n,

• x 2 f 2 (x 2 , x ±1
1 , x ±1 0 ) comes from the other monomials of P whose degree in X 4 is equal to ℓ and the degree in X 3 is equal to m,

• x 3 f 3 (x 3 , x ±1 2 , x ±1 1 , x ±1
0 ) comes from the monomials of P whose degree in X 4 is equal to ℓ,

• x 4 f 4 (x 4 , x ±1 3 , x ±1 2 , x ±1 1 , x ±1
0 ) comes from the monomials of P whose degree in X 4 is > ℓ.

For some r 0 , r 1 , r 2 , r 3 ∈ N, we have

1 + x 0 f 0 (x 0 ) + x r 0 0 x 1 g 1 (x 1 , x -1 0 ) + x r 1 1 x 2 g 2 (x 2 , x -1 1 , x -1 0 ) + x r 2 2 x 3 g 3 (x 3 , x -1 2 , x -1 1 , x -1 0 ) + x 4 x r 3 3 g 4 (x 4 , x 3 , x -1 2 , x -1 1 , x -1 0 ) = 0, (33)
where

g 1 ∈ R[X 1 , X -1 0 ], g 2 ∈ R[X 2 , X -1 1 , X -1 0 ], g 3 ∈ R[X 3 , X -1 2 , X -1 1 , X -1 0 ], and g 4 ∈ R[X 4 , X 3 , X -1 2 , X -1 1 , X -1 0 ]. Let y 0 = 1 + x 0 f 0 (x 0 ) x r 0 0 , y 1 = y 0 + x 1 g 1 (x 1 , x -1 0 ) x r 1 1 , y 2 = y 1 + x 2 g 2 (x 2 , x -1 1 , x -1 0 ) x r 2 2 , y 3 = x 4 x r 3 3 . Condition (28): 1 = x r 0 0 y 0 -x 0 f 0 (x 0 ) ∈ x 0 , y 0 in R[x 0 , y 0 ] (even if r 0 = 0). Condition (29): y 0 = y 1 x r 1 1 -x 1 g 1 (x 1 , x -1 0 )
; if y 0 = 0 we divide by y 0 and we obtain

1 ∈ x 1 , y 1 in R[x 1 , y 1 , x -1 0 , y -1 0 ]. Condition (30): y 1 = y 2 x r 2 2 -x 2 g 2 (x 2 , x -1 1 , x -1 0 ); if y 1 = 0 we divide by y 1 and we obtain 1 ∈ x 2 , y 2 in R[y -1 1 , x -1 1 , x -1 0 , x 2 , y 2 ]
. Condition (31): Equality (33) reads 32): y 3 x r 3 3 = x 4 (and we divide by y 3 x r 3 3 if y 3 = 0). vdim n =⇒ Vdim n Let x 0 , . . . , x n be nonzero in the field of fractions K of R. We look for u 0 , u 1 , . . . , u n in the distributive lattice generated by the V ′ (x) which form a complementary sequence of x 0 , x 1 , . . . , x n . In other words:

x 3 g 3 (x 3 , x -1 2 , x -1 1 , x -1 0 ) + y 3 g 4 (y 3 x r 3 3 , x 3 , x -1 2 , x -1 1 , x -1 0 ) = -y 2 If y 2 = 0 we divide by y 2 and get that 1 ∈ x 3 , y 3 in R[y -1 2 , x -1 2 , x -1 1 , x -1 0 , x 3 , y 3 ]. Condition (
We use the fact that Kdim R[x 0 , . . . , x n ] n. We have a polynomial P ∈ R[X 0 , . . . , X n ] with trailing coefficient 1 (for the lexicographic monomial order with X n > X n-1 > • • • > X 0 ) which vanishes at (x 0 , . . . , x n ). Let X qn n • • • X q 0 0 be the trailing monomial of P . By dividing P (x 0 , . . . , x n ) by x qn n • • • x q 0 0 , we obtain an equality

1 + x 0 f 0 (x 0 ) + x 1 f 1 (x 1 , x ±1 0 ) + . . . + x n f n (x n , x ±1 n-1 , . . . , x ±1 0 ) = 0, where f 0 ∈ R[X 0 ], f 1 ∈ R[X 1 , X ±1 0 ], . . . , f n ∈ R[X n , X ±1 n-1 , . . . , X ±1 0 ]
. For some r 0 , . . . , r n ∈ N, we have

1 + x 0 f 0 (x 0 ) + x r 0 0 x 1 g 1 (x 1 , x -1 0 ) + • • • + x r n-3 n-3 x n-2 g n-2 (x n-2 , x -1 n-3 , . . . , x -1 0 ) + x r n-2 n-2 x n-1 g n-1 (x n-1 , x -1 n-2 , . . . , x -1 0 ) + x n x r n-1 n-1 g n (x n , x n-1 , x -1 n-2 , . . . x -1 0 ) • • • = 0, where g 1 ∈ R[X 1 , X -1 0 ], . . . , g n-1 ∈ R[X n-1 , X -1 n-2 , . . . , X r 0 -1], g n ∈ R[X n , X n-1 , X -1 n-2 , . . . , X -1 0 ]. Let y 0 = 1 + x 0 f 0 (x 0 ) x r 0 0 , y 1 = y 0 + x 1 g 1 (x 1 , x -1 0 ) x r 1 1 , . . . , y n-2 = y n-3 + x n-2 g n-2 (x n-2 , x -1 n-3 , . . . , x -1 0 ) x r n-2 n-2 , y n-1 = x n x r n-1 n-1
.

It is then sufficient to take

u 0 = V ′ (y 0 ), u 1 = V ′ (y 1 ) ∧ V ′ (x 0 ), u 2 = V ′ (y 2 ) ∧ V ′ (x 1 ) ∧ V ′ (x 0 ), . . . , u n-2 = V ′ (y n-2 ) ∧ V ′ (x n-3 ) ∧ • • • ∧ V ′ (x 0 ), u n-1 = V ′ (y n-1
), and u n = 0.

vdim = Vdim in the general case

We note that when R is a pp-ring, the ring Frac(R) is a reduced zero-dimensional ring. Moreover a discrete field is a reduced zero-dimensional ring in which any idempotent is equal to 0 or 1.

We then start with the following remark which follows from the elementary localglobal machinery No. 1.

Lemma 3.5. Let R be a pp-ring. Let us define Val(R) := Val(Frac(R), R) and Vdim(R) := Kdim(Val(R)) as in (10) by replacing K by Frac(R). Then we obtain the equality vdim(R) = Vdim(R) as in the integral case.

In the remainder of this paragraph, we do not give proofs: we refer to the general study Lombardi and Mahboubi 2023.

We define a dynamical theory val as follows. We consider the signature

(• | •; • + •, • × •, -•, 0, 1).
The axioms are as follows.

Col val 0 | 1 ⊢ ⊥ (collapse) av1 ⊢ 1 | -1 av2 a | b ⊢ ac | bc Av1 a | b, b | c ⊢ a | c Av2 a | b, a | c ⊢ a | b + c AV1 ⊢ a | b or b | a AV2 ax | bx ⊢ a | b or 0 | x
The equality x = 0 is defined as an abbreviation for x | 0.

Definition 3.6.

1. If R is a commutative ring, the dynamical algebraic structure val (R) is obtained by taking as presentation the positive diagram of the ring R.

2. If k ⊆ R are two rings,8 or more generally if ϕ : k → R is an algebra, we denote by val (R, k) the dynamical algebraic structure whose presentation is given by

• the positive diagram of K as a commutative ring;

• the axioms ⊢ 1 | ϕ(x) for the elements x of k.

The two dynamical algebraic structures val (R) and val (R, Z), where Z is the smallest subring of R, are canonically isomorphic. Definition 3.7. Let k be a subring of a ring R. We define the distributive lattice val(R, k) through the entailment relation ⊢ R,k,val on the set R × R given by the following equivalence.

(a

1 , b 1 ), . . . , (a n , b n ) ⊢ R,k,val (c 1 , d 1 ), . . . , (c m , d m ) def ⇐⇒ a 1 | b 1 , . . . , a n | b n ⊢ val (R,k) c 1 | d 1 or . . . or c m | d m . ( 34
)
The following result can be proved.

Lemma 3.8. Let R be an integral ring with field of fractions K. We have natural morphisms Val(K, R) → val(K, R) and val(R, R) → val(K, R). These are isomorphisms.

The following definition is therefore reasonable. We shall see that it coincides with the one given in Lemma 3.5 in the case of pp-rings. Definition 3.9. Let R be an arbitrary commutative ring. We define Vdim(R)

n by Kdim(val(R, R))

n.

This dimension coincides with the one already defined when R is integral. But it is not in general equal to the dimension of the lattice val(Frac(R), R).

From our point of view, this means that Frac(R min ) is a much better substitute than Frac(R) for the field of fractions when R is not an integral ring. In fact R min coincides with Frac(R) only for pp-rings.

Finally, we can prove the following theorem.

Theorem 3.10. The distributive lattices val(R, R) and val(R min , R min ) ≃ val(Frac(R min ), R min )

have the same Krull dimension.

With Lemma 3.5 and Definitions 3.6 and 3.9 this completes the work. Note. We could have defined Vdim(R) = Vdim(R min ) directly without using the theory val , but this would have been an ad hoc definition, because Vdim(R) has no direct natural definition for an arbitrary ring if we use only the theory Val .

Définition et propriétés caractéristiques de la dimension valuative en mathématiques classiques

En mathématiques classiques, la dimension valuative d'un anneau intègre R est la longueur maximum n d'une chaine d'anneaux de valuation

V 0 • • • V n = K du corps de fractions K = Frac R qui contiennent R.
La dimension valuative d'un anneau arbitraire est définie comme la borne supérieure des dimensions valuatives de ses quotients intègres (Cahen 1990).

Un corps discret est de dimension valuative 0. La dimension de l'anneau trivial, qui ne possède pas de quotient intègre, est par convention égale à -1.

En mathématiques classiques on démontre les équivalences suivantes.

Théorème 1.1. Soit R un anneau commutatif intègre non trivial avec K = Frac(R).

Les propriétés suivantes sont équivalentes.

1. R est de dimension valuative n.

Pour tout entier

k et tous x 1 , . . . , x k ∈ K, Kdim(R[x 1 , . . . , x k ]) n. 3. Pour tout entier k, Kdim(R[X 1 , . . . , X k ]) n + k. 4. Kdim(R[X 1 , . . . , X n ]) 2n.
En outre, sans supposer R intègre, mais en le supposant non trivial, les points Nous proposons dans la section 2 de rappeler des définitions constructives précises concernant ces trois approches.

Nous notons Vdim(R) une définition constructive correspondant à la caractérisation donnée dans le poin 1 du théorème 1.1.

Nous notons vdim(R) une définition constructive correspondant à la caractérisation donnée dans le point 3 du théorème 1.1.

Nous notons dimv(R) la définition constructive donnée par Kemper et Yengui.

Ces définitions constructives ont déjà été démontrées équivalentes à la définition classique en mathématiques classiques, au moins dans le cas d'un anneau intègre. Dans la section 3 nous démontrons constructivement l'équivalence de ces trois définitions en toute généralité. Un anneau est dit localement sans diviseur de zéro 2 lorsque, la règle suivante est satisfaite

Terminologie constructive de base

• ab = 0 ⊢ ∃s, t (sa = 0, tb = 0, s + t = 1).

1. En mathématiques constructives, ou a son sens intuitif, i.e. l'une des deux propriétés est valide de manière explicite. Sachant d'un anneau est sans diviseur de zéro avec un ou explicite, il n'y a pas de démonstration constructive que tout élément est nul ou régulier avec un ou explicite.

2. En anglais, un pf-ring : les idéaux principaux sont plats.

Alors, dans R[1/s] l'élément a est nul, et dans R[1/t] l'élément b est nul 3 . Un anneau est dit quasi intègre 4 si l'annulateur de tout élément a est engendré par un idempotent (nécessairement unique), noté 1e a . On a R R[1/e a ] × R/ e a . Dans l'anneau R[1/e a ], l'élément a est régulier, et dans R/ e a , a est nul 5 . Un anneau quasi intègre est localement sans diviseur de zéro mais la réciproque n'est pas valable. Notons que l'on a e ab = e a e b , e a a = a et e 0 = 0. Les anneaux quasi intègres ont une définition purement équationnelle. Supposons en effet qu'un anneau commutatif soit muni d'une loi unaire a → a • qui vérifie les trois axiomes suivants :

a • a = a, (ab) • = a • b • , 0 • = 0. (1)
Alors, pour tout a ∈ R, Ann(a) = 1a Le fait de pouvoir scinder systématiquement en deux composantes un anneau quasi intègre conduit à la méthode générale suivante. La différence essentielle avec le lemme de scindage précédent est que l'on ne connait pas à priori la famille finie d'éléments qui va provoquer le scindage.

Machinerie locale-globale élémentaire n o 1. La plupart des algorithmes qui fonctionnent avec les anneaux intègres non triviaux peuvent être modifiés de manière à fonctionner avec les anneaux quasi intègres, en scindant l'anneau en deux composantes chaque fois que l'algorithme écrit pour les anneaux intègres utilise le test cet élément est-il nul ou régulier ? . Dans la première composante l'élément en question est nul, dans la seconde il est régulier.

Dans un corps valué (K, V) on dit que x divise y et on écrit x | y s'il existe un z ∈ V tel que xz = y. On note Γ(V) (ou Γ si le contexte est clair) le groupe K × /V × (noté additivement), avec la relation induite par la relation | dans K × . On note Γ ∞ = Γ ∪ {∞} (où ∞ est un élément maximum). Dans ces conditions, l'application naturelle v : K → Γ ∞ est appelée la valuation du corps valué. On a

v(xy) = v(x) + v(y), et v(x + y) min(v(x), v(y)) avec égalité si v(x) = v(y). On a aussi V = { x ∈ K ; v(x) 0 } et V × = { x ∈ K ; v(x) = 0 }.

Dimension des treillis distributifs

Dans ce paragraphe nous expliquons la définition constructive de la dimension d'un treillis distributif. Un treillis distributif T peut être vu comme l'ensemble des ouverts quasicompacts d'un espace spectral, que l'on appelle l'espace dual de T. La définition constructive de cette dimension correspond à la définition de la dimension d'un espace spectral en mathématiques classiques. En mathématiques classiques c'est aussi la longueur maximum d'une chaine croissante d'idéaux premiers du treillis voir le théorème 1.5.

Un idéal b d'un treillis distributif (T, ∧, ∨, 0, 1) est une partie qui satisfait les contraintes :

0 ∈ b x, y ∈ b =⇒ x ∨ y ∈ b x ∈ b, z ∈ T =⇒ x ∧ z ∈ b    (2)
On note T/(b = 0) le treillis quotient obtenu en forçant les éléments de b à être nuls. Un idéal principal est un idéal engendré par un seul élément a, il est noté ↓a. On a ↓a = { x ∈ T ; x a }. L'idéal ↓a, muni des lois ∧ et ∨ de T est un treillis distributif dans lequel l'élément maximum est a. L'injection canonique ↓a → T n'est pas un morphisme de treillis distributifs parce que l'image de a n'est pas égale à 1 T . Par contre l'application T → ↓a, x → x ∧ a est un morphisme surjectif, qui définit donc ↓a comme une structure quotient T/(a = 1).

La notion de filtre est la notion opposée (c'est-à-dire obtenue en renversant la relation d'ordre) à celle d'idéal.

Une règle particulièrement importante pour les treillis distributifs, appelée coupure, est la suivante

(x ∧ a b) ∧ (a x ∨ b) ⇒ (a b). (3)
Si A ∈ P fe (T) (ensemble des parties finiment énumérées de T) on notera

A := x∈A x et A := x∈A x.
On note A ⊢ B ou A ⊢ T B la relation définie comme suit sur l'ensemble P fe (T) :

A ⊢ B def ⇐⇒ A B.
Cette relation vérifie les axiomes suivants, dans lesquels on écrit

x pour {x} et A, B pour A ∪ B. x ⊢ x (R) si A ⊢ B alors A, A ′ ⊢ B, B ′ (M) si (A, x ⊢ B) et (A ⊢ B, x) alors A ⊢ B (T ).
On dit que la relation est réflexive, monotone et transitive. La troisième règle (transitivité) peut être vue comme une généralisation de la règle (3) et s'appelle également la règle de coupure.

Définition 1.3. Pour un ensemble S arbitraire, une relation sur P fe qui est réflexive, monotone et transitive est appelée une relation implicative (en anglais, entailment relation).

Le théorème suivant est fondamental. Il dit que les trois propriétés des relations implicatives sont exactement ce qu'il faut pour que l'interprétation en forme de treillis distributif soit adéquate.

Théorème 1.4 (théorème fondamental des relations implicatives, [START_REF] Cederquist | Entailment relations and distributive lattices[END_REF], Lorenzen 1951). Soit un ensemble S avec une relation implicative ⊢ S sur P fe (S). On considère le treillis distributif T défini par générateurs et relations comme suit : les générateurs sont les éléments de S et les relations sont les

A ⊢ T B chaque fois que A ⊢ S B. Alors, pour tous A, B dans P fe (S), on a A ⊢ T B =⇒ A ⊢ S B.
En mathématiques classiques un idéal premier p d'un treillis distributif T = 1 est un idéal dont le complémentaire v est un filtre (qui est alors un filtre premier). On a alors T/(p = 0, v = 1) ≃ 2. Il revient au même de se donner un idéal premier de T ou un morphisme de treillis distributifs T → 2.

Théorème 1.5 (dimension d'un treillis distributif, Coquand et Lombardi 2003[START_REF] Lombardi | Dimension de Krull, Nullstellensätze et évaluation dynamique[END_REF], Lombardi et Quitté 2021, chapitre XIII). En mathématiques classiques, pour un treillis distributif non trivial et pour n 0, les propriétés suivantes sont équivalentes.

1. Le treillis est de dimension n, c'est-à-dire par définition la longueur de toute chaine d'idéaux premiers est n.

Pour tout

x ∈ T le treillis quotient T/(x = 0, I x = 0), où I x = { y ; x ∧ y = 0 }, est de dimension n -1 6 .
3. Pour toute suite (x 0 , . . . , x n ) dans T il existe une suite complémentaire (y 0 , . . . , y n ) au sens suivant

1 ⊢ y n , x n y n , x n ⊢ y n-1 , x n-1 . . . . . . . . . y 1 , x 1 ⊢ y 0 , x 0 y 0 , x 0 ⊢ 0              (4)
6. Un treillis est dit de dimension -1 s'il est trivial, i.e. réduit à un point, cela initialise la récurrence dans le point 2. On vérifie facilement qu'un trillis est zéro-dimensionnel, c'est-à-dire de dimension 0 si, et seulement si, c'est une algèbre de Boole.

Par exemple, pour n = 2 les inégalités dans le point 3 correspondent au dessin suivant dans T.

1

✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ x 2 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ y 2 q q q q q q q • • x 1 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼
q q q q q q q q y 1 q q q q q q q q ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼

• • x 0 q q q q q q q q y 0 ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ 0 ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐
Définition et remarque importantes. Les points 2 et 3 sont équivalents en mathématiques constructives et servent de définition pour la dimension de T, notée Kdim(T) et appelée dimension de Krull du treillis distributif. Notez cependant que d'un point de vue constructif on a seulement défini clairement la phrase Kdim(T) n. Pour établir Kdim(T) = n il serait nécessaire de démontrer aussi ¬(Kdim(T) n + 1). Heureusement, la plupart des théorèmes en mathématiques classiques fonctionnent avec une hypothèse du type Kdim(T) n. On a en outre le résultat constructif suivant, qui simplifie l'utilisation du point 3.

Lemme 1.6. Soit S une partie d'un treillis distributif T qui engendre T en tant que treillis distributif. En mathématiques constructives, pour n 0, les propriétés suivantes sont équivalentes.

1. Pour toute suite (x 0 , . . . , x n ) dans T il existe une suite complémentaire (y 0 , . . . , y n ) dans T.

2. Pour toute suite (x 0 , . . . , x n ) dans S il existe une suite complémentaire (y 0 , . . . , y n ) dans T.

Dans les deux paragraphes qui terminent cette section, nous expliquons comment les spectres des treillis distributifs conduisent à des espaces spectraux en algèbre abstraite. La dualité entre treillis distributifs et espaces spectraux a été établie par Stone (1937). Hochster (1969) a introduit la terminologie d'espace spectral et a popularisé leur utilisation. Mais il ne cite pas Stone 1937 et il n'indique pas le lien entre les espaces spectraux et les treillis distributifs.

Dimension de Krull d'un anneau commutatif

Nous rappelons tout d'abord l'idée principale de l'approche constructive du spectre d'un anneau commutatif développée par [START_REF] Joyal | Spectral spaces and distributive lattices[END_REF][START_REF] Joyal | Les théorèmes de Chevalley-Tarski et remarques sur l'algèbre constructive[END_REF].

Si a est un idéal de R, nous notons D R (a) (ou D(a) si le contexte est clair) le nilradical de l'idéal a :

D R (a) = R √ a = { x ∈ R ; ∃m ∈ N x m ∈ a } . ( 5
D R (a 1 ) ∧ D R (a 2 ) = D R (a 1 a 2 ) et D R (a 1 ) ∨ D R (a 2 ) = D R (a 1 + a 2 ).
Le treillis de Zariski de R est un treillis distributif et

D R (x 1 , . . . , x n ) = x 1 ∨ • • • ∨ x n .
les éléments x forment système générateur (stable par ∧) de Zar(R).

Si est un monoïde multiplicatif dans R engendré par U = {u 1 , . . . , u m } et si a = a 1 , . . . , a n est un idéal de type fini nous avons les équivalences i∈{1,...,m}

u i Zar(R) j∈{1,...,n} a j ⇐⇒ u∈{1,...,m} u i ∈ R √ a ⇐⇒ M ∩ a = ∅ (6)
cela décrit complètement le treillis distributif Zar(R). En effet la première formule dans (6) définit une relation implicative sur R qui donne une autre description Zar(R).

Nous avons aussi la caractérisation suivante (voir [START_REF] Cederquist | Entailment relations and distributive lattices[END_REF], Coquand et Lombardi 2003).

Proposition 1.7 (définition à la Joyal du spectre d'un anneau commutatif). Le treillis distributif Zar(R) est (à isomorphisme unique près) le treillis engendré par les symboles D R (a) pour a ∈ R soumis aux relations suivantes :

D R (0 R ) = 0, D R (1 R ) = 1, D R (x + y) D R (x) ∨ D R (y), D R (xy) = D R (x) ∧ D R (y).
La construction R → Zar(R) donne un foncteur de la catégorie des anneaux commutatifs vers celle des treillis distributifs. Via ce foncteur la projection

R → R/D R (0 R ) donne un isomorphisme Zar(R) → Zar(R/D R (0 R )). Nous avons Zar(R) = 1 si, et seu- lement si, 1 R = 0 R .
En mathématiques classiques on a une démonstration simple du fait que la dimension du treillis distributif Zar(R) est la dimension de Krull de l'anneau R.

Le treillis de Zariski d'un anneau est l'exemple paradigmatique d'un treillis distributif engendré par une structure algébrique dynamique. Nous expliquons la méthode générale dans le paragraphe qui suit.

Structures algébriques dynamiques

Références : Coste, Lombardi, et Roy 2001, Lombardi 1998, 2006, 2020[START_REF] Bezem | Automating coherent logic[END_REF], Coquand 2005. Les structures algébriques dynamiques (du premier ordre) sont explicitement nommées dans Lombardi (1998Lombardi ( , 2006)). Dans Coste, Lombardi, et Roy 2001 elles sont implicites, mais décrites sous la forme de leurs présentations. Elles sont également implicites dans [START_REF] Lombardi | Dimension de Krull, Nullstellensätze et évaluation dynamique[END_REF], et, last but not least, dans Della Dora, Dicrescenzo, et Duval 1985, D5, qui L'espace spectral dual est appelé le spectre de Zariski de la structure algébrique dynamique D, ou peut aussi lui attribuer un nom particulier.

Enfin la dimension de Krull de D est par définition égale à Kdim(Zar(D)). La définition de Vdim(R) dans le paragraphe suivant est donnée selon ce schéma.

Trois définitions constructives de la dimension valuative

Clôture quasi intègre minimale d'un anneau réduit

Nous rappelons ici quelques résultats essentiels donné dans Lombardi et Quitté 2015. Si le contexte a ∈ R est clair, nous notons a ⊥ l'idéal annulateur de l'élément a dans R.

Nous utilisons aussi la notation a ⊥ pour l'annulateur d'un idéal a.

Lemme 2.1. Soit R un anneau réduit et a ∈ R. On définit

R {a} def = R a ⊥ × R (a ⊥ ) ⊥
et l'on note ψ a : R → R {a} l'homomorphisme canonique.

1. ψ a (a) ⊥ est engendré par l'idempotent (0, 1), donc ψ a (a) ⊥ = (1, 0) ⊥ .

2. ψ a est injectif (on peut identifier R à un sous-anneau de R {a} ). Remarque. Le cas où ab = 0 est typique : quand on le rencontre, on voudrait bien scinder l'anneau en composantes où les choses sont claires . La construction précédente donne alors les trois composantes On note R red = R/ R 0 l'anneau réduit engendré par R.

R (ab ⊥ ) ⊥ , R (a ⊥ b) ⊥ et R (a ⊥ b ⊥ ) ⊥ .
Théorème et définition 2.4 (clôture quasi intègre minimale). Soit R un anneau réduit. On peut définir un anneau R min comme limite inductive filtrante en itérant la construction de base qui consiste à remplacer E (l'anneau en cours , qui contient R) par

E {a} def = a ⊥ × E (a ⊥ ) ⊥ = E/Ann E (a) × E/Ann E (Ann E (a))
lorsque a parcourt R.

1. Cet anneau R min est quasi intègre, il contient R et il est entier sur R.

Pour tout

x ∈ R min , x ⊥ ∩ R est un idéal annulateur dans R.
Cet anneau R min est appelé la clôture quasi intègre minimale de R. Lorsque R n'est pas nécessairement réduit, on prendra R min def = (R red ) min .

On note P n l'ensemble des parties finies de {1, . . . , n}. Voici une description de chaque anneau obtenu à un étage fini de la construction de R min .

Lemme 2.5. Soit R un anneau réduit et (a) = (a 1 , . . . , a n ) une suite de n éléments de R. Pour I ∈ P n , on note a I l'idéal

a I = i∈I a i ⊥ j / ∈I a j ⊥ = a i , i ∈ I ⊥ j / ∈I a j ⊥ .
Alors R min contient l'anneau suivant, produit de 2 n anneaux quotients de R (certains éventuellement nuls) :

R {a} = I∈Pn R/a I .
On note B(R) l'algèbre de Boole des idempotents de l'anneau R.

Lemme 2.6.

1. Soit R un anneau quasi intègre. (a) R min = R. (b) R[X] est quasi intègre, et B(R) = B(R[X]).
2. Pour tout anneau R on a un isomorphisme canonique

R min [X 1 , . . . , X n ] ≃ (R[X 1 , . . . , X n ]) min .
Notre suggestion est que la bonne généralisation de la notion du corps de fractions d'un anneau R n'est pas l'anneau Frac R mais l'anneau zéro-dimensionnel réduit Frac R min . Pour n = 0, -1, on a vdim(R) = n ⇔ Kdim(R) = n. On note que, comme pour la dimension de Krull, on n'a pas vraiment défini vdim R comme un élément de N ∪ {∞} : seule la propriété vdim R n est bien définie, constructivement, pour tout entier n -1.

Première approche constructive de la dimension valuative : vdim

Théorème 2.8 (Lombardi et Quitté 2015, Theorem XIII-8.19). Les équivalences suivantes sont valides.

1. Si n 1 et k -1, alors vdim R k ⇐⇒ vdim R[X 1 , . . . , X n ] n + k. (8)
Si R est non trivial et vdim R < ∞, cela signifie intuitivement que l'on a une égalité vdim R[X 1 , . . . , X n ] = n + vdim R. La structure algébrique dynamique Val (R, K) peut être décrite comme la théorie dynamique construite sur la signature

Si n

0, alors vdim R n ⇐⇒ Kdim R[X 1 , . . . , X n ] 2n. (9
(• = 0, Vr(•) ; 0, 1, • + •, -•, • × •, (a) a∈K )
dans laquelle les éléments de K sont des constantes de la théorie 10 . Tout d'abord il y a les axiomes des corps discrets non triviaux sur le langage des anneaux commutatifs.

• ⊢ 0 = 0

• x = 0, y = 0 ⊢ x + y = 0 • 1 = 0 ⊢ ⊥ • x = 0 ⊢ xy = 0 • ⊢ x = 0 ou ∃y xy = 1
Ensuite on ajoute le diagramme de K :

• ⊢ 0 K = 0 • ⊢ 1 K = 1 • ⊢ a + b = c (si a + b = K c) • ⊢ ab = c (si ab = K c)
Enfin il y a les axiomes décrivant les propriétés du prédicat Vr(x) qui signifie que x appartient à l'anneau de valuation supposé du corps K.

• ⊢ Vr(a) (si a ∈ R)

• Vr(x), Vr(y) ⊢ Vr(x + y) est toujours satisfaite si l'un des y j est nul ; et si l'un des x i est nul, elle est équivalente à la même règle où l'on a supprimé le Vr(x i ) correspondant à la gauche du ⊢. On constate les mêmes faits pour le Valuativstellensatz exprimé sous la forme [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF] : si l'un des y j est nul on prend Q = 0 ; si l'un des x i est nul, il n'intervient pas dans [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF]. Ainsi le Valuativstellensatz sous la forme [START_REF]Nous utilisons k comme petit anneau pour nous référer à l'intuition donnée dans la situation fréquente où k est un corps discret. Bibliographie Marc Bezem et Thierry Coquand : Automating coherent logic[END_REF] est toujours valable, ce qui évite d'avoir à raisonner cas par cas.

Le treillis Val R peut donc être caractérisé comme le treillis distributif engendré par la relation implicative ⊢ Val R sur K définie par l'équivalence

x 1 , . . . , x n ⊢ Val R y 1 , . . . , y m def ⇐⇒ ∃p 1 , . . . , p n 0 ∃Q ∈ R[X, Y ] y p 1 1 • • • y pm m = Q(x 1 , . . . , x n , y 1 , . . . , y m ) (12)
où tous les monômes de Q ont un degré en Y strictement inférieur à (p 1 , . . . , p m ).

Pour rendre les calculs à venir plus lisibles, nous introduisons le prédicat

V ′ (x) def ⇐⇒ ∃u(ux = 1, Vr(u)).
En d'autres termes, nous ajoutons un prédicat V ′ (x) dans la signature avec les deux axiomes

• ux = 1, Vr(u) ⊢ V ′ (x) • V ′ (x) ⊢ ∃u (ux = 1, Vr(u))
La nouvelle théorie est une extension conservative de la précédente. En outre on a les règles valides suivantes qui permettent de retrouver Vr à partir de

V ′ • ⊢ Vr(0) • ux = 1, V ′ (u) ⊢ Vr(x) • Vr(x) ⊢ x = 0 ou ∃u (ux = 1, V ′ (u))
On peut lire V ′ (x) comme Vr(1/x) en considérant que Vr(1/0) ⊢ ⊥ (effondrement de la théorie). Le prédicat V ′ (x) signifie que l'élément x de K n'est pas un élément résiduellement nul de V. Ce prédicat satisfait notamment les axiomes suivants dans la théorie dynamique considérée :

• ⊢ V ′ (a) (si a ∈ R × ) • V ′ (x + y) ⊢ V ′ (x) ou V ′ (y) • V ′ (x), V ′ (y) ⊢ V ′ (xy) • V ′ (0) ⊢ ⊥ • xy = 1 ⊢ V ′ (x) ou V ′ (y)
Le Valuativstellensatz devient, cette fois-ci pour des x i et y j ∈ K sans restriction x j P j (x, y) . . .

• V ′ (y 1 ), . . . , V ′ (y n ) ⊢ V ′ (x 1 ) ou . . . ou V ′ (x m ) ⇐⇒ 1 ∈ x 1 , . . . , x m R[x 1 , . . . , x m , y -1 1 , . . . ,
avec les multiexposants en Y dans les P j tous (p 1 , . . . , p n ). Si l'un des y i est nul, l'égalité est automatiquement satisfaite car on peut prendre les P j nuls.

Ce prédicat V ′ est le prédicat Nrn dans l'article Lombardi 2000 qui donne un Valuativstellensatz très général. Remarque 2.9. On peut introduire le treillis Val ′ R associé au prédicat V ′ . On peut démontrer alors que Val ′ R est isomorphe au treillis opposé à Val R. Cela tient à ce que x → x -1 est une bijection de K × sur lui-même. Dans cet article, nous utilisons seulement le fait que les caractérisations ( 11) et (13) sont équivalentes.

Nous introduirons plus loin le treillis valuatif d'un anneau arbitraire.

Troisième approche : ordre monomiaux rationnels gradués, dimv On note < lex l'ordre monomial sur Z n correspondant à l'ordre lexicographique.

Un ordre monomial rationnel gradué < M sur Z n ou, de manière équivalente, sur les monômes de R[X ±1 1 , . . . , X ±1 1 ] est défini au moyen d'une matrice M ∈ Mat n (N) inversible dans Mat n (Q) avec les coefficients de la première ligne tous > 0, de la manière suivante : R on a un polynôme P ∈ R[X 0 , . . . , X n ] qui annule (x 0 , . . . , x n ) et dont le plus petit coefficient pour l'ordre lexicographique est égal à 1. Par exemple Kdim R 1 si, et seulement si, pour tous x 0 , x 1 ∈ R on peut trouver une égalité 0 = x e 0 0 (x e 1 1 (1 + c 1 x 1 ) + c 0 x 0 ) : ici les c i sont des éléments de R ou tout aussi bien des éléments de R[x 0 , x 1 ].

Dans Kemper et Viet Trung 2014, les auteurs ont montré, en mathématiques classiques, que pour un anneau noethérien, on peut caractériser la dimension de Krull de la même manière en utilisant un ordre monomial arbitraire.

Dans Kemper et Yengui 2020, les auteurs ont montré, en mathématiques classiques, que pour un anneau arbitraire, on peut caractériser la dimension valuative de la même manière à condition d'utiliser un ordre monomial rationnel gradué à la place de l'ordre lexicographique.

Autrement dit, nous pouvons les paraphraser avec la définition suivante.

Définition 2.10. Nous disons que dimv R n si, lorsqu'on considère un ordre monomial rationnel gradué < M , on a pour tous x 0 , . . . , x n ∈ R un polynôme P ∈ R[X 0 , . . . , X n ] nul en (x 0 , . . . , x n ) dont le plus petit coefficient pour l'ordre < M est égal à 1.

Le résultat dans

(dimv B d, dimv C d) ⇒ dimv(B × C) d.
Voyons l'implication réciproque. On considère x 0 , . . . , x d ∈ R. On a tout d'abord un polynôme P 1 (X 0 , . . . , X d ) ∈ R[X] de coefficient minimum égal à c 1 = 1 + y 1 et tel que P 1 (x 0 , . . . , x d ) = z 1 avec y 1 , z 1 ∈ a ⊥ . On a par ailleurs un polynôme P 2 (X) de coefficient minimum c 2 = 1 + y 2 et tel que P 2 (x) = z 2 , avec y 2 , z 2 ∈ (a ⊥ ) ⊥ . On a alors On utilise le fait que Kdim R[x 0 , . . . , x n ] n. On a un polynôme P ∈ R[X 0 , . . . , X n ] de plus petit coefficient 1 (pour l'ordre monomial lexicographique avec X n > X n-1 > • • • > X 0 ) qui s'annule en (x 0 , . . . , x n ). Soit X qn n • • • X q 0 0 le plus petit monôme de P . En divisant P (x 0 , . . . , x n ) par x qn n • • • x q 0 0 , on obtient une égalité 1 + x 0 f 0 (x 0 ) + x 1 f 1 (x 1 , x ± 0 ) + . . . + x n f n (x n , x ± n-1 , . . . , x ± 0 ) = 0,

où f 0 ∈ R[X 0 ], f 1 ∈ R[X 1 , X ± 0 ], . . . , f n ∈ R[X n , X ± n-1 , .
. . , X ± 0 ]. Pour certains r 0 , . . . , r n ∈ N, on a :

1 + x 0 f 0 (x 0 ) + x r 0 0 x 1 g 1 (x 1 , x -1 0 ) + • • • + x r n-3
n-3 x n-2 g n-2 (x n-2 , x -1 n-3 , . . . , x -1 0 ) +x r n-2

n-2 x n-1 g n-1 (x n-1 , x -1 n-2 , . . . , x -1 0 ) + xn x r n-1 n-1

g n (x n , x n-1 , x -1 n-2 , . . . x -1 0 ) • • • = 0, où g 1 ∈ R[X 1 , X -1 0 ], . . . , g n-1 ∈ R[X n-1 , X -1 n-2 , .
. . , X r 0 -1], g n ∈ R[X n , X n-1 , X -1 n-2 , . . . , X -1 0 ]. On pose y 0 = 1+x 0 f 0 (x 0 ) x r 0 0 , y 1 = y 0 +x 1 g 1 (x 1 ,x -1 0 ) x Il suffit alors de prendre u 0 = V ′ (y 0 ),

u 1 = V ′ (y 1 ) ∧ V ′ (x 0 ), u 2 = V ′ (y 2 ) ∧ V ′ (x 1 ) ∧ V ′ (x 0 ), . . . , u n-2 = V ′ (y n-2 ) ∧ V ′ (x n-3 ) ∧ • • • ∧ V ′ (x 0 ), u n-1 = V ′ (y n-1 ) et u n = 0.

vdim = Vdim dans le cas général

On note que lorsque R est un anneau quasi intègre, l'anneau Frac(R) est un anneau zéro-dimensionnel réduit. Par ailleurs un corps discret est un anneau zéro-dimensionnel réduit dans lequel tout idempotent est égal à 0 ou 1.

Nous commençons alors par la remarque suivante qui découle de la machinerie constructive élémentaire n o 1. Dans la suite de ce paragraphe, nous ne donnons pas de démonstration. Nous renvoyons à l'étude générale Lombardi et Mahboubi (2023). Nous définissons une théorie dynamique val comme suit. On considère la signature

Σ val = ( • | • ; • + •, • × •, -•, 0, 1 )
Les axiomes sont les suivants.

2

  of the valuative dimension in classical mathematics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . E3 Basic constructive terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . E4 Valuation rings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . E5 Dimension of a distributive lattice . . . . . . . . . . . . . . . . . . . . . . . . . E6 Krull dimension of a commutative ring . . . . . . . . . . . . . . . . . . . . . . E8 Dynamical algebraic structures . . . . . . . . . . . . . . . . . . . . . . . . . . E9 Three constructive definitions of the valuative dimension E10 Minimal pp-closure of a reduced ring . . . . . . . . . . . . . . . . . . . . . . . E10 First constructive approach to the valuative dimension: vdim . . . . . . . . . . E11 Second approach: valuative lattice and valuative spectrum, Vdim . . . . . . . . E12 Third approach: graded monomial order, dimv . . . . . . . . . . . . . . . . . . E15 3 Constructive equivalence of the three constructive definitions E16 vdim = dimv . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . E16 vdim = Vdim in the integral case . . . . . . . . . . . . . . . . . . . . . . . . . E17 Proof of the converse inequality . . . . . . . . . . . . . . . . . . . . . . . E17 vdim = Vdim in the general case . . . . . . . . . . . . . . . . . . . . . . . . . . E22

Lemma 2 . 3 .

 23 If R ⊆ C with C a pp-ring, the smallest pp-subring of C containing R is equal to R[(e a ) a∈R ], where e a is the idempotent of C such that Ann C (a) = 1e a C . More generally, if R ⊆ B with B reduced and if any element a of R has an annihilator in B generated by an idempotent 1e a , then R[(e a ) a∈R ] is a pp-subring of B.

Definition 2 .

 2 7 (according toLombardi and Quitté 2015).

)

  Quand a = x 1 , . . . , x n , nous notons D R (a) sous la forme D R (x 1 , . . . , x n ). Si le contexte est clair nous notons aussi x pour D R (x).Par définition, le treillis de Zariski de R, noté Zar(R), est l'ensemble des D R (x 1 , . . . , x n ) avec l'inclusion pour relation d'ordre. Les bornes inférieure et supérieure sont données pas

  a été une source d'inspiration essentielle : on peut calculer de manière sûre dans la clôture algébrique d'un corps discret, même quand il n'est pas possible de construire cette clôture algébrique. Il suffit donc de considérer la clôture algébrique comme une structure algébrique dynamique à la D5 plutôt que comme une structure algébrique usuelle : l'évaluation paresseuse à la D5 fournit une sémantique constructive pour la clôture algébrique d'un corps discret. Une étude plus détaillée en cours de rédaction se trouve dans Lombardi 2022. Voir aussi Lombardi et Mahboubi 2023. Une théorie dynamique (finitaire) T = (L, A) est une version purement calculatoire, sans logique, d'une théorie cohérente. Le langage L est donné par une signature, les axiomes (éléments de A) sont des règles dynamiques. Une structure algébrique dynamique D pour une théorie dynamique T est donnée par générateurs et relations : D = (G, R), T . Si (G, R) est le diagramme positif d'une structure algébrique usuelle R on note D = T (R).Considérons une structure algébrique dynamique D = (G, R), T pour une théorie dynamique T = (L, A). Soit S un ensemble de formules atomiques closes de D. On définit la relation implicative ⊢ D,S sur S associée à D comme suit pour A i et B j ∈ S :A 1 , . . . , A n ⊢ D,S B 1 , . . . , B m def ⇐⇒ A 1 , . . . , A n ⊢ D B 1 ou . . . ou B m(7)On pourra noter Zar(D, S) le treillis distributif engendré par cette relation implicative.Intuitivement ce treillis est le treillis des valeurs de vérité des formules de S dans la structure algébrique dynamique D.Le treillis de Zariski (complet) d'une structure algébrique dynamique D est défini en prenant pour S l'ensemble Atcl(D) de toutes les formules atomiques closes de D. On le note Zar(D, T ) ou Zar(D) ou avec un nom particulier correspondant à la théorie T .

3.

  Soit b un idéal dans R {a} , alors l'idéal ψ -1 a (b ⊥ ) = b ⊥ ∩ R est un idéal annulateur dans R. 4. L'anneau R {a} est réduit.Lemme 2.2. Soit R réduit et a, b ∈ R. Alors avec les notations du lemme 2.1 les deux anneaux (R {a} ) {b} et (R {b} ) {a} sont canoniquement isomorphes.

  Dans la première a est régulier et b = 0, dans la seconde b est régulier et a = 0, et dans la troisième a = b = 0.

Lemme 2 . 3 .

 23 Si R ⊆ C avec C quasi intègre, le plus petit sous-anneau quasi intègre de Ccontenant R est égal à R[(e a ) a∈R ], où e a est l'idempotent de C tel que Ann C (a) = 1a C . Plus généralement, si R ⊆ B avec B réduit et si tout élément a de R admet un annulateur dans B engendré par un idempotent 1-e a , alors le sous-anneau R[(e a ) a∈R ] de B est quasi intègre.

Lombardi 2006 .

 2006 La troisième est basée sur la notion d'idéal bord (ou de filtre bord) et donne lieu à une définition par récurrence. L'équivalence de ces notions est pour l'essentiel démontrée dans Coquand et Lombardi 2003 et traitée très en détail dans Coquand et Lombardi 2018. Dans le cas d'un sous-anneau (intègre) R d'un corps discret K, l'article Coquand 2009 définit le treillis valuatif Val(R, K) comme le treillis distributif qui traduit les règles valides pour le prédicat Vr 8 dans la théorie dynamique Val (R, K) des anneaux de valuation du corps K qui contiennent R 9 . Enfin le treillis Val(R) est une notation abrégée de Val(R, Frac R).

(e 1

 1 , . . . , e n ) < M (f 1 , . . . , f n ) Lorsque les coefficients de la première ligne de M sont égaux à 1, l'ordre monomial < M est un ordre subordonné au degré total. L'ordre monomial < grlex gradué lexicographique est celui défini par la matrice  Dans Lombardi 2006, la dimension de Krull d'un anneau arbitraire R est caractérisée constructivement par l'équivalence entre Kdim R n et le fait que pour tous x 0 , . . . , x n ∈

y 1 y 2 = 1

 21 y 1 z 2 = z 1 y 2 = z 1 z 2 = 0.Quitte à multiplier P 1 et P 2 par des monômes convenables, on peut supposer que leurs monômes initiaux coïncident. AlorsQ 2 = P 2y 2 P 1 a pour coefficient minimum (1 + y 2 )y 2 (1 + y 1 ) = 1 et vérifie Q 2 (x) = z 2 . De même Q 1 = P 1y 1 P 2 a pour coefficient minimum (1 + y 1 )y 1 (1 + y 2 ) = 1 et vérifie Q 1 (x) = z 1 . Donc le polynôme Q 1 Q 2 nous convient. vdim = Vdim dans le cas intègre Lemme 3.4. Pour un anneau intègre R, et pour un entier n -Vdim R n ⇒ vdim R n Démonstration. L'article Coquand 2009 montre d'une part que Vdim R n ⇒ Kdim R n et d'autre part que Vdim R n ⇒ Vdim R[X] n + 1. Donc Vdim R n ⇒ Kdim R[X 1 , .. . , X n ] 2n. Dans Lombardi et Quitté 2015 il est démontré que Kdim R[X 1 , . . . , X n ] 2n ⇒ vdim R n.

r 1 1 ,

 1 . . . , y n-2 = y n-3 +x n-2 g n-2 (x n-2 ,x -1n-3 ,...,x -

  Lemme 3.5. Soit R un anneau quasi intègre. Définissons Val(R) := Val(R, Frac(R)) et Vdim(R) = Kdim(Val(R)) comme dans (10) en remplaçant K par Frac(R). Alors on obtient l'égalité vdim(R) = Vdim(R) comme dans le cas intègre.

Col val 0

 0 | 1 ⊢ ⊥ (effondrement) fav1 ⊢ 1 | -1 fav2 a | b ⊢ ac | bc fAv1 a | b, b | c ⊢ a | c fAv2 a | b, a | c ⊢ a | b + c fAV1 ⊢ a | b ou b | a fAV2 ax | bx ⊢ a | b ou 0 | x

Table des matières

 des 1 Introduction F3 Définition et propriétés caractéristiques de la dimension valuative en mathématiques classiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . F3 Terminologie constructive de base . . . . . . . . . . . . . . . . . . . . . . . . . F4 Domaines de valuation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . F5 Dimension des treillis distributifs . . . . . . . . . . . . . . . . . . . . . . . . . F6 Dimension de Krull d'un anneau commutatif . . . . . . . . . . . . . . . . . . . F8 Structures algébriques dynamiques . . . . . . . . . . . . . . . . . . . . . . . . F9 2 Trois définitions constructives de la dimension valuative F10 Clôture quasi intègre minimale d'un anneau réduit . . . . . . . . . . . . . . . F10 Première approche constructive de la dimension valuative : vdim . . . . . . . . F12 Deuxième approche : treillis valuatif et spectre valuatif, Vdim . . . . . . . . . . F12 Troisième approche : ordre monomiaux rationnels gradués, dimv . . . . . . . . F15 3 Équivalence constructive des trois définitions constructives F16 vdim = dimv . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . F16 vdim = Vdim dans le cas intègre . . . . . . . . . . . . . . . . . . . . . . . . . . F17 vdim = Vdim dans le cas général . . . . . . . . . . . . . . . . . . . . . . . . . F22Cet article est écrit dans le style des mathématiques constructives à la Bishop[START_REF] Bishop | Foundations of constructive analysis[END_REF][START_REF] Bishop | Constructive analysis[END_REF], Bridges et Richman 1987, Lombardi et Quitté 2021, Mines, Richman, et Ruitenburg 1988, Yengui 2015).On utilisera quand c'est nécessaire le vocabulaire et les notations des structures algébriques dynamiques. VoirCoste, Lombardi, et Roy 2001, Coquand et Lombardi 2006, Lombardi 2006, 2020. Nous comparons dans cet article les différentes constructives de la dimension valuative que l'on trouve dansCoquand 2009, Kemper et Yengui 2020, Lombardi et Quitté 2015, 2021, ainsi qu'une version constructive qui étend celle de Coquand 2009 au cas d'un anneau non nécessairement intègre. Le lecteur qui ne connait pas les mathématiques constructives dans le style de Bishop peut consulter les chapitres 1 et 2 de Bishop 1967, l'article Coquand et Lombardi 2006 et les recensions Myhill 1972 and Stolzenberg 1970. Quand une définition ou un théorème classiques utilisent des notions abstraites sans contenu calculatoire, nous essayons en mathématiques constructives de trouver ce que nous appelons une version constructive de cette définition ou de ce théorème. Cette version doit être équivalente en mathématiques classiques à la version classique. De plus il est nécessaire que les exemples de base usuels puissent être traités avec la version constructive. Par exemple la version constructive d'un anneau local est simplement un anneau dans lequel, lorsqu'une somme finie d'éléments est inversible, l'un des termes de la somme doit être inversible.

	1 Introduction
	Bibliographie	F24

  Enfin, dans l'articleKemper et Yengui 2020, qui fait suite à Kemper et Viet Trung 2014, une nouvelle caractérisation constructive de la dimension valuative d'un anneau commutatif est proposée, inspirée de la caractérisation constructive de la dimension de Krull donnée dans Lombardi 2006. Nous sommes donc en possession d'au trois approches possibles de la dimension valuative d'un anneau commutatif en mathématiques classiques. Celle correspondant au point 1 ci-dessus, celle correspondant aux points 3 et 4 et celle proposée par Kemper et Yengui.

	1, 3 et 4
	sont toujours équivalents.

  Une partie P d'un ensemble E est dite détachable lorsque la propriété x ∈ P est décidable pour les x ∈ E. Autrement dit, la règle suivante est satisfaite : tout élément est nul ou régulier, et qu'un anneau est un corps discret lorsque tout élément est nul ou inversible. Cela n'exclut pas l'anneau trivial. Un anneau est dit sans diviseur de zéro lorsque la règle • xy = 0 ⊢ x = 0 ou y = 0 est satisfaite. Un anneau intègre est sans diviseur de zéro. La réciproque, valable en mathématiques classiques, n'est pas assurée constructivement 1 . Certaines versions locales des notions d'anneau intègre et d'anneau sans diviseur de zéro sont discernables y compris en mathématiques classiques.

• ⊢ x ∈ P ou x / ∈ P. Pour décrire cette situation, il faut donc introduire à la fois le prédicat d'appartenance et le prédicat opposé. Nous disons qu'un anneau est intègre (ou est un domaine d'intégrité), lorsque

  • et a • est idempotent, de sorte que l'anneau est quasi intègre. Lemme 1.2 (lemme de scindage quasi intègre). Soient n éléments x 1 , . . ., x n dans un anneau quasi intègre R. Il existe un système fondamental d'idempotents orthogonaux (e j ) de cardinal 2 n tel que dans chacune des composantes R[1/e j ], chaque x i est nul ou régulier.

  Dans l'ouvrage Lombardi et Quitté 2015, les auteurs notent Vdim(R) au lieu de vdim(R). Nous préférons dans cet article, réserver Vdim(R) pour la notion définie par T. Coquand. Dans Lombardi et Quitté 2015 la définition suivante est constructive parce qu'il y a une définition constructive de la dimension de Krull. Et le théorème suivant est démontré constructivement. Donc, pour le cas d'un anneau intègre, le théorème 2.8 donne une version constructive de l'équivalence entre les points 2, 3 et 4 dans le théorème classique 1.1. Définition 2.7 (selon Lombardi et Quitté 2015). 1. Si R est un anneau quasi intègre, la dimension valuative est définie comme suit. Soit n ∈ N et K = Frac R, on dit que la dimension valuative de R est inférieure ou égale à n et l'on écrit vdim R n si pour toute suite (x 1 , . . . , x m ) dans K on a Kdim R[x 1 , . . . , x m ] n. Par convention vdim R = -1 si R est trivial. 2. Dans le cas général on définit vdim R n par vdim R min n 7 .

)

  Dans le cas où R est quasi intègre, ceci est aussi équivalent à : pour tous x 1 , . . .,x n dans Frac R, on a Kdim R[x 1 , . . . , x n ]n. Vdim R min en mathématiques classiques. C'est une manière de ramener le cas général au cas d'un anneau intègre sans utiliser d'idéaux premiers.

	Deuxième approche : treillis valuatif et spectre valuatif, Vdim
	Tout d'abord rappelons que concernant la dimension d'un treillis distributif ou de l'es-
	pace spectral dual, il y a trois approches constructives constructivement équivalentes.
	La première historiquement est celle définie par Joyal (1975), reprise dans Coquand et
	Persson 2001 et Coquand 2009. La deuxième provient de la notion de chaine potentielle

d'idéaux premiers, à la manière de ce qui est fait pour les anneaux commutatifs dans 7. Lombardi et Quitté (2015) démontrent qu'en mathématiques classiques on a l'équivalence vdim R d ⇐⇒ Vdim R d où Vdim R est définie comme dans Cahen 1990. Par suite, cela démontre que Vdim R =

  Le treillis Val(R, K) est alors le treillis distributif engendré par la relation implicative ⊢ Val,R,K sur K × définie par l'équivalence x 1 , . . . , x n ⊢ Val,R,K y 1 , . . . , y m Dans ce cadre, la dimension valuative de R, que nous noterons Vdim R, est définie comme égale à Kdim(Val(R)).Le théorème 8 de l'article Coquand 2009 donne un Valuativstellensatz sous la forme de l'équivalence suivante (pour desy i et x j ∈ K × ) • Vr(x 1 ), . . . , Vr(x n ) ⊢ Val (R,K) Vr(y 1 ) ou . . . ou Vr(y m ) 8.Vr rappelle Valuation ring . 9. Sans toutefois utiliser en tant que tel le langage des théories dynamiques. 10. Pour la théorie dynamique Val toute nue, on supprime tout ce qui concerne R et K.⇐⇒1 ∈ y -1 1 , . . . , y -1 m R[x 1 , . . . , x n , y -1 1 , . . . , y -1 m ] En chassant les dénominateurs on obtient la formulation équivalente suivantey p 1 1 • • • y pm m = Q(x 1 , . . . , x n , y 1 , . . . , y m ) . . .(11)pour un polynômeQ ∈ R[X 1 , . . . ,X n , Y 1 , . . . , Y m ] dont tous les monômes ont un degré en Y strictement inférieur à (p 1 , . . . , p m ). Que se passe-t-il si nous acceptons que certains x i ou y j soient éventuellement nuls ? Comme la règle ⊢ Vr(0) est valide, la règle • Vr(x 1 ), . . . , Vr(x n ) ⊢ Vr(y 1 ) ou . . . ou Vr(y m )

	• Vr(x), Vr(y) ⊢ Vr(xy)
	• xy = 1 ⊢ Vr(x) ou Vr(y)

def ⇐⇒ Vr(x 1 ), . . . , Vr(x n ) ⊢ Val (R,K) Vr(y 1 ) ou . . . ou Vr(y m )

(10)

Enfin on note Val(R) pour Val(R, Frac R).

  y -1 n ] qu'il faut réécrire sous la forme suivante pour éviter les 0 -1 : il existe des exposants p 1 , . . . , p m et des polynômes P j ∈ R[X, Y ] tels que

	y p 1 1 . . . , y pn n =	m j=1

  Kemper et Yengui 2020 est alors le suivant. Théorème 2.11. 1. Cette définition de dimv R n ne dépend pas de la matrice M considérée. 2. Elle équivaut en mathématiques classiques au fait que la dimension valuative de R est n. Par convention dimv R = -1 signifie que l'anneau est trivial. En fait, la démonstration du théorème 2.11 dans Kemper et Yengui 2020 est clairement constructive pour le cas d'un anneau intègre R : pour tout n On a un premier lemme qui prolonge (14) au cas quasi intègre. Démonstration. On reprend la démonstration constructive de (14) donnée dans le cas intègre et on utilise la machinerie locale-globale élémentaire n o 1. Pour étendre l'équivalence constructive (14) du cas d'un anneau intègre au cas d'un anneau arbitraire, étant donné que dans le cas général on a défini vdim R d comme signifiant vdim R min d, et vu le lemme 3.1, il nous suffit de démontrer constructivement l'équivalence dimv R d ⇐⇒ dimv R min d (16) Cela implique en particulier constructivement l'analogue de l'équivalence (9) pour dimv. Cette équivalence (16) se ramène aux deux lemmes suivants. Démonstration. La démonstration est laissée à la lectrice. Lemme 3.3. Soient R un anneau réduit et a ∈ R. Alors on a Démonstration. L'implication ⇒ est assez simple. D'une part, l'implication dimv R d ⇒ dimv(R/a) d est claire pour tout quotient R/a. Et d'autre part on voit que

	Lemme 3.2. On a toujours
		dimv R	d ⇐⇒ dimv R red	d	(17)
		dimv R	d ⇐⇒ dimv R {a}	d	(18)
				0 on a constructivement
	l'équivalence
	vdim R	n (définition 2.7.1) ⇐⇒ dimv R	n (définition 2.10).	(14)
	3 Équivalence constructive des trois définitions cons-
	tructives
	vdim = dimv
	Lemme 3.1. Pour un anneau quasi intègre R on a l'équivalence
		vdim R	d ⇐⇒ dimv R	d	(15)

In constructive mathematics, "or" has its intuitive meaning, i.e. one of the two properties is explicitly valid. From the fact that the ring is without zerodivisor, with an explicit "or", there is no constructive proof that any element is zero or regular, with an explicit "or".

In classical mathematics, elements of a ring can be seen as "functions" defined on the Zariski spectrum. Here we have two basic open sets D(s) and D(t) which cover the Zariski spectrum; on the first one a = 0, on the second one b = 0.

 3 In classical mathematics, we have a partition of the Zariski spectrum into two basic open sets D(1e a ) and D(e a ); on the first one a = 0, on the second one a is regular.

A lattice is said to be of dimension -1 if it is trivial, i.e. reduced to a point; this initialises the induction in Item 2. It is easy to check that a lattice is zero-dimensional, i.e. of dimension 0, if, and only if, it is a Boolean algebra.

= V ′ (x 0 )∨u 0 , V ′ (x 0 )∧u 0 V ′ (x 1 )∨u 1 , . . . , V ′ (x n-1 )∧u n-1 V ′ (x n )∨u n , V ′ (x n )∧u n = 0.

We use k as notation for the small ring in order to invoke the intuition provided by the frequent situation where k is a discrete field.

Nous disons qu'un idéal est premier s'il produit au quotient un anneau sans diviseur de zéro. Cela n'exclut pas l'idéal 1 . Ces conventions (adoptées dansLombardi et Quitté 2015) n'utilisent pas la négation et permettent d'éviter certains raisonnements cas par cas litigieux d'un point de vue constructif.Domaines de valuationUn domaine de valuation V est un sous-anneau d'un corps discret K satisfaisant l'axiome• xy = 1 ⊢ x ∈ V ou y ∈ V (x, y ∈ K)On dit alors que V est un anneau de valuation du corps discret K et que (K, V) est un corps valué.Un domaine de valuation est la même chose qu'un domaine de Bézout local, ou encore un anneau intègre dont le groupe de divisibilité est totalement ordonné.3. En mathématiques classiques, les éléments d'un anneau peuvent être vus comme des fonctions définies sur le spectre de Zariski. Ici nous avons deux ouverts de base D(s) et D(t) qui recouvrent le spectre de Zariski ; sur le premier a = 0, sur le second b = 0.4. En anglais, un pp-ring : les idéaux principaux sont projectifs. 5. En mathématiques classiques nous avons une partirion du spectre de Zariski en deux ouverts de base D(1e a ) et D(e a ) ; sur le premier a = 0, sur le second a est régulier.

We propose to find the u i in the form u 0 = V ′ (y 0 ), u 1 = V ′ (y 1 ) ∧ V ′ (x 0 ), u 2 = V ′ (y 2 ) ∧ V ′ (x 1 ) ∧ V ′ (x 0 ), u 3 = V ′ (y 3 ), u 4 = 0 with y 0 , y 1 , y 2 , y 3 ∈ K such that

) and (30)

) V ′ (x 4 ) ∧ u 4 = 0 (this is guaranteed by u 4 = 0).

(28) amounts to saying that 1 ∈ x 0 , y 0 in R[x 0 , y 0 ]. (29) amounts to saying that 1 ∈ x 1 , y 1 in R[y -1 0 , x -1 0 , x 1 , y 1 ]. (30) amounts to saying that

3 , y -1 3 , x 4 ]. We use the fact that Kdim R[x 0 , x 1 , x 2 , x 3 , x 4 ] 4. We have a polynomial P ∈ R[X 0 , X 1 , X 2 , X 3 , X 4 ] with trailing coefficient 1 (for the lexicographic monomial order with X 4 > X 3 > X 2 > X 1 > X 0 ) which vanishes at (x 0 , x 1 , x 2 , x 3 , x 4 ). Let X ℓ 4 X n 3 X m 2 X p 1 X q 0 be the trailing monomial of P . Dividing P (x 0 , x 1 , x 2 , x 3 , x 4 ) by x ℓ 4 x m 3 x n 2 x p 1 x q 0 , we obtain an equality Dimension valuative, points de vue constructifs Keywords : Mathématiques constructives, dimension valuative d'un anneau commutatif, algorithmes, programme de Hilbert pour l'algèbre abstraite. MSC : 13B40, 13J15, 03F65 * Université de Franche-Comté, CNRS, UMR 6623, LmB, 25000 Besançon, France. henri.lombardi@univ-fcomte.fr † Université de Franche-Comté, CNRS, UMR 6623, LmB, 25000 Besançon, France. stefan.neuwirth@univ-fcomte.fr ‡ Département de mathématiques, Faculté des sciences de Sfax, Université de Sfax, 3000 Sfax, Tunisia. ihsen.yengui@fss.rnu.tn Nous allons maintenant démontrer l'inégalité opposée.

Nous allons démontrer l'implication vdim

n =⇒ Vdim n en construisant des suites complémentaires. Pour comprendre la démonstration, nous traiterons d'abord les cas n = 2, 3, 4 : lorsque n = 2, la suite complémentaire est fabriquée avec des éléments de la forme V ′ (y), tandis que les cas n = 3 et n = 4 donnent des idées successives pour construire une suite complémentaire dans le treillis distributif engendré par ce type d'éléments. vdim 2 ⇒ Vdim 2 Supposons que l'on a x 0 , x 1 , x 2 non nuls dans le corps de fractions K de R. On cherche y 0 , y 1 , y 2 ∈ K (on sait que y 2 est nul) tels que :

provient des monômes de P autres que M dont le degré en X 2 est égal à n et le degré en X 1 est égal à m, x 1 f 1 (x 1 , x ± 0 ) provient des autres monômes de P dont le degré en X 2 est égal à n, alors que x 2 f 2 (x 2 , x ± 1 , x ± 0 ) provient des monômes de P dont le degré en X 2 est > n). Pour certains r 0 , r 1 ∈ N, on a :

). Prenons comme exemple d'effondrement :

En divisant par x 0 x 2 1 x 2 2 , on obtient une égalité

On voit que y 0 =

x 3 non nuls dans le corps de fractions K de R. On cherche u 0 , u 1 , u 2 , u 3 dans le treillis distributif engendré par les V ′ (x) qui forment une suite complémentaire de x 0 , x 1 , x 2 , x 3 (voir les inégalités (4) dans le théorème 1.5). Autrement dit :

On propose de trouver les u i sous la forme

3. On a un polynôme P ∈ R[X 0 , X 1 , X 2 , X 3 ] de plus petit coefficient 1 (pour l'ordre monomial lexicographique avec X 3 > X 2 > X 1 > X 0 ) qui s'annule en (x 0 , x 1 , x 2 , x 3 ). Soit X n 3 X m 2 X p 1 X q 0 le plus petit monôme de P . En divisant P (x 0 , x 1 , x 2 , x 3 ) par x m 3 x n 2 x p 1 x q 0 , on obtient une égalité

• x 0 f 0 (x 0 ) provient des monômes de P autres que M dont le degré en X 3 est égal à m, le degré en X 2 est égal à n et le degré en X 1 est égal à p,

• x 1 f 1 (x 1 , x ± 0 ) provient des autres monômes de P dont le degré en X 3 est égal à m et le degré en X 2 est égal à n,

1 , x ± 0 ) provient des autres monômes de P dont le degré en X 3 est égal à m,

provient des monômes de P dont le degré en X 3 est > m)

Pour certains r 0 , r 1 ∈ N, on a :

Condition ( 22) : 1 = x r 0 0 y 0x 0 f 0 (x 0 ) ∈ x 0 , y 0 dans R[x 0 , y 0 ] (même si r 0 = 0). Condition ( 23) : 25) : l'égalité ( 27) se relit comme suit

Si y 1 = 0 on divise par y 1 .

Par ailleurs on a aussi un bon résultat si y 0 = 0 ou y 1 = 0 (voir le commentaire après l'égalité ( 13)).

vdim 4 ⇒ Vdim 4 Soient x 0 , x 1 , x 2 , x 3 , x 4 non nuls dans le corps de fractions K de R. On cherche u 0 , u 1 , u 2 , u 3 , u 4 dans le treillis distributif engendré par les V ′ (x) qui forment une suite complémentaire de x 0 , x 1 , x 2 , x 3 , x 4 (voir les inégalités (4) dans le théorème 1.5). Autrement dit :

On propose de trouver les u i sous la forme

On utilise le fait que Kdim R[x 0 , x 1 , x 2 , x 3 , x 4 ] 4. On a un polynôme P ∈ R[X 0 , X 1 , X 2 , X 3 , X 4 ] de plus petit coefficient 1 (pour l'ordre monomial lexicographique avec X 4 > X 3 > X 2 > X 1 > X 0 ) qui s'annule en (x 0 , x 1 , x 2 , x 3 , x 4 ). Soit X ℓ 4 X n 3 X m 2 X p 1 X q 0 le plus petit monôme de P . En divisant P (x 0 , x 1 , x 2 , x 3 , x 4 ) par x ℓ 4 x m 3 x n 2 x p 1 x q 0 , on obtient une égalité

provient des monômes de P autres que M dont le degré en X 4 est égal à ℓ, le degré en X 3 est égal à m, le degré en X 2 est égal à n et le degré en X 1 est égal à p,

• x 1 f 1 (x 1 , x ± 0 ) provient des autres monômes de P dont le degré en X 4 est égal à ℓ, le degré en X 3 est égal à m, le degré en X 2 est égal à n,

1 , x ± 0 ) provient des autres monômes de P dont le degré en X 4 est égal à ℓ et le degré en X 3 est égal à m,

provient des monômes de P dont le degré en X 4 est > ℓ. Pour certains r 0 , r 1 , r 2 , r 3 ∈ N, on a : . Condition (28) : 1 = x r 0 0 y 0x 0 f 0 (x 0 ) ∈ x 0 , y 0 dans R[x 0 , y 0 ] (même si r 0 = 0). Condition (29) : y 0 = y 1 x r 1 1x 1 g 1 (x 1 , x -1 0 ), si y 0 = 0 on divise par y 0 et l'on obtient 1 ∈ x 1 , y 1 dans R[x 1 , y 1 , x -1 0 , y -1 0 ]. Condition (30) : y 1 = y 2 x r 2 2x 2 g 2 (x 2 , x -1 1 , x -1 0 ), si y 1 = 0 on divise par y 1 et l'on obtient 1 ∈ x 2 , y 2 dans R[y -1 1 , x -1 1 , x -1 0 , x 2 , y 2 ]. Condition (31) : l'égalité (33) se relit x 3 g 3 (x 3 , x -1 2 , x -1 1 , x -1 0 ) + y 3 g 4 (y 3 x r 3 3 , x 3 , x -1 2 , x -1 1 , x -1 0 ) = -y 2 Si y 2 = 0 on divise par y 2 et l'on obtient 1 ∈ x 3 , y 3 dans R[y -1 2 , x -1 2 , x -1 1 , x -1 0 , x 3 , y 3 ]. Condition (32) : y 3 x r 3 3 = x 4 , (et on divise par y 3 x r 3 3 si y 3 = 0). vdim n ⇒ Vdim n Soient x 0 , . . . , x n non nuls dans le corps de fractions K de R. On cherche u 0 , u 1 , . . . , u n dans le treillis distributif engendré par les V ′ (x) qui forment une suite complémentaire de x 0 , x 1 , . . . , x n . Autrement dit :