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.

Equations

• Ideal.ofList rs = Ideal.span {r : R | r ∈ rs}

@[simp]

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

@[simp]

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

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

@[simp]

theorem Ideal.ofList_cons {R : Type u_1} [Semiring R] (r : R) (rs : List R) : Ideal.ofList (r :: rs) = Ideal.span {r} ⊔ Ideal.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) : Ideal.map f (Ideal.ofList rs) = Ideal.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) : Ideal.ofList (r :: rs) • N = r • N ⊔ Ideal.ofList rs • N

theorem Submodule.smul_top_le_comap_smul_top {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (I : Ideal R) (f : M →ₗ[R] M₂) : I • ⊤ ≤ Submodule.comap f (I • ⊤)

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).

Equations

• One or more equations did not get rendered due to their size.

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ₙ)).

Equations

• One or more equations did not get rendered due to their size.

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₂) : ↑(Submodule.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) ⋯ ∘ₗ ↑(Submodule.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) : RingTheory.Sequence.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) : RingTheory.Sequence.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) : RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.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) : RingTheory.Sequence.IsWeaklyRegular M (List.map (⇑(algebraMap R S)) rs) ↔ RingTheory.Sequence.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) : RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.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) : RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.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) : RingTheory.Sequence.IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.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) : RingTheory.Sequence.IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.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] : RingTheory.Sequence.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 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs) : RingTheory.Sequence.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 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) : RingTheory.Sequence.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) → RingTheory.Sequence.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 : RingTheory.Sequence.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 : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.
• RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular nil cons x_7 = nil x

def RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst : 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 → RingTheory.Sequence.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} : RingTheory.Sequence.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.

Equations

• RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular nil cons = RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular nil fun {M : Type ?u.132} [AddCommGroup M] [Module R M] => cons

@[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) → RingTheory.Sequence.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 : RingTheory.Sequence.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 : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.
• RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing nil cons x_10 = nil x✝³ x✝¹

def RingTheory.Sequence.IsWeaklyRegular.ndrecWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst : 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 → RingTheory.Sequence.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} : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.

theorem RingTheory.Sequence.isWeaklyRegular_singleton_iff {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (r : R) : RingTheory.Sequence.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) : RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔ RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧ RingTheory.Sequence.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) : RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔ RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧ RingTheory.Sequence.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] : RingTheory.Sequence.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 : RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs) : RingTheory.Sequence.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 : RingTheory.Sequence.IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)) : RingTheory.Sequence.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) → RingTheory.Sequence.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 : RingTheory.Sequence.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 : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.

def RingTheory.Sequence.IsRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst : Module R M] → List R → 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) → IsSMulRegular M r → RingTheory.Sequence.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} : RingTheory.Sequence.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.

Equations

• RingTheory.Sequence.IsRegular.ndrecIterModByRegular nil cons = RingTheory.Sequence.IsRegular.recIterModByRegular nil fun {M : Type ?u.135} [AddCommGroup M] [Module R M] => cons

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) → RingTheory.Sequence.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 : RingTheory.Sequence.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 : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.

def RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst : 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] → [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) → IsSMulRegular M r → RingTheory.Sequence.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} : RingTheory.Sequence.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.

Equations

• One or more equations did not get rendered due to their size.

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 : RingTheory.Sequence.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 : RingTheory.Sequence.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) : RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.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 ∈ IsLocalRing.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} : RingTheory.Sequence.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 : RingTheory.Sequence.IsWeaklyRegular M rs) : RingTheory.Sequence.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 : RingTheory.Sequence.IsWeaklyRegular M rs) : RingTheory.Sequence.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₄ : RingTheory.Sequence.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 : RingTheory.Sequence.IsWeaklyRegular M rs) {rs' : List R} (h'' : rs.Perm rs') (h' : ∀ (a b : R) (rs' : List R), (a :: b :: rs').Subperm rs → let K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b; K = a • K → K = ⊥) : RingTheory.Sequence.IsWeaklyRegular M rs'

theorem RingTheory.Sequence.IsWeaklyRegular.prototype_perm.aux {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {rs : List R} (h' : ∀ (a b : R) (rs' : List R), (a :: b :: rs').Subperm rs → let K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b; K = a • K → K = ⊥) {rs₁ rs₂ : List R} (rs₀ : List R) (h₁₂ : rs₁.Perm rs₂) (H₁ : (rs₀ ++ rs₁).Subperm rs) (H₃ : (rs₀ ++ rs₂).Subperm rs) (h : RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁) : RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) 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 : RingTheory.Sequence.IsWeaklyRegular M rs) (h2 : rs.Perm rs') (h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : RingTheory.Sequence.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 : RingTheory.Sequence.IsRegular M rs) (h2 : rs.Perm rs') (h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) : RingTheory.Sequence.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 ∈ IsLocalRing.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'

@[deprecated IsLocalRing.isRegular_of_perm]

theorem LocalRing.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'

Alias of IsLocalRing.isRegular_of_perm.