Documentation

Mathlib.RingTheory.Regular.RegularSequence

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

The ideal generated by a list of elements.

Equations
Instances For
    @[simp]
    theorem Ideal.ofList_nil {R : Type u_1} [Semiring R] :
    @[simp]
    theorem Ideal.ofList_append {R : Type u_1} [Semiring R] (rs₁ : List R) (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) :
    @[simp]
    theorem Ideal.ofList_cons {R : Type u_1} [Semiring R] (r : R) (rs : List R) :
    @[simp]
    theorem Ideal.map_ofList {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (rs : List R) :
    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) :
    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₂) :

    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.
    Instances For

      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.
      Instances For
        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₂) :
        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) :
        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]
        structure RingTheory.Sequence.IsWeaklyRegular {R : Type u_1} (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (rs : List R) :

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

        Instances For
          theorem RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {rs : List R} (self : RingTheory.Sequence.IsWeaklyRegular M rs) (i : ) (h : i < rs.length) :
          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]

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

          Instances For
            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) :
            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) :
            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) :
            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) :
            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) :
            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) :
            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 rsSort 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 h2motive 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
            Instances For
              def RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst : Module R M] → List RSort 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 rRingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rsmotive (QuotSMulTop r M) rsmotive M (r :: rs)) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} :

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

              Equations
              Instances For
                @[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 rsSort 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) h2motive 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
                Instances For
                  def RingTheory.Sequence.IsWeaklyRegular.ndrecWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst : Module R M] → List RSort 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 rRingTheory.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} :

                  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.
                  Instances For
                    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 rsSort 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 h2motive 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.
                    Instances For
                      def RingTheory.Sequence.IsRegular.ndrecIterModByRegular {R : Type u_1} [CommRing R] {motive : (M : Type v) → [inst : AddCommGroup M] → [inst : Module R M] → List RSort 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 rRingTheory.Sequence.IsRegular (QuotSMulTop r M) rsmotive (QuotSMulTop r M) rsmotive M (r :: rs)) {M : Type v} [AddCommGroup M] [Module R M] {rs : List R} :
                      RingTheory.Sequence.IsRegular M rsmotive M rs

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

                      Equations
                      Instances For
                        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 rsSort 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) h2motive 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.
                        Instances For
                          def RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRing {motive : (R : Type u) → [inst : CommRing R] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst : Module R M] → List RSort 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 rRingTheory.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 rsmotive 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.
                          Instances For
                            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 rslet K := Submodule.torsionBy R (M Ideal.ofList rs' ) b; K = a KK = ) :
                            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 rslet K := Submodule.torsionBy R (M Ideal.ofList rs' ) b; K = a KK = ) {rs₁ : List R} {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₁) :
                            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 : List R} {rs' : List R} (h1 : RingTheory.Sequence.IsWeaklyRegular M rs) (h2 : rs.Perm rs') (h3 : rrs, r (Module.annihilator R M).jacobson) :
                            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 : List R} {rs' : List R} (h1 : RingTheory.Sequence.IsRegular M rs) (h2 : rs.Perm rs') (h3 : rrs, r (Module.annihilator R M).jacobson) :
                            theorem LocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LocalRing R] [IsNoetherian R M] {rs : List R} {rs' : List R} (h1 : RingTheory.Sequence.IsWeaklyRegular M rs) (h2 : rs.Perm rs') (h3 : rrs, r LocalRing.maximalIdeal R) :
                            theorem LocalRing.isRegular_of_perm {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [LocalRing R] [IsNoetherian R M] {rs : List R} {rs' : List R} (h1 : RingTheory.Sequence.IsRegular M rs) (h2 : rs.Perm rs') :