Regular local rings of dimension at most two are factorial

A regular local ring of dimension at most two is a unique factorization domain. In dimension zero and one it is a field or a discrete valuation ring. In dimension two, the quotient R ⧸ (x) by a parameter x ∈ 𝔪 \ 𝔪² is a discrete valuation ring, and the following elementary argument shows that every prime 𝔮 of R not containing x is principal. Since 𝔮 is prime and x ∉ 𝔮, the kernel 𝔮 ∩ (x) of 𝔮 → R ⧸ (x) is x 𝔮. The image of 𝔮 is principal in the principal ideal ring R ⧸ (x), generated by the image of some f ∈ 𝔮, so 𝔮 = (f) + x 𝔮 and Nakayama's lemma gives 𝔮 = (f) (Ideal.IsPrime.isPrincipal_of_isPrincipal_map_quotient_span_singleton). Every nonzero prime then contains a prime element: x if it contains x, and its generator otherwise. Kaplansky's criterion concludes (UniqueFactorizationMonoid.of_isPrincipalIdealRing_quotient_span_singleton).

This is the dimension-two case of the Auslander–Buchsbaum theorem that every regular local ring is factorial, and it is the case needed for regular surfaces, such as a regular model of a curve over a discrete valuation ring. There, every height-one prime of a local ring is principal, so that the integral curves on the surface, in particular the irreducible components of the special fibre, are effective Cartier divisors.

Main results

• TauCeti.IsRegularLocalRing.uniqueFactorizationMonoid: a regular local ring of Krull dimension at most two is a unique factorization domain.

References

• The Stacks Project, Tag 0AG0, the general statement that a regular local ring is a unique factorization domain, proved there through the Auslander–Buchsbaum formula.
• H. Matsumura, Commutative Ring Theory, Section 20, for the general statement, and I. Kaplansky, Commutative Rings, for the criterion by prime elements in prime ideals, which is Mathlib's UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime.

theorem TauCeti.IsRegularLocalRing.uniqueFactorizationMonoid {R : Type u_1} [CommRing R] [IsRegularLocalRing R] (h : ringKrullDim R ≤ 2) : UniqueFactorizationMonoid R

A regular local ring of dimension at most two is a unique factorization domain.