Documentation

TauCeti.Algebra.WordFiltration.Noetherian

A word-filtered algebra whose associated graded is Noetherian is Noetherian #

Let f : M →ₗ[R] A be a linear family of generators of an algebra A and let TauCeti.Algebra.wordFiltration f be the filtration it generates. This file proves the filtered-to-graded transfer of the Noetherian property: if the associated graded ring TauCeti.Algebra.wordFiltration.AssociatedGraded f is left Noetherian and the filtration is exhaustive, then A is left Noetherian. The specialization to the PBW filtration of a universal enveloping algebra is TauCeti/Algebra/Lie/UniversalEnveloping/PBW/Noetherian/Basic.lean; it is the companion of the domain transfer in TauCeti/Algebra/WordFiltration/Domain.lean, which has the same shape and the same two inputs.

The mechanism is the symbol ideal. A left ideal I ⊆ A meets the filtration in I ⊓ F n, and the classes of those elements in the graded piece F n / F_{n-1} form an R-submodule symbolSubmodule f I n of that piece, the degree-n symbols of I. Multiplying a symbol of I on the left by any homogeneous class again gives a symbol of I, because I is a left ideal, so the ideal symbolIdeal f I of the associated graded generated by all the symbols has no homogeneous component beyond them: an element of the associated graded lies in symbolIdeal f I exactly when each of its homogeneous components is a symbol of I (mem_symbolIdeal_iff).

Symbols therefore pin a left ideal inside a larger one: if I ≤ J are left ideals and the symbol ideal of J is contained in that of I, the two coincide (eq_of_le_of_symbolIdeal_le). Nothing is claimed here about left ideals that are not nested. The proof is an induction on the filtration degree: if a lies in the larger ideal and in F n, its degree-n symbol is a symbol of the smaller ideal I, so a differs from an element of I by an element of F_{n-1}, and that difference is handled by the inductive hypothesis; exhaustivity starts the induction for every a. An ascending chain of left ideals of A then has an ascending chain of symbol ideals, which stabilizes because the associated graded is Noetherian, and every step past that point is a nested pair with the same symbol ideal, hence an equality.

Only the left ideals of A are considered, matching Mathlib's IsNoetherianRing; the right-handed statement is the same theorem read in the opposite algebra, whose word filtration is generated by the same family.

Main definitions #

Main results #

References #

source
def TauCeti.Algebra.wordFiltration.symbolSubmodule {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (I : Ideal A) (n : ℕ) :
Submodule R (GradedPiece f n)

The degree-n symbols of a left ideal I of a word-filtered algebra: the classes in the degree-n graded piece of the elements of I of filtration degree at most n.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Algebra.wordFiltration.mk_mem_symbolSubmodule {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I : Ideal A} {n : ℕ} (a : ↥(wordFiltration f n)) (ha : ↑a ∈ I) :
    Submodule.Quotient.mk a ∈ symbolSubmodule f I n

    The class of an element of a left ideal is a symbol of that ideal.

    source
    theorem TauCeti.Algebra.wordFiltration.exists_mem_of_mem_symbolSubmodule {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I : Ideal A} {n : ℕ} {z : GradedPiece f n} (hz : z ∈ symbolSubmodule f I n) :
    ∃ (a : ↥(wordFiltration f n)), ↑a ∈ I ∧ Submodule.Quotient.mk a = z

    Every symbol of a left ideal is the class of an element of that ideal.

    source
    theorem TauCeti.Algebra.wordFiltration.gradedMul_mem_symbolSubmodule {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (I : Ideal A) (i j : ℕ) (x : GradedPiece f i) {y : GradedPiece f j} (hy : y ∈ symbolSubmodule f I j) :
    ((gradedMul f i j) x) y ∈ symbolSubmodule f I (i + j)

    The symbols of a left ideal absorb homogeneous multiplication on the left: a homogeneous class of degree i times a degree-j symbol of I is a degree-i + j symbol of I.

    source
    noncomputable def TauCeti.Algebra.wordFiltration.symbolIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (I : Ideal A) :
    Ideal (AssociatedGraded f)

    The symbol ideal of a left ideal I: the ideal of the associated graded generated by the homogeneous symbols of I, the degree-n classes of the elements of I of filtration degree at most n.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.Algebra.wordFiltration.of_mk_mem_symbolIdeal {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I : Ideal A} {n : ℕ} (a : ↥(wordFiltration f n)) (ha : ↑a ∈ I) :
      (DirectSum.of (GradedPiece f) n) (Submodule.Quotient.mk a) ∈ symbolIdeal f I

      The homogeneous symbol of an element of a left ideal lies in the symbol ideal. Not a simp lemma: TauCeti.Algebra.wordFiltration.mem_symbolIdeal_iff already rewrites its left-hand side.

      source
      theorem TauCeti.Algebra.wordFiltration.symbolIdeal_mono {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I J : Ideal A} (h : I ≤ J) :
      symbolIdeal f I ≤ symbolIdeal f J

      Passing to the symbol ideal is monotone.

      source
      @[simp]
      theorem TauCeti.Algebra.wordFiltration.mem_symbolIdeal_iff {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I : Ideal A} {z : AssociatedGraded f} :
      z ∈ symbolIdeal f I ↔ ∀ (n : ℕ), z n ∈ symbolSubmodule f I n

      Membership in the symbol ideal is degreewise: an element of the associated graded lies in the symbol ideal of I exactly when every one of its homogeneous components is a symbol of I. In particular the symbol ideal adds nothing to the symbols in any single degree.

      source
      theorem TauCeti.Algebra.wordFiltration.symbolSubmodule_le_of_symbolIdeal_le {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {I J : Ideal A} (h : symbolIdeal f J ≤ symbolIdeal f I) (n : ℕ) :
      symbolSubmodule f J n ≤ symbolSubmodule f I n

      Comparing symbol ideals compares symbols degreewise.

      source
      theorem TauCeti.Algebra.wordFiltration.eq_of_le_of_symbolIdeal_le {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (hex : ∀ (a : A), ∃ (k : ℕ), a ∈ wordFiltration f k) {I J : Ideal A} (hIJ : I ≤ J) (h : symbolIdeal f J ≤ symbolIdeal f I) :
      I = J

      Nested left ideals with the same symbols are equal: if I ≤ J are left ideals of an exhaustively word-filtered algebra and the symbol ideal of J is contained in that of I, then I = J. Only that one inclusion of symbol ideals is hypothesized, the other being the monotonicity TauCeti.Algebra.wordFiltration.symbolIdeal_mono; the statement says nothing about left ideals that are not nested.

      source
      theorem TauCeti.Algebra.wordFiltration.isNoetherianRing_of_isNoetherianRing_associatedGraded {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) [IsNoetherianRing (AssociatedGraded f)] (hex : ∀ (a : A), ∃ (k : ℕ), a ∈ wordFiltration f k) :
      IsNoetherianRing A

      The filtered-to-graded transfer of the Noetherian property: an exhaustively word-filtered algebra whose associated graded ring is left Noetherian is itself left Noetherian.