Localising at 1 + I

For an ideal I of a semiring B, the set 1 + I is a submonoid of B. If B is commutative, I is finitely generated, and its image in a localisation at 1 + I lies in every prime there, then a single element of 1 + I annihilates a power of I.

Over a commutative ring that annihilator makes the powers of I constant, which is the form Wedhorn's argument actually uses and the one stated last below: its conclusion mentions neither the localisation nor the submonoid.

Only these implications are proved here, and only under I.FG; the converses are not stated.

The nilpotence step is not about localisation at all and lives in TauCeti.RingTheory.Ideal.Nilpotent as Ideal.exists_pow_map_eq_bot. Localisation enters here, to turn "the image of I ^ n is zero" into an annihilator lying in 1 + I.

Main results

• Ideal.oneAdd: 1 + I as a submonoid of an arbitrary semiring B. Membership is recorded existentially, as ∃ a ∈ I, x = 1 + a, so that no subtraction is needed.
• Ideal.exists_mem_oneAdd_forall_mul_eq_zero: if I is finitely generated and its image in a localisation C at 1 + I is contained in every prime of C, there is a single s ∈ 1 + I with s * x = 0 for every x ∈ I ^ n.
• Ideal.exists_forall_pow_eq_pow: over a commutative ring, the same hypotheses make the powers of I constant from some point on.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 7.49(2). The construction here follows the argument of that proposition's proof, which localises at 1 + I in exactly this way; the statements below are stated for their own sake and do not mention Spa.

def Ideal.oneAdd {B : Type u_1} [Semiring B] (I : Ideal B) : Submonoid B

1 + I is a submonoid. Closure is the identity (1 + a)(1 + b) = 1 + (a + b + a * b), which needs no commutativity: a * b lies in I because I is closed under left multiplication.

Equations

• I.oneAdd = { carrier := {x : B | ∃ a ∈ I, x = 1 + a}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem Ideal.mem_oneAdd {B : Type u_1} [Semiring B] (I : Ideal B) {x : B} : x ∈ I.oneAdd ↔ ∃ a ∈ I, x = 1 + a

theorem Ideal.exists_mem_oneAdd_forall_mul_eq_zero {B : Type u_1} {C : Type u_2} [CommSemiring B] [CommSemiring C] [Algebra B C] {I : Ideal B} [IsLocalization I.oneAdd C] (hfg : I.FG) (hprime : ∀ (P : Ideal C), P.IsPrime → map (algebraMap B C) I ≤ P) : ∃ (n : ℕ), ∃ s ∈ I.oneAdd, ∀ x ∈ I ^ n, s * x = 0

A single element of 1 + I annihilates a power of I. Let I be a finitely generated ideal of B whose image in a localisation C at 1 + I is contained in every prime of C. Then there are n : ℕ and s ∈ 1 + I with s * x = 0 for every x ∈ I ^ n — one s serving the whole of I ^ n, not one per element.

theorem Ideal.exists_forall_pow_eq_pow {B : Type u_1} {C : Type u_2} [CommRing B] [CommSemiring C] [Algebra B C] {I : Ideal B} [IsLocalization I.oneAdd C] (hfg : I.FG) (hprime : ∀ (P : Ideal C), P.IsPrime → map (algebraMap B C) I ≤ P) : ∃ (n : ℕ), ∀ (k : ℕ), n ≤ k → I ^ k = I ^ n

The powers of I are eventually constant. If I is a finitely generated ideal of a commutative ring B whose image in a localisation C at 1 + I lies in every prime of C, then I ^ k = I ^ n for some n and all k ≥ n.

This is the closing step of Wedhorn's proof of Proposition 7.49(2), and the reason the localisation is introduced there at all. Note what the conclusion does not mention: neither C nor 1 + I survives it, so a caller who has discharged the hypothesis is left with a statement purely about I.