Regular parameters on finite normal local algebras

Let A → B be a finite injective local homomorphism from a two-dimensional regular local ring to a normal local domain. Every pair generating the maximal ideal of A is regular on B, viewed as an A-module. Such a pair is also regular on A itself. These are the simultaneous regular parameters needed to apply a regular-sequence criterion for freeness to B.

The argument uses normality to exclude the maximal ideal of B from the associated primes of a principal quotient. Integrality and locality imply that the images of the parameters generate an ideal with maximal radical in B. No flatness assumption is made.

Main results

• TauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal: a parameter pair on the base is regular on the finite normal local algebra.
• TauCeti.IsRegularLocalRing.exists_regular_parameters_of_finite_normal: a pair generating the base maximal ideal and regular on both rings exists.

References

• The Stacks Project, Lemma 10.106.3 (00NQ), regular systems of parameters.
• The Stacks Project, Lemma 10.157.4 (031S), normal rings satisfy Serre's condition (S₂).

theorem TauCeti.IsRegularLocalRing.isRegular_pair_of_finite_normal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsRegularLocalRing A] [IsLocalRing B] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [IsLocalHom (algebraMap A B)] (hinj : Function.Injective ⇑(algebraMap A B)) (hdim : ringKrullDim A = 2) {x y : A} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal A) : RingTheory.Sequence.IsRegular B [x, y]

Over a two-dimensional regular local ring, every pair generating the maximal ideal is regular on any finite injective normal local algebra, considered as a module over the base.

theorem TauCeti.IsRegularLocalRing.exists_regular_parameters_of_finite_normal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsRegularLocalRing A] [IsLocalRing B] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [IsLocalHom (algebraMap A B)] (hinj : Function.Injective ⇑(algebraMap A B)) (hdim : ringKrullDim A = 2) : ∃ (x : A) (y : A), Ideal.span {x, y} = IsLocalRing.maximalIdeal A ∧ RingTheory.Sequence.IsRegular A [x, y] ∧ RingTheory.Sequence.IsRegular B [x, y]

A finite injective normal local algebra over a two-dimensional regular local ring admits a pair of base parameters regular on both the base and the algebra.