Documentation

Mathlib.RingTheory.Filtration

I-filtrations of modules #

This file contains the definitions and basic results around (stable) I-filtrations of modules.

Main results #

theorem Ideal.Filtration.ext {R : Type u} :
∀ {inst : CommRing R} {I : Ideal R} {M : Type u} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (x y : Ideal.Filtration I M), x.N = y.Nx = y
theorem Ideal.Filtration.ext_iff {R : Type u} :
∀ {inst : CommRing R} {I : Ideal R} {M : Type u} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (x y : Ideal.Filtration I M), x = y x.N = y.N
structure Ideal.Filtration {R : Type u} [CommRing R] (I : Ideal R) (M : Type u) [AddCommGroup M] [Module R M] :

An I-filtration on the module M is a sequence of decreasing submodules N i such that I • (N i) ≤ N (i + 1). Note that we do not require the filtration to start from .

Instances For
    theorem Ideal.Filtration.pow_smul_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (i : ) (j : ) :
    theorem Ideal.Filtration.pow_smul_le_pow_smul {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (i : ) (j : ) (k : ) :
    theorem Ideal.Filtration.antitone {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) :
    @[simp]
    theorem Ideal.trivialFiltration_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :
    def Ideal.trivialFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :

    The trivial I-filtration of N.

    Instances For
      instance Ideal.Filtration.instSupFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :

      The sup of two I.Filtrations is an I.Filtration.

      The sSup of a family of I.Filtrations is an I.Filtration.

      instance Ideal.Filtration.instInfFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :

      The inf of two I.Filtrations is an I.Filtration.

      The sInf of a family of I.Filtrations is an I.Filtration.

      @[simp]
      theorem Ideal.Filtration.sup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (F' : Ideal.Filtration I M) :
      (F F').N = F.N F'.N
      @[simp]
      theorem Ideal.Filtration.sSup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (S : Set (Ideal.Filtration I M)) :
      (sSup S).N = sSup (Ideal.Filtration.N '' S)
      @[simp]
      theorem Ideal.Filtration.inf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (F' : Ideal.Filtration I M) :
      (F F').N = F.N F'.N
      @[simp]
      theorem Ideal.Filtration.sInf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (S : Set (Ideal.Filtration I M)) :
      (sInf S).N = sInf (Ideal.Filtration.N '' S)
      @[simp]
      theorem Ideal.Filtration.top_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      @[simp]
      theorem Ideal.Filtration.bot_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      @[simp]
      theorem Ideal.Filtration.iSup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {ι : Sort u_1} (f : ιIdeal.Filtration I M) :
      (iSup f).N = ⨆ (i : ι), (f i).N
      @[simp]
      theorem Ideal.Filtration.iInf_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {ι : Sort u_1} (f : ιIdeal.Filtration I M) :
      (iInf f).N = ⨅ (i : ι), (f i).N
      def Ideal.Filtration.Stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) :

      An I filtration is stable if I • F.N n = F.N (n+1) for large enough n.

      Instances For
        @[simp]
        theorem Ideal.stableFiltration_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (i : ) :
        def Ideal.stableFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :

        The trivial stable I-filtration of N.

        Instances For
          theorem Ideal.Filtration.Stable.exists_pow_smul_eq {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) :
          n₀, ∀ (k : ), Ideal.Filtration.N F (n₀ + k) = I ^ k Ideal.Filtration.N F n₀
          theorem Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} (h : Ideal.Filtration.Stable F) :
          n₀, ∀ (n : ), n n₀Ideal.Filtration.N F n = I ^ (n - n₀) Ideal.Filtration.N F n₀
          theorem Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : Ideal.Filtration I M} :
          Ideal.Filtration.Stable F n₀, ∀ (n : ), n n₀Ideal.Filtration.N F n = I ^ (n - n₀) Ideal.Filtration.N F n₀
          def Ideal.Filtration.submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) :

          The R[IX]-submodule of M[X] associated with an I-filtration.

          Instances For
            @[simp]
            theorem Ideal.Filtration.mem_submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (f : PolynomialModule R M) :
            theorem Ideal.Filtration.submodule_eq_span_le_iff_stable_ge {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : Ideal.Filtration I M) (n₀ : ) :
            Ideal.Filtration.submodule F = Submodule.span { x // x reesAlgebra I } (⋃ (i : ) (_ : i n₀), ↑(PolynomialModule.single R i) '' ↑(Ideal.Filtration.N F i)) ∀ (n : ), n n₀I Ideal.Filtration.N F n = Ideal.Filtration.N F (n + 1)

            If the components of a filtration are finitely generated, then the filtration is stable iff its associated submodule of is finitely generated.

            theorem Ideal.exists_pow_inf_eq_pow_smul {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [Module.Finite R M] (N : Submodule R M) :
            k, ∀ (n : ), n kI ^ n N = I ^ (n - k) (I ^ k N)

            Artin-Rees lemma

            theorem Ideal.mem_iInf_smul_pow_eq_bot_iff {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [Module.Finite R M] (x : M) :
            x ⨅ (i : ), I ^ i r, r x = x
            theorem Ideal.iInf_pow_smul_eq_bot_of_localRing {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) [IsNoetherianRing R] [LocalRing R] [Module.Finite R M] (h : I ) :
            ⨅ (i : ), I ^ i =
            theorem Ideal.iInf_pow_eq_bot_of_localRing {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [LocalRing R] (h : I ) :
            ⨅ (i : ), I ^ i =

            Krull's intersection theorem for noetherian local rings.

            theorem Ideal.iInf_pow_eq_bot_of_isDomain {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R] (h : I ) :
            ⨅ (i : ), I ^ i =

            Krull's intersection theorem for noetherian domains.