Stabilization of the powers of an ideal

Two facts about when the powers of an ideal I become constant.

The first is general: if I ^ (n + 1) = I ^ n, then I ^ k = I ^ n for every k ≥ n. Nothing about the ring beyond Semiring is used, and no annihilator appears.

The second is the conditional stabilization criterion: if some i ∈ I is such that 1 + i annihilates I ^ n, then I ^ (n + 1) = I ^ n, and hence the powers are constant from n on. The annihilating element is a hypothesis here, and neither statement needs commutativity.

Finite generation of I, and the localization at 1 + I that produces such an i in Wedhorn's proof of Proposition 7.49(2), are deliberately outside this module: nothing below mentions a localization, and no theorem here derives the annihilator.

Main results

• Ideal.pow_eq_pow_of_pow_succ_eq_pow: I ^ (n + 1) = I ^ n propagates to all k ≥ n.
• Ideal.pow_succ_eq_pow_of_forall_mul_eq_zero: an i ∈ I whose 1 + i annihilates I ^ n gives I ^ (n + 1) = I ^ n.
• Ideal.pow_eq_pow_of_forall_mul_eq_zero: hence I ^ k = I ^ n for all k ≥ n.

References

• Wedhorn, Adic Spaces, proof of Proposition 7.49(2), where the conditional criterion is the closing step.

theorem Ideal.pow_eq_pow_of_pow_succ_eq_pow {R : Type u_1} [Semiring R] {I : Ideal R} {n : ℕ} (h : I ^ (n + 1) = I ^ n) {k : ℕ} (hk : n ≤ k) : I ^ k = I ^ n

Once the powers of an ideal repeat once, they are constant from that point on.

theorem Ideal.pow_succ_eq_pow_of_forall_mul_eq_zero {B : Type u_1} [Ring B] {I : Ideal B} {i : B} (hi : i ∈ I) {n : ℕ} (h : ∀ x ∈ I ^ n, (1 + i) * x = 0) : I ^ (n + 1) = I ^ n

If some i ∈ I is such that 1 + i annihilates I ^ n, then I ^ (n + 1) = I ^ n.

Commutativity is not needed.

theorem Ideal.pow_eq_pow_of_forall_mul_eq_zero {B : Type u_1} [Ring B] {I : Ideal B} {i : B} (hi : i ∈ I) {n : ℕ} (h : ∀ x ∈ I ^ n, (1 + i) * x = 0) {k : ℕ} (hk : n ≤ k) : I ^ k = I ^ n

Under the same hypothesis, the powers of I are constant from n on.