Algebra and Analysis Seminar: Krull's Lemma as Proof Transformation

Peter Schuster (University of Leeds)

The Kuratowski-Zorn Lemma is utterly effective within many an indirect proof in which a minimal or maximal counterexample helps to quickly obtain the desired contradiction. A typical example is the Gelfand proof of Wiener's 1/f Theorem, where a maximal ideal of Fourier series is chosen as to contain the supposed non-unit f. Its transfinite character notwithstanding, this proof method has proved to possess computational content, at least when it rather is about prime ideals. In fact, Krull's Lemma has turned out to correspond to an algorithm that transforms any given proof for integral domains, of a definite Horn clause in the language of rings, into a proof for reduced rings. An extensive generalisation of this transformation only requires very light universal algebra, and has the Artin-Schreier Theorem from real algebra as its perhaps most unexpected instance.

Joint work with Davide Rinaldi, Leeds.