Antwerp, March 2025

Constructivization techniques for commutative algebra
-- an incomplete syllabus --

(many techniques are related and many techniques can be made more accessible by
modal language for the toposophic multiverse)

(we mention here only few examples, each technique has found countless
applications, and only list very few references, more can then be found in the
linked articles)


## 1. Nontrivial uses of trivial rings

Make judicious use of rings like A[f⁻¹] or A/(f), and when determining that
these are zero rings, make the most out of it.

Examples.
- Injective matrices with more columns than rows
- Surjective matrices with more rows than columns

References.
- Fred Richman. Nontrivial uses of trivial rings


## 2. Generic objects / formal topology

For an ordinary prime ideal 𝔭 in classical mathematics, for every ring element x
there is a definite truth value (0 or 1) as to whether x is contained in 𝔭.

We can generalize this notion to L-valued prime ideals (or prime filters, or
maximal ideals, or subrings, etc.), where L is a bounded lattice different from {0,1}.

Classical proofs about prime ideals can often be rewritten to refer to L-valued
prime ideals.

Examples.
- Krull's theorem ("if a ring element is contained in every prime ideal, then
  it is nilpotent") can be constructivized (and trivialized) as "if a ring
  element is contained in every L-valued prime ideal, for every L, then it is
  nilpotent")
- Noetherian condition (see below)

References.
- Ingo Blechschmidt. Generalized spaces for constructive algebra.
  (and many references therein)
- Thierry Coquand. Space of valuations.


## 3. Localization at the generic prime filter

Given a ring A and an L-valued multiplicatively closed subset S (for instance
the generic prime filter), we can form the localization of A at S. The resulting
object will not be a ring in the usual sense, but a "ring on L" (a
contravariant functor from L to the category of rings).

The localization of A at its generic prime filter is called A~ and is
remarkable in that on the one hand, it is close to A:
1. For every x ∈ A, if x is zero in A~, then it is zero in A.
2. Assuming the Boolean Prime Ideal Axiom (implied by the axiom of choice),
   for every geometric implication X it holds that:
   A~ validates X if and only if every stalk of A (at ordinary prime ideals)
   validates X.

On the other, it has better ring-theoretic properties than A: If A is reduced,
then ...
3. A~ is a field: ∀x∈A~. ¬(x inv.) ⇒ x = 0
4. A~ has stable equality: ∀x,y ∈ A~. ¬¬(x = y) ⇒ x = y
5. A~ is anonymously Noetherian: Every ideal of A~ is not not finitely generated

Examples.
- Grothendieck's Generic Freeness Lemma
- McCoy's theorem

References.
- Ingo Blechschmidt. Generalized spaces for constructive algebra.
  (and many references therein)


## 4. Positive notions for advanced learners

The classical notions of Noetherian rings ("every ascending sequence of ideals
stabilizes") and of well quasiorders ("every sequence is good") are not
positive in that they do not start with an existential quantifier but with a
universal quantifier.

As a rule of thumb, positive statements are "better", they disclose information
which can never be taken away again. (Even if we pass to an extension of the
base mathematical universe.)

After a long line of research by several authors, positive reformulations of
Noetherian rings and well quasiorders have become available. These
reformulations finally allowed us to give constructive proofs of several key
theorems (Hilbert's basis theorem; Dickson's lemma, Higman's lemma, Kruskal's
tree theorem).

These reformulations also feel quite alien. They can be cast in more familiar
language by using modal operators.

References.
- Thierry Coquand, Henrik Persson. Gröbner bases in type theory.
- Thierry Coquand. Notions invariant by change of bases.
- Ingo Blechschmidt, Gabriele Buriola, Peter Schuster. A constructive picture
  of Noetherian conditions and well quasi-orders.
- Ingo Blechschmidt. The topos-theoretic multiverse: a modal approach for computation.


## 5. Double negation translation

Constructively, we do not have A ∨ ¬A, but we do have ¬¬(A ∨ ¬A).

As a consequence, every classical proof (making use of LEM) can be transformed
to a constructive proof (not using LEM), at the price of introducing double
negations in front of every disjunction, existential quantifier and atomic
relation.

This translation is possible even if negation is not defined as usual as ¬P :≡
(P ⇒ ⊥), but as (P ⇒ X) for some fixed statement X. In this case we can use
the (with the usual definition invalid) tautology ¬¬X ⇒ X to escape the double
negation monad.

Barr's metatheorem covers a wide range of cases: If a geometric implication
admits a classical proof from some set of axioms, then it also admits a
constructive proof (from the same set of axioms).

The double negation translation cannot be used to constructivize usages of the
axiom of choice.

Examples.
- (ℕ,≤) is a well quasiorder in the sense that every function f : ℕ → ℕ is good
  in that there are indices i < j such that f(i) ≤ f(j).
- Och's theorem in field theory
- McCoy's theorem

References.
- See course notes and references therein at rt.quasicoherent.io


## 6. Entailment relations

References.
- Davide Rinaldi, Peter Schuster, Daniel Wessel. Eliminating disjunctions by
  disjunction elimination.
  (and references therein)


## 7. Dialectica interpretation


## 8. Dynamical methods

In the dynamical approach, we replace some objects which are hard to obtain
(splitting fields, maximal ideals, ...) by approximations, where we are
prepared to refine those to better approximations when evidence of their
inadequacy surfaces.

For instance, given a monic polynomial f ∈ K[X] over a field K,
to construct a field extension Ω of K containing a zero of f, we start out
with the definition Ω := K[X]/(f). (This ring is only a field in case that f is
irreducible, which me might not be able to check or not check efficiently.)

Given an element [g] ∈ Ω, we can then distinguish three cases:
- If gcd(f,g) = 1, then [g] is invertible in Ω.
- If gcd(f,g) = f, then [g] is zero in Ω.
- If 1 < deg(gcd(f,g)) < deg(f), then [g] is neither invertible nor zero in Ω.
  In this case we have found, in d := gcd(f,g), a nontrivial factor of f,
  and we restart the computation with Ω' := K[X]/(d) in place of Ω.

This is related to double negation as follows: For every monic polynomial f ∈ K[X]
over a field K, it is not not the case that there exists a ring extension K' of K
containing a zero of f such that

    ∀x ∈ K'. ¬¬(x = 0 ∨ x inv.).

Examples.
- Suslin's lemma

References.
- Henri Lombardi, Claude Quitté. Commutative Algebra: Constructive Methods.
- Ingo Blechschmidt, Peter Schuster. Reifying dynamical algebra: maximal ideals, constructively.
  (and especially the references therein)