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_iff {R : Type u} :
∀ {inst : CommRing R} {I : Ideal R} {M : Type u} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (x y : I.Filtration M), x = y x.N = y.N
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 : I.Filtration M), x.N = y.Nx = y
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.mono {R : Type u} [CommRing R] {I : Ideal R} {M : Type u} [AddCommGroup M] [Module R M] (self : I.Filtration M) (i : ) :
    self.N (i + 1) self.N i
    theorem Ideal.Filtration.smul_le {R : Type u} [CommRing R] {I : Ideal R} {M : Type u} [AddCommGroup M] [Module R M] (self : I.Filtration M) (i : ) :
    I self.N i self.N (i + 1)
    theorem Ideal.Filtration.pow_smul_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) (i : ) (j : ) :
    I ^ i F.N j F.N (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 : I.Filtration M) (i : ) (j : ) (k : ) :
    I ^ (i + k) F.N j I ^ k F.N (i + j)
    theorem Ideal.Filtration.antitone {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration 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) :
    ∀ (x : ), (I.trivialFiltration N).N x = N
    def Ideal.trivialFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :
    I.Filtration M

    The trivial I-filtration of N.

    Equations
    • I.trivialFiltration N = { N := fun (x : ) => N, mono := , smul_le := }
    Instances For
      instance Ideal.Filtration.instSup {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      Sup (I.Filtration M)

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

      Equations
      • Ideal.Filtration.instSup = { sup := fun (F F' : I.Filtration M) => { N := F.N F'.N, mono := , smul_le := } }
      instance Ideal.Filtration.instSupSet {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      SupSet (I.Filtration M)

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

      Equations
      • Ideal.Filtration.instSupSet = { sSup := fun (S : Set (I.Filtration M)) => { N := sSup (Ideal.Filtration.N '' S), mono := , smul_le := } }
      instance Ideal.Filtration.instInf {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      Inf (I.Filtration M)

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

      Equations
      • Ideal.Filtration.instInf = { inf := fun (F F' : I.Filtration M) => { N := F.N F'.N, mono := , smul_le := } }
      instance Ideal.Filtration.instInfSet {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      InfSet (I.Filtration M)

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

      Equations
      • Ideal.Filtration.instInfSet = { sInf := fun (S : Set (I.Filtration M)) => { N := sInf (Ideal.Filtration.N '' S), mono := , smul_le := } }
      instance Ideal.Filtration.instTop {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      Top (I.Filtration M)
      Equations
      • Ideal.Filtration.instTop = { top := I.trivialFiltration }
      instance Ideal.Filtration.instBot {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      Bot (I.Filtration M)
      Equations
      • Ideal.Filtration.instBot = { bot := I.trivialFiltration }
      @[simp]
      theorem Ideal.Filtration.sup_N {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) (F' : I.Filtration 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 (I.Filtration 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 : I.Filtration M) (F' : I.Filtration 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 (I.Filtration 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 : ιI.Filtration 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 : ιI.Filtration M) :
      (iInf f).N = ⨅ (i : ι), (f i).N
      instance Ideal.Filtration.instCompleteLattice {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      CompleteLattice (I.Filtration M)
      Equations
      instance Ideal.Filtration.instInhabited {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} :
      Inhabited (I.Filtration M)
      Equations
      • Ideal.Filtration.instInhabited = { default := }
      def Ideal.Filtration.Stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) :

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

      Equations
      • F.Stable = ∃ (n₀ : ), nn₀, I F.N n = F.N (n + 1)
      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 : ) :
        (I.stableFiltration N).N i = I ^ i N
        def Ideal.stableFiltration {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :
        I.Filtration M

        The trivial stable I-filtration of N.

        Equations
        • I.stableFiltration N = { N := fun (i : ) => I ^ i N, mono := , smul_le := }
        Instances For
          theorem Ideal.stableFiltration_stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) :
          (I.stableFiltration N).Stable
          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 : I.Filtration M} (h : F.Stable) :
          ∃ (n₀ : ), ∀ (k : ), F.N (n₀ + k) = I ^ k F.N 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 : I.Filtration M} (h : F.Stable) :
          ∃ (n₀ : ), nn₀, F.N n = I ^ (n - n₀) F.N 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 : I.Filtration M} :
          F.Stable ∃ (n₀ : ), nn₀, F.N n = I ^ (n - n₀) F.N n₀
          theorem Ideal.Filtration.Stable.exists_forall_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : I.Filtration M} {F' : I.Filtration M} (h : F.Stable) (e : F.N 0 F'.N 0) :
          ∃ (n₀ : ), ∀ (n : ), F.N (n + n₀) F'.N n
          theorem Ideal.Filtration.Stable.bounded_difference {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : I.Filtration M} {F' : I.Filtration M} (h : F.Stable) (h' : F'.Stable) (e : F.N 0 = F'.N 0) :
          ∃ (n₀ : ), ∀ (n : ), F.N (n + n₀) F'.N n F'.N (n + n₀) F.N n
          def Ideal.Filtration.submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) :

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

          Equations
          • F.submodule = { carrier := {f : PolynomialModule R M | ∀ (i : ), f i F.N i}, add_mem' := , zero_mem' := , smul_mem' := }
          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 : I.Filtration M) (f : PolynomialModule R M) :
            f F.submodule ∀ (i : ), f i F.N i
            theorem Ideal.Filtration.inf_submodule {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) (F' : I.Filtration M) :
            (F F').submodule = F.submodule F'.submodule
            def Ideal.Filtration.submoduleInfHom {R : Type u} (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            InfHom (I.Filtration M) (Submodule ((reesAlgebra I)) (PolynomialModule R M))

            Ideal.Filtration.submodule as an InfHom.

            Equations
            Instances For
              theorem Ideal.Filtration.submodule_closure_single {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) :
              AddSubmonoid.closure (⋃ (i : ), (PolynomialModule.single R i) '' (F.N i)) = F.submodule.toAddSubmonoid
              theorem Ideal.Filtration.submodule_span_single {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) :
              Submodule.span ((reesAlgebra I)) (⋃ (i : ), (PolynomialModule.single R i) '' (F.N i)) = F.submodule
              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 : I.Filtration M) (n₀ : ) :
              F.submodule = Submodule.span ((reesAlgebra I)) (⋃ (i : ), ⋃ (_ : i n₀), (PolynomialModule.single R i) '' (F.N i)) nn₀, I F.N n = F.N (n + 1)
              theorem Ideal.Filtration.submodule_fg_iff_stable {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} (F : I.Filtration M) (hF' : ∀ (i : ), (F.N i).FG) :
              F.submodule.FG F.Stable

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

              theorem Ideal.Filtration.Stable.of_le {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : I.Filtration M} [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable) {F' : I.Filtration M} (hf : F' F) :
              F'.Stable
              theorem Ideal.Filtration.Stable.inter_right {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : I.Filtration M} (F' : I.Filtration M) [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable) :
              (F F').Stable
              theorem Ideal.Filtration.Stable.inter_left {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F : I.Filtration M} (F' : I.Filtration M) [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable) :
              (F' F).Stable
              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 : ), nk, I ^ 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 : I), 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.

              Also see Ideal.isIdempotentElem_iff_eq_bot_or_top for integral domains.

              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.