Ideals of a noncommutative algebra extended from the base ring

Let A be an R-algebra, with R commutative but A not necessarily so. The image of algebraMap R A is central, and that single fact makes the extended ideal of an ideal I of R — the left ideal of A generated by its image — behave like an ideal of a commutative ring: it is two-sided, extension is multiplicative, and as an R-submodule of A it is nothing but I • (⊤ : Submodule R A).

The last identity is the point of the file. It is the passage between a two-sided ideal of a noncommutative ring and an ideal of a commutative ring acting on a module, and it is what lets commutative statements — Noetherian hypotheses, the Artin-Rees lemma, the Krull intersection theorem — say something about powers of a two-sided ideal of A. Mathlib's Ideal.smul_top_eq_map is the same identity for a commutative A, proved through Ideal.smul_restrictScalars, which is stated only there; without commutativity I • (⊤ : Submodule R A) first has to be shown stable under multiplication by A on the left before it is an ideal at all, and that is where centrality of the image of algebraMap R A is used.

The motivating example is a universal enveloping algebra U(L) over a commutative subalgebra R generated by central elements: the two-sided ideal that the central elements generate is extended from R, so the Krull intersection theorem applies to its powers.

Main results

• Ideal.smul_top_eq_restrictScalars_map: the extended ideal is I • ⊤, the identity I • (⊤ : Submodule R A) = Submodule.restrictScalars R (I.map (algebraMap R A)).
• Ideal.instIsTwoSidedMapAlgebraMap: the extended ideal is two-sided.
• Ideal.map_algebraMap_mul and Ideal.map_algebraMap_pow: extension along algebraMap R A is multiplicative, and therefore commutes with powers.
• Ideal.pow_smul_top_eq_restrictScalars_map_pow: the combination of the two, I ^ n • (⊤ : Submodule R A) = Submodule.restrictScalars R ((I.map (algebraMap R A)) ^ n), which is the statement consumed by the Krull intersection theorem.
• Ideal.span_pow_smul_top_eq_restrictScalars_span_image_pow: the same identity written through a generating set, which is the form in which the powers of a two-sided ideal generated by central elements become the action of powers of a commutative ideal.
• Ideal.mem_iInf_map_algebraMap_pow_iff: the Krull intersection theorem for an extended ideal. Over a Noetherian R with A a finite R-module, an element of every power of the extended ideal is fixed by multiplication by a scalar in I.
• Ideal.iInf_map_algebraMap_pow_eq_bot: the powers of an extended ideal meet in zero when A has no zero divisors and no scalar in I becomes 1.

References

The identity and its use are the shape in which G. Hochschild, An Addition to Ado's Theorem, Proceedings of the American Mathematical Society 17 (1966), 531-533, applies the Krull intersection theorem to the central ideal of a universal enveloping algebra.

The Krull intersection theorem itself is Mathlib's Ideal.mem_iInf_smul_pow_eq_bot_iff, stated for an ideal of a commutative ring acting on a module; it is not restated here.

@[simp]

theorem Ideal.smul_top_eq_restrictScalars_map {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal R) : I • ⊤ = Submodule.restrictScalars R (map (algebraMap R A) I)

The extension of an ideal along algebraMap R A is I • ⊤. This is Ideal.smul_top_eq_map with the commutativity of A removed: what replaces it is that the image of algebraMap R A is central.

theorem Ideal.mem_map_algebraMap_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal R) {x : A} : x ∈ map (algebraMap R A) I ↔ x ∈ I • ⊤

Membership in an extended ideal, read off the module I • ⊤.

instance Ideal.instIsTwoSidedMapAlgebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal R) : (map (algebraMap R A) I).IsTwoSided

An extended ideal is two-sided, because the image of algebraMap R A is central.

theorem Ideal.map_algebraMap_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I J : Ideal R) : map (algebraMap R A) (I * J) = map (algebraMap R A) I * map (algebraMap R A) J

Extension along algebraMap R A is multiplicative.

theorem Ideal.map_algebraMap_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal R) (n : ℕ) : map (algebraMap R A) (I ^ n) = map (algebraMap R A) I ^ n

Extension along algebraMap R A commutes with powers.

theorem Ideal.pow_smul_top_eq_restrictScalars_map_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (I : Ideal R) (n : ℕ) : I ^ n • ⊤ = Submodule.restrictScalars R (map (algebraMap R A) I ^ n)

A power of an extended ideal is I ^ n • ⊤. This is the statement that carries a commutative theorem about the ideal I ^ n of R acting on the module A over to the two-sided ideal of A generated by I.

theorem Ideal.span_pow_smul_top_eq_restrictScalars_span_image_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set R) (n : ℕ) : span s ^ n • ⊤ = Submodule.restrictScalars R (span (⇑(algebraMap R A) '' s) ^ n)

The extended-ideal power identity in generating-set form. The two-sided ideal of A generated by the image of a set s of scalars is Ideal.span R s • ⊤, and likewise for its powers. Powers of a two-sided ideal of A are therefore the action on A of powers of an ideal of the commutative ring R.

theorem Ideal.mem_iInf_map_algebraMap_pow_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsNoetherianRing R] [Module.Finite R A] (I : Ideal R) (x : A) : x ∈ ⨅ (n : ℕ), map (algebraMap R A) I ^ n ↔ ∃ r ∈ I, (algebraMap R A) r * x = x

The Krull intersection theorem for an extended ideal. If R is Noetherian and A is a finite R-module, an element of every power of the two-sided ideal of A generated by I is fixed by multiplication by some scalar in I.

theorem Ideal.iInf_map_algebraMap_pow_eq_bot {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsNoetherianRing R] [Module.Finite R A] [NoZeroDivisors A] (I : Ideal R) (h : ∀ r ∈ I, (algebraMap R A) r ≠ 1) : ⨅ (n : ℕ), map (algebraMap R A) I ^ n = ⊥

The powers of an extended ideal meet in zero when A has no zero divisors and no scalar in I becomes 1 in A. The second hypothesis is what an augmentation supplies in the intended application, where the image of every r ∈ I lies in its kernel: such an augmentation sends algebraMap R A r to 0 and 1 to 1, so the two cannot be equal.

Together with Ideal.mem_iInf_map_algebraMap_pow_iff this is the passage from the commutative Krull intersection theorem to a two-sided ideal of a noncommutative ring.