Module-finite quotients by ideals

Let R be a commutative ring generated as an algebra over a commutative semiring A by a finite set s, and let J = Ideal.span s be the ideal that the same set spans. Then R ⧸ J ^ n is spanned as an A-module by the images of the products of fewer than n elements of s: every element of R is an A-combination of products of elements of s, and a product of n or more of them already lies in J ^ n. That spanning set is indexed by the tuples Fin k → s with k < n, a finite type as soon as s is finite, so the quotient is a finite A-module.

Products also preserve module-finite quotients when the first factor ideal is finitely generated over R. The filtration with successive quotients I / IJ and R / I proves this over a commutative base semiring, without an invertibility or domain hypothesis.

Finiteness also transfers to a noncommutative algebra. If B is an R-algebra and J is a two-sided ideal of B containing the extension of an ideal I of R — for instance the two-sided ideal generated by the image of s — then B ⧸ J is annihilated by I, hence an algebra over R ⧸ I. When B ⧸ J is finite as an R-module, it is also finite over R ⧸ I, and module-finiteness composes:

Module.Finite R (B ⧸ J) → Module.Finite A (R ⧸ I) → Module.Finite A (B ⧸ J).

Finiteness of B over R is a sufficient condition for the quotient-finiteness hypothesis. Under that sufficient condition, combining the two gives TauCeti.finite_quotient_pow_of_algebraMap_mem: a two-sided ideal of B containing the image of a finite generating set of R has finite-module quotients by all of its powers. The motivating application is a universal enveloping algebra U(L) over a commutative subalgebra R generated by finitely many central elements of the augmentation ideal: the quotient of U(L) by any power of the two-sided ideal those elements generate is finite dimensional over the base field.

Main results

• Ideal.finite_quotient_mul: products preserve module-finite quotients when the first ideal is finitely generated over R.

• Ideal.fg_of_le_of_finite_quotient: over a noetherian base, an ideal containing a finitely generated ideal with module-finite quotient is finitely generated.

• TauCeti.span_range_prod_quotient_span_pow_eq_top: an explicit spanning set of R ⧸ Ideal.span s ^ n, the images of the products of fewer than n elements of s.

• TauCeti.finite_quotient_span_pow_of_adjoin_eq_top: R ⧸ Ideal.span s ^ n is a finite A-module when the finite set s generates R as an A-algebra, because that spanning set is then finite.

• TauCeti.finite_quotient_of_map_algebraMap_le: finiteness of R ⧸ I over A transfers to B ⧸ J when B ⧸ J is finite over R and the two-sided ideal J contains the extension of I.

• TauCeti.finite_quotient_pow_of_algebraMap_mem: the combination of the two, for the powers of a two-sided ideal containing the image of a finite generating set, when B is finite over R.

theorem TauCeti.span_range_prod_quotient_span_pow_eq_top {A : Type u_1} {R : Type u_2} [CommSemiring A] [CommRing R] [Algebra A R] {s : Set R} (htop : Algebra.adjoin A s = ⊤) (n : ℕ) : Submodule.span A (Set.range fun (f : (k : Fin n) × (Fin ↑k → ↑s)) => (Ideal.Quotient.mk (Ideal.span s ^ n)) (∏ i : Fin ↑f.fst, ↑(f.snd i))) = ⊤

A quotient by a power of the ideal spanned by a set of algebra generators is spanned by the products of fewer than that many generators. The products of n or more elements of s lie in Ideal.span s ^ n, so the images of the shorter products already span R ⧸ Ideal.span s ^ n. The spanning set is indexed by the tuples Fin k → s with k < n, which is a finite type whenever s is finite.

theorem TauCeti.finite_quotient_span_pow_of_adjoin_eq_top {A : Type u_1} {R : Type u_2} [CommSemiring A] [CommRing R] [Algebra A R] {s : Set R} (hs : s.Finite) (htop : Algebra.adjoin A s = ⊤) (n : ℕ) : Module.Finite A (R ⧸ Ideal.span s ^ n)

A quotient by a power of the ideal spanned by a finite set of algebra generators is a finite module. The spanning set of TauCeti.span_range_prod_quotient_span_pow_eq_top is indexed by a finite type when s is finite.

theorem TauCeti.finite_quotient_of_map_algebraMap_le {A : Type u_1} {R : Type u_2} {B : Type u_3} [CommSemiring A] [CommRing R] [Ring B] [Algebra A R] [Algebra A B] [Algebra R B] [IsScalarTower A R B] {I : Ideal R} {J : Ideal B} [J.IsTwoSided] [Module.Finite R (B ⧸ J)] (hIJ : Ideal.map (algebraMap R B) I ≤ J) (h : Module.Finite A (R ⧸ I)) : Module.Finite A (B ⧸ J)

Module-finiteness of a quotient passes from the commutative base to a finite quotient module. If B ⧸ J is finite over the commutative ring R of central scalars and the two-sided ideal J of B contains the extension of I, then B ⧸ J is an algebra over R ⧸ I and is finite over A whenever R ⧸ I is finite over A. In particular, the quotient-finiteness hypothesis holds when B is finite over R.

theorem TauCeti.finite_quotient_pow_of_algebraMap_mem {A : Type u_1} {R : Type u_2} {B : Type u_3} [CommSemiring A] [CommRing R] [Ring B] [Algebra A R] [Algebra A B] [Algebra R B] [IsScalarTower A R B] [Module.Finite R B] {s : Set R} (hs : s.Finite) (htop : Algebra.adjoin A s = ⊤) {J : Ideal B} [J.IsTwoSided] (hsJ : ∀ x ∈ s, (algebraMap R B) x ∈ J) (n : ℕ) : Module.Finite A (B ⧸ J ^ n)

Every power of a two-sided ideal containing a finite set of algebra generators of the central scalars has a finite-module quotient. This is the form consumed downstream: s generates the commutative ring R of central scalars as an A-algebra, B is finite over R, and the two-sided ideal J of B contains the image of s.

theorem Ideal.finite_quotient_mul {A : Type u_1} {R : Type u_2} [CommSemiring A] [CommRing R] [Algebra A R] (I J : Ideal R) [Module.Finite R ↥I] [Module.Finite A (R ⧸ I)] [Module.Finite A (R ⧸ J)] : Module.Finite A (R ⧸ I * J)

Products preserve module-finite quotients when the first factor ideal is finitely generated. This does not require that factor to be invertible.

theorem Ideal.fg_of_le_of_finite_quotient {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] [Algebra A R] [IsNoetherianRing A] {I J : Ideal R} (hJ : J.FG) (hJI : J ≤ I) [Module.Finite A (R ⧸ J)] : I.FG

Over a noetherian base ring A, an ideal I of an A-algebra R is finitely generated as soon as it contains a finitely generated ideal J such that R ⧸ J is a finite A-module: then R ⧸ J is a noetherian R-module.