Documentation

TauCeti.RingTheory.Regular.RegularSequence

Constructing regular sequences #

This file produces regular sequences on a module M from local information.

If a, b is a weakly M-regular sequence, then bʲ is regular on M ⧸ aⁿ M and aʲ is regular on M ⧸ bⁿ M for all n and j. For M = R, an element of the total ring of fractions of R which lies in R after multiplication by a power of a, and also after multiplication by a power of b, already lies in R. When a and b are non-zero-divisors, this says that R_a and R_b intersect in R inside the total ring of fractions.

If f₁, …, f_r is weakly M-regular, every relation ∑ fᵢ mᵢ = 0 with mᵢ ∈ M has all its coefficients in (f₁, …, f_r) M. Dividing the last element out first, f_r m_r ∈ (f₁, …, f_{r-1}) M forces m_r = ∑_{i<r} fᵢ nᵢ, and the relation ∑_{i<r} fᵢ (mᵢ + f_r nᵢ) = 0 among the first r - 1 elements finishes the induction.

Let M be a finite module over a Noetherian ring R and I an ideal of R. By prime avoidance, I contains an M-regular element exactly when I lies in no associated prime of M. Iterating, if depth M_p ≥ n at every prime p ⊇ I, then I contains a weakly M-regular sequence of length n: an associated prime containing I would give a localization of depth zero, and dividing by a regular element of I lowers each of these local depths by exactly one.

The second statement passes from depth at the points of the closed subset V(I) of Spec R to a regular sequence on M itself. This is how a depth condition at the points of V(I) is used to extend sections of M~ across V(I) (Stacks, Lemma 31.5.11 (0E9I)).

Main results #

References #

source
@[simp]
theorem Ideal.ofList_ofFn {R : Type u_1} [Semiring R] {n : ℕ} (f : Fin n → R) :
ofList (List.ofFn f) = span (Set.range f)

The ideal generated by the entries of List.ofFn f is the span of the range of f.

source
theorem Ideal.ofList_eq_span_range_getElem {R : Type u_1} [Semiring R] (rs : List R) :
ofList rs = span (Set.range fun (i : Fin rs.length) => rs[i])

The ideal generated by a list is the span of its entries, indexed by position.

source
theorem RingTheory.Sequence.IsWeaklyRegular.of_subsingleton {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] (rs : List R) :
IsWeaklyRegular M rs

Every finite sequence is weakly regular on a module with at most one element.

source
theorem TauCeti.isSMulRegular_quotSMulTop_iff {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {a b : R} :
IsSMulRegular (QuotSMulTop a M) b ↔ ∀ (m c : M), a • c = b • m → m ∈ a • ⊤

An element b is regular on M ⧸ a M exactly when a c = b m forces m ∈ a M.

source
theorem RingTheory.Sequence.IsWeaklyRegular.isSMulRegular_quotSMulTop_pow {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {a b : R} (h : IsWeaklyRegular M [a, b]) (n j : ℕ) :
IsSMulRegular (QuotSMulTop (a ^ n) M) (b ^ j)

If a, b is a weakly M-regular sequence, then bʲ is regular on M ⧸ aⁿ M.

source
theorem RingTheory.Sequence.IsWeaklyRegular.isSMulRegular_quotSMulTop_pow_swap {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {a b : R} (h : IsWeaklyRegular M [a, b]) (n j : ℕ) :
IsSMulRegular (QuotSMulTop (b ^ n) M) (a ^ j)

If a, b is a weakly M-regular sequence, then aʲ is regular on M ⧸ bⁿ M. Here b need not be regular on M.

source
theorem RingTheory.Sequence.IsWeaklyRegular.mem_range_algebraMap_of_pow_mul_mem {R : Type u} [CommRing R] {K : Type v} [CommRing K] [Algebra R K] [IsFractionRing R K] {a b : R} (h : IsWeaklyRegular R [a, b]) {z : K} {n j : ℕ} (ha : (algebraMap R K) (a ^ n) * z ∈ (algebraMap R K).range) (hb : (algebraMap R K) (b ^ j) * z ∈ (algebraMap R K).range) :
z ∈ (algebraMap R K).range

If a, b is a weakly R-regular sequence, an element of the total ring of fractions of R which lies in R after multiplication by a power of a, and also after multiplication by a power of b, already lies in R. When b is also a non-zero-divisor, this says that the localizations R_a and R_b intersect in R inside the total ring of fractions.

source
theorem RingTheory.Sequence.IsWeaklyRegular.mem_ofList_smul_top_of_sum_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} (h : IsWeaklyRegular M rs) {m : Fin rs.length → M} (hm : ∑ i : Fin rs.length, rs[i] • m i = 0) (i : Fin rs.length) :
m i ∈ Ideal.ofList rs • ⊤

Relations among a weakly regular sequence have coefficients in the ideal it generates. If rs is weakly regular on M and ∑ rsᵢ • mᵢ = 0, then every mᵢ lies in (rs) M.

source
theorem RingTheory.Sequence.IsWeaklyRegular.isLeftRegular_mk_ofList {R : Type u} [CommRing R] {rs : List R} {r : R} (h : IsWeaklyRegular R (rs ++ [r])) :
IsLeftRegular ((Ideal.Quotient.mk (Ideal.ofList rs)) r)

The last element of a weakly R-regular sequence is a left-regular element of the quotient ring by the ideal generated by the preceding elements.

source
theorem IsLocalRing.exists_isSMulRegular_of_depth_ne_zero {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [IsLocalRing R] [Small.{v, u} R] (h : depth ↧M ≠ 0) :
∃ a ∈ maximalIdeal R, IsSMulRegular M a

Over a Noetherian local ring, a finite module of nonzero depth has a regular element in the maximal ideal.

source
theorem TauCeti.exists_isWeaklyRegular_of_le_depth_localizedModule {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) (n : ℕ) (h : ∀ (p : Ideal R) [inst : p.IsPrime], I ≤ p → ↑n ≤ IsLocalRing.depth ↧(LocalizedModule p.primeCompl M)) :
∃ (rs : List R), rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsWeaklyRegular M rs

Let M be a finite module over a Noetherian ring and I an ideal. If depth M_p ≥ n for every prime p containing I, then I contains a weakly M-regular sequence of length n.