Regular sequences and weakly regular sequences

The notion of a regular sequence is fundamental in commutative algebra. Properties of regular sequences encode information about singularities of a ring and regularity of a sequence can be tested homologically. However the notion of a regular sequence is only really sensible for Noetherian local rings.

TODO: Koszul regular sequences, H_1-regular sequences, quasi-regular sequences, depth.

Tags

module, regular element, regular sequence, commutative algebra

@[reducible, inline]

abbrev Ideal.ofList {R : Type u_1} [Semiring R] (rs : List R) : Ideal R

The ideal generated by a list of elements.

@[simp]

theorem Ideal.ofList_nil {R : Type u_1} [Semiring R] : ofList [] = ⊥

@[simp]

theorem Ideal.ofList_append {R : Type u_1} [Semiring R] (rs₁ rs₂ : List R) : ofList (rs₁ ++ rs₂) = ofList rs₁ ⊔ ofList rs₂

theorem Ideal.ofList_singleton {R : Type u_1} [Semiring R] (r : R) : ofList [r] = span {r}

@[simp]

theorem Ideal.ofList_cons {R : Type u_1} [Semiring R] (r : R) (rs : List R) : ofList (r :: rs) = span {r} ⊔ ofList rs

@[simp]

theorem Ideal.map_ofList {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (rs : List R) : map f (ofList rs) = ofList (List.map (⇑f) rs)

theorem Ideal.ofList_cons_smul {R : Type u_7} [CommSemiring R] (r : R) (rs : List R) {M : Type u_8} [AddCommMonoid M] [Module R M] (N : Submodule R M) : ofList (r :: rs) • N = r • N ⊔ ofList rs • N

def Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : (M ⧸ Ideal.ofList (r :: rs) • ⊤) ≃ₗ[R] QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤

The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ r₀M) ⧸ (r₁, …, rₙ) (M ⧸ r₀M).

def Submodule.quotOfListConsSMulTopEquivQuotSMulTopOuter {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : (M ⧸ Ideal.ofList (r :: rs) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs • ⊤)

The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ (r₁, …, rₙ)) ⧸ r₀ (M ⧸ (r₁, …, rₙ)).

theorem Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (r : R) (rs : List R) (f : M →ₗ[R] M₂) : ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f ⋯ = (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f) ⋯ ∘ₗ ↑(quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)

theorem Submodule.top_eq_ofList_cons_smul_iff {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

structure RingTheory.Sequence.IsWeaklyRegular {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) : Prop

A sequence [r₁, …, rₙ] is weakly regular on M iff rᵢ is regular on M⧸(r₁, …, rᵢ₋₁)M for all 1 ≤ i ≤ n.

• regular_mod_prev (i : ℕ) (h : i < rs.length) : IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]

theorem RingTheory.Sequence.isWeaklyRegular_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) : IsWeaklyRegular M rs ↔ ∀ (i : ℕ) (h : i < rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]

theorem RingTheory.Sequence.isWeaklyRegular_iff_Fin {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) : IsWeaklyRegular M rs ↔ ∀ (i : Fin rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) rs) • ⊤) rs[i]

structure RingTheory.Sequence.IsRegular {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) extends RingTheory.Sequence.IsWeaklyRegular M rs : Prop

A weakly regular sequence rs on M is regular if also M/rsM ≠ 0.

• regular_mod_prev (i : ℕ) (h : i < rs.length) : IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]
• top_ne_smul : ⊤ ≠ Ideal.ofList rs • ⊤

theorem RingTheory.Sequence.isRegular_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) : IsRegular M rs ↔ IsWeaklyRegular M rs ∧ ⊤ ≠ Ideal.ofList rs • ⊤

theorem AddEquiv.isWeaklyRegular_congr {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] {e : M ≃+ M₂} {as : List R} {bs : List S} (h : List.Forall₂ (fun (r : R) (s : S) => ∀ (x : M), e (r • x) = s • e x) as bs) : RingTheory.Sequence.IsWeaklyRegular M as ↔ RingTheory.Sequence.IsWeaklyRegular M₂ bs

theorem LinearEquiv.isWeaklyRegular_congr' {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] M₂) (rs : List R) : RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ (List.map (⇑σ) rs)

theorem LinearEquiv.isWeaklyRegular_congr {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (rs : List R) : RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ rs

theorem AddEquiv.isRegular_congr {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] {e : M ≃+ M₂} {as : List R} {bs : List S} (h : List.Forall₂ (fun (r : R) (s : S) => ∀ (x : M), e (r • x) = s • e x) as bs) : RingTheory.Sequence.IsRegular M as ↔ RingTheory.Sequence.IsRegular M₂ bs

theorem LinearEquiv.isRegular_congr' {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] M₂) (rs : List R) : RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ (List.map (⇑σ) rs)

theorem LinearEquiv.isRegular_congr {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (rs : List R) : RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ rs

theorem RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff {R : Type u_1} (S : Type u_2) (M : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (rs : List R) : IsWeaklyRegular M (List.map (⇑(algebraMap R S)) rs) ↔ IsWeaklyRegular M rs

@[simp]

theorem RingTheory.Sequence.isWeaklyRegular_cons_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs

theorem RingTheory.Sequence.isWeaklyRegular_cons_iff' {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

@[simp]

theorem RingTheory.Sequence.isRegular_cons_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs

theorem RingTheory.Sequence.isRegular_cons_iff' {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) (rs : List R) : IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

@[simp]

theorem RingTheory.Sequence.IsWeaklyRegular.nil (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] : IsWeaklyRegular M []

theorem RingTheory.Sequence.IsWeaklyRegular.cons {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {r : R} {rs : List R} (h1 : IsSMulRegular M r) (h2 : IsWeaklyRegular (QuotSMulTop r M) rs) : IsWeaklyRegular M (r :: rs)

theorem RingTheory.Sequence.IsWeaklyRegular.cons' {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {r : R} {rs : List R} (h1 : IsSMulRegular M r) (h2 : IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) : IsWeaklyRegular M (r :: rs)

def RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → (rs : List R) → IsWeaklyRegular M rs → Sort u_7} (nil : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → motive M [] ⋯) (cons : {M : Type v} → [inst : AddCommGroup M] → [inst_1 : Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) → (h2 : IsWeaklyRegular (QuotSMulTop r M) rs) → motive (QuotSMulTop r M) rs h2 → motive M (r :: rs) ⋯) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} (h : IsWeaklyRegular M rs) : motive M rs h

Weakly regular sequences can be inductively characterized by:

• The empty sequence is weakly regular on any module.
• If r is regular on M and rs is a weakly regular sequence on M⧸rM then the sequence obtained from rs by prepending r is weakly regular on M.

This is the induction principle produced by the inductive definition above. The motive will usually be valued in Prop, but Sort* works too.

def RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [Module R M] → List R → Sort u_7} (nil : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → motive M []) (cons : {M : Type v} → [inst : AddCommGroup M] → [inst_1 : Module R M] → (r : R) → (rs : List R) → IsSMulRegular M r → IsWeaklyRegular (QuotSMulTop r M) rs → motive (QuotSMulTop r M) rs → motive M (r :: rs)) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} : IsWeaklyRegular M rs → motive M rs

A simplified version of IsWeaklyRegular.recIterModByRegular where the motive is not allowed to depend on the proof of IsWeaklyRegular.

@[irreducible]

def RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (rs : List R) → IsWeaklyRegular M rs → Sort u_7} (nil : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive R M [] ⋯) (cons : {R : Type u} → [inst : CommRing R] → {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) → (h2 : IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) → motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) h2 → motive R M (r :: rs) ⋯) {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} (h : IsWeaklyRegular M rs) : motive R M rs h

An alternate induction principle from IsWeaklyRegular.recIterModByRegular where we mod out by successive elements in both the module and the base ring. This is useful for propagating certain properties of the initial M, e.g. faithfulness or freeness, throughout the induction.

def RingTheory.Sequence.IsWeaklyRegular.ndrecWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} (nil : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive R M []) (cons : {R : Type u} → [inst : CommRing R] → {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (r : R) → (rs : List R) → IsSMulRegular M r → IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) → motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) → motive R M (r :: rs)) {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} : IsWeaklyRegular M rs → motive R M rs

A simplified version of IsWeaklyRegular.recIterModByRegularWithRing where the motive is not allowed to depend on the proof of IsWeaklyRegular.

theorem RingTheory.Sequence.isWeaklyRegular_singleton_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : IsWeaklyRegular M [r] ↔ IsSMulRegular M r

theorem RingTheory.Sequence.isWeaklyRegular_append_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs₁ rs₂ : List R) : IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂

theorem RingTheory.Sequence.isWeaklyRegular_append_iff' {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs₁ rs₂ : List R) : IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) (List.map (⇑(Ideal.Quotient.mk (Ideal.ofList rs₁))) rs₂)

theorem RingTheory.Sequence.IsRegular.nil (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] : IsRegular M []

theorem RingTheory.Sequence.IsRegular.cons {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {r : R} {rs : List R} (h1 : IsSMulRegular M r) (h2 : IsRegular (QuotSMulTop r M) rs) : IsRegular M (r :: rs)

theorem RingTheory.Sequence.IsRegular.cons' {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {r : R} {rs : List R} (h1 : IsSMulRegular M r) (h2 : IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) : IsRegular M (r :: rs)

def RingTheory.Sequence.IsRegular.recIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → (rs : List R) → IsRegular M rs → Sort u_7} (nil : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → [inst_2 : Nontrivial M] → motive M [] ⋯) (cons : {M : Type v} → [inst : AddCommGroup M] → [inst_1 : Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) → (h2 : IsRegular (QuotSMulTop r M) rs) → motive (QuotSMulTop r M) rs h2 → motive M (r :: rs) ⋯) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} (h : IsRegular M rs) : motive M rs h

Regular sequences can be inductively characterized by:

• The empty sequence is regular on any nonzero module.
• If r is regular on M and rs is a regular sequence on M⧸rM then the sequence obtained from rs by prepending r is regular on M.

This is the induction principle produced by the inductive definition above. The motive will usually be valued in Prop, but Sort* works too.

def RingTheory.Sequence.IsRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [Module R M] → List R → Sort u_7} (nil : (M : Type v) → [inst : AddCommGroup M] → [inst_1 : Module R M] → [Nontrivial M] → motive M []) (cons : {M : Type v} → [inst : AddCommGroup M] → [inst_1 : Module R M] → (r : R) → (rs : List R) → IsSMulRegular M r → IsRegular (QuotSMulTop r M) rs → motive (QuotSMulTop r M) rs → motive M (r :: rs)) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} : IsRegular M rs → motive M rs

A simplified version of IsRegular.recIterModByRegular where the motive is not allowed to depend on the proof of IsRegular.

def RingTheory.Sequence.IsRegular.recIterModByRegularWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (rs : List R) → IsRegular M rs → Sort u_7} (nil : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [inst_3 : Nontrivial M] → motive R M [] ⋯) (cons : {R : Type u} → [inst : CommRing R] → {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (r : R) → (rs : List R) → (h1 : IsSMulRegular M r) → (h2 : IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) → motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) h2 → motive R M (r :: rs) ⋯) {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} (h : IsRegular M rs) : motive R M rs h

An alternate induction principle from IsRegular.recIterModByRegular where we mod out by successive elements in both the module and the base ring. This is useful for propagating certain properties of the initial M, e.g. faithfulness or freeness, throughout the induction.

def RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} (nil : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [Nontrivial M] → motive R M []) (cons : {R : Type u} → [inst : CommRing R] → {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (r : R) → (rs : List R) → IsSMulRegular M r → IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) → motive (R ⧸ Ideal.span {r}) (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) → motive R M (r :: rs)) {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} : IsRegular M rs → motive R M rs

A simplified version of IsRegular.recIterModByRegularWithRing where the motive is not allowed to depend on the proof of IsRegular.

theorem RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {rs : List R} (h : IsRegular M rs) (N : Submodule R M) : Nontrivial (M ⧸ Ideal.ofList rs • N)

theorem RingTheory.Sequence.IsRegular.nontrivial {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {rs : List R} (h : IsRegular M rs) : Nontrivial M

theorem RingTheory.Sequence.isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] {rs : List R} (h : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : IsRegular M rs ↔ IsWeaklyRegular M rs

theorem IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Nontrivial M] [Module.Finite R M] {rs : List R} (h : ∀ r ∈ rs, r ∈ maximalIdeal R) : RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs

theorem RingTheory.Sequence.eq_nil_of_isRegular_on_artinian {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsArtinian R M] {rs : List R} : IsRegular M rs → rs = []

theorem RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_lTensor {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [Module.Flat R M₂] {rs : List R} (h : IsWeaklyRegular M rs) : IsWeaklyRegular (TensorProduct R M₂ M) rs

theorem RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_rTensor {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [Module.Flat R M₂] {rs : List R} (h : IsWeaklyRegular M rs) : IsWeaklyRegular (TensorProduct R M M₂) rs

theorem RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {M₄ : Type u_6} [CommRing R] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] {rs : List R} {f₁ : M →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M₄} (h₁₂ : Function.Exact ⇑f₁ ⇑f₂) (h₂₃ : Function.Exact ⇑f₂ ⇑f₃) (h₃ : Function.Surjective ⇑f₃) (h₄ : IsWeaklyRegular M₄ rs) : Function.Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯) ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)

theorem RingTheory.Sequence.IsWeaklyRegular.prototype_perm {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {rs : List R} (h : IsWeaklyRegular M rs) {rs' : List R} (h'' : rs.Perm rs') (h' : ∀ (a b : R) (rs' : List R), (a :: b :: rs').Subperm rs → have K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b; K = a • K → K = ⊥) : IsWeaklyRegular M rs'

theorem RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {rs rs' : List R} (h1 : IsWeaklyRegular M rs) (h2 : rs.Perm rs') (h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : IsWeaklyRegular M rs'

theorem RingTheory.Sequence.IsRegular.of_perm_of_subset_jacobson_annihilator {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {rs rs' : List R} (h1 : IsRegular M rs) (h2 : rs.Perm rs') (h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : IsRegular M rs'

theorem IsLocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [IsNoetherian R M] {rs rs' : List R} (h1 : RingTheory.Sequence.IsWeaklyRegular M rs) (h2 : rs.Perm rs') (h3 : ∀ r ∈ rs, r ∈ maximalIdeal R) : RingTheory.Sequence.IsWeaklyRegular M rs'

theorem IsLocalRing.isRegular_of_perm {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [IsNoetherian R M] {rs rs' : List R} (h1 : RingTheory.Sequence.IsRegular M rs) (h2 : rs.Perm rs') : RingTheory.Sequence.IsRegular M rs'

theorem nontrivial_quotSMulTop_of_mem_maximalIdeal {R : Type u_7} [CommRing R] [IsLocalRing R] (L : Type u_8) [AddCommGroup L] [Module R L] [Module.Finite R L] [Nontrivial L] {x : R} (mem : x ∈ IsLocalRing.maximalIdeal R) : Nontrivial (QuotSMulTop x L)

theorem RingTheory.Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal {R : Type u_7} [CommRing R] [IsLocalRing R] (L : Type u_8) [AddCommGroup L] [Module R L] [Module.Finite R L] [Nontrivial L] {rs : List R} (mem : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) (reg : IsWeaklyRegular L rs) : IsRegular L rs