Regular sequences of polynomial variables

Any finite list of distinct indeterminates is a regular sequence over a nontrivial commutative ring. This is the starting regular sequence for transporting polynomial coordinates to a polynomial algebra and then along a flat extension.

The proof uses Mathlib's description of the ideal generated by a set of variables as the kernel of the substitution killing those variables.

theorem MvPolynomial.isSMulRegular_quotient_span_X_image {R : Type u_1} {σ : Type u_2} [CommRing R] (s : Set σ) {i : σ} (hi : i ∉ s) : IsSMulRegular (MvPolynomial σ R ⧸ Ideal.span (X '' s)) (X i)

A variable outside a set of variables is regular modulo the ideal they generate.

theorem MvPolynomial.isWeaklyRegular_map_X {R : Type u_1} {σ : Type u_2} [CommRing R] (l : List σ) (hl : l.Nodup) : RingTheory.Sequence.IsWeaklyRegular (MvPolynomial σ R) (List.map X l)

Distinct polynomial variables form a weakly regular sequence, without a nontriviality hypothesis on the coefficient ring.

theorem MvPolynomial.isRegular_map_X {R : Type u_1} {σ : Type u_2} [CommRing R] [Nontrivial R] (l : List σ) (hl : l.Nodup) : RingTheory.Sequence.IsRegular (MvPolynomial σ R) (List.map X l)

Any finite list of distinct polynomial variables is a regular sequence.