Some remarks about normal rings

TL;DR

This paper provides a constructive proof that polynomial rings over normal rings are normal, with applications to henselization of local rings, using explicit localizations instead of minimal primes.

Contribution

It introduces a constructive method to prove the normality of polynomial rings over normal rings, extending classical results with explicit localization techniques.

Findings

Constructive proof of normality of R[X] when R is normal

Application to henselization of local rings

Use of explicit localizations instead of minimal primes

Abstract

We give a constructive proof that $R[X]$ is normal when $R$ is normal. We apply this result to an operation needed for studying the henselization of a local ring. Our proof is based on the case where $R$ is without zero divisors, which is more involved than the case where $R$ is an integral domain. We have to use a constructive deciphering technique that replaces the use of minimal primes (in classical mathematics) by suitable explicit localizations in a suitable tree.