Regular local rings of dimension two

Let A be a regular local ring of dimension two and let x, y generate its maximal ideal. Then A ⧸ (x) is a discrete valuation ring with uniformizer the image of y, so a finite module on which x, y is a weakly regular sequence is free: modulo x it is a torsion-free finite module over a principal ideal domain, and freeness lifts along the regular element x.

Applied to a prime 𝔭 ≠ 𝔪, this shows that 𝔭 is a free A-module, hence principal. Every nonzero prime ideal therefore contains a prime element (for 𝔪, a regular parameter), and Kaplansky's criterion shows that A is a unique factorization domain. In particular A is integrally closed. This is the dimension-two case of the theorem of Auslander and Buchsbaum that regular local rings are factorial; it supplies the normality of the base needed for going down from finite algebras over a two-dimensional regular local ring.

The same criterion shows that the dual N* = Hom(N, A) of a finite module is free: a regular sequence x, y on A stays weakly regular on Hom(N, A). Hence over a regular local ring of dimension at most two every finite reflexive module is free. This is the step of the structure theory of finitely generated modules over such rings, for instance over the Iwasawa algebra O⟦T⟧, that handles the torsion-free part.

Main results

• TauCeti.IsRegularLocalRing.free_of_isWeaklyRegular: a finite module on which a pair generating the maximal ideal is weakly regular is free.
• TauCeti.IsRegularLocalRing.isPrincipal_of_ne_maximalIdeal: a prime ideal other than the maximal ideal is principal.
• TauCeti.IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two: a regular local ring of dimension at most two is a unique factorization domain.
• TauCeti.IsRegularLocalRing.free_dual: over a regular local ring of dimension at most two, the dual of a finite module is free.
• TauCeti.IsRegularLocalRing.free_of_isReflexive: over a regular local ring of dimension at most two, a finite reflexive module is free.

References

• The Stacks Project, Lemma 10.106.5, lifting freeness along a regular element.
• H. Matsumura, Commutative Ring Theory, Theorem 20.3 (Auslander–Buchsbaum): regular local rings are unique factorization domains.
• Kaplansky's criterion, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime in Mathlib.
• The Stacks Project, Lemma 15.24.10, the depth of a module of homomorphisms.

theorem TauCeti.IsRegularLocalRing.spanFinrank_maximalIdeal_eq_two {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) : Submodule.spanFinrank (IsLocalRing.maximalIdeal A) = 2

The maximal ideal of a two-dimensional regular local ring needs exactly two generators.

theorem TauCeti.IsRegularLocalRing.exists_span_pair_eq_maximalIdeal {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) : ∃ (x : A) (y : A), Ideal.span {x, y} = IsLocalRing.maximalIdeal A

The maximal ideal of a two-dimensional regular local ring is generated by two elements.

theorem TauCeti.IsRegularLocalRing.free_of_isWeaklyRegular {A : Type u_1} [CommRing A] [IsRegularLocalRing A] {M : Type u_2} [AddCommGroup M] [Module A M] [Module.Finite A M] {x y : A} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal A) (hM : RingTheory.Sequence.IsWeaklyRegular M [x, y]) : Module.Free A M

Over a regular local ring, a finite module is free as soon as some pair generating the maximal ideal is a weakly regular sequence on it. The ring then has dimension two, unless the module is zero.

theorem TauCeti.IsRegularLocalRing.isPrincipal_of_ne_maximalIdeal {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) {p : Ideal A} [p.IsPrime] (hp : p ≠ IsLocalRing.maximalIdeal A) : Submodule.IsPrincipal p

In a regular local ring of dimension at most two, every prime ideal other than the maximal ideal is principal. In dimension two such a prime is a free module, since a pair generating the maximal ideal is regular on it.

theorem TauCeti.IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) : UniqueFactorizationMonoid A

A regular local ring of dimension at most two is a unique factorization domain. In dimension at most one it is a field or a discrete valuation ring. In dimension two every nonzero prime ideal contains a prime element, a regular parameter for the maximal ideal and a generator for every other prime, so Kaplansky's criterion applies.

theorem TauCeti.IsRegularLocalRing.free_dual {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) (N : Type u_2) [AddCommGroup N] [Module A N] [Module.Finite A N] : Module.Free A (Module.Dual A N)

Over a regular local ring of dimension at most two, the dual Hom(N, A) of a finite module N is free. In dimension two a regular system of parameters x, y is a regular sequence on A, so it is weakly regular on Hom(N, A); in smaller dimension A is a principal ideal domain.

theorem TauCeti.IsRegularLocalRing.free_of_isReflexive {A : Type u_1} [CommRing A] [IsRegularLocalRing A] (hdim : ringKrullDim A ≤ 2) (N : Type u_2) [AddCommGroup N] [Module A N] [Module.Finite A N] [Module.IsReflexive A N] : Module.Free A N

Reflexive modules are free in dimension two. Over a regular local ring of dimension at most two, a finite reflexive module is free, being isomorphic to the dual of its dual.