Colon ideals by powers of a nonzero element

The ideal-theoretic identities behind the transform of a marked ideal (I, m) under a blow-up, π_*^{-1}(I, m) = (𝒪(mF) · π^* I, m) [Kol07, Definition 60], computed at a stalk where the exceptional divisor F is cut out by a single element u: dividing by 𝒪(mF) is taking the colon (A : u^m). In a commutative ring R:

• Ideal.colon_coe_span_singleton_pow: the colon by the ideal (u)^k is the colon by {u^k};
• Ideal.colon_singleton_pow_mono: (A : u^s) ⊆ (A : u^t) for s ≤ t;
• Ideal.span_pow_mul_colon_of_le: exact division, A = (u^a) · (A : u^a) when A ⊆ (u^a);

and, when R is a domain and u ≠ 0:

• Ideal.colon_span_pow_mul_self: cancellation, ((u^k) · C : u^k) = C;
• Ideal.colon_mul_pow_add, Ideal.colon_pow_pow_mul, Ideal.colon_sup_pow: the colon of a product, a power or a sum of ideals contained in the corresponding powers of (u) is the product, power or sum of the colons — the stalk form of the rules for products and sums of marked ideals [Kol07, Definition 59].

In a Noetherian local ring whose order (IsLocalRing.ord) is multiplicative, J ⊆ (u^m) with u ∈ 𝔪 and ord J ≤ m forces (J : u^m) = (1) (IsLocalRing.colon_span_singleton_pow_eq_top_of_ord_le).

None of these is stated in the sources; they are elementary. They are the local computations behind the weak transform of an ideal sheaf [Hir64, Ch. 0, §5, p. 142] on the scheme side, and behind the algebra of marked transforms of ideal sheaves on analytic manifolds.

Colon algebra in a domain: exact division by a power of a nonzero element

theorem Ideal.colon_coe_span_singleton_pow {R : Type u_1} [CommRing R] (A : Ideal R) (u : R) (k : ℕ) : Submodule.colon A ↑(span {u} ^ k) = Submodule.colon A {u ^ k}

The colon by the set of elements of the ideal (u)^k is the colon by the singleton {u ^ k}: the form in which a colon stalk (π⁻¹(J)_a : I_{F,a}^k) meets a generator u of the stalk I_{F,a} of the exceptional ideal.

theorem Ideal.colon_singleton_pow_mono {R : Type u_1} [CommRing R] (A : Ideal R) (u : R) {s t : ℕ} (hst : s ≤ t) : Submodule.colon A {u ^ s} ≤ Submodule.colon A {u ^ t}

The colon by a smaller power is smaller: (A : u^s) ⊆ (A : u^t) for s ≤ t. At a stalk this compares the transforms of one ideal under two markings, as in the proof of [Kol07, Theorem 100].

theorem Ideal.span_pow_mul_colon_of_le {R : Type u_1} [CommRing R] (A : Ideal R) (u : R) (a : ℕ) (hA : A ≤ span {u ^ a}) : span {u ^ a} * Submodule.colon A {u ^ a} = A

Exact division: an ideal A ⊆ (u^a) is u^a times its colon, A = (u^a) · (A : u^a). This is the identity π^* I = I_F^m · π_*^{-1}(I, m) of [Kol07, Definition 60] at a stalk.

theorem Ideal.colon_span_pow_mul_self {R : Type u_1} [CommRing R] [IsDomain R] (C : Ideal R) {u : R} (hu : u ≠ 0) (k : ℕ) : Submodule.colon (span {u ^ k} * C) {u ^ k} = C

Cancellation in a domain: ((u^k) · C : u^k) = C for u ≠ 0. The stalk form of the statement that the weak transform is determined by dividing out the exceptional ideal exactly [Hir64, Ch. 0, §5, p. 142].

theorem Ideal.colon_mul_pow_add {R : Type u_1} [CommRing R] [IsDomain R] (A B : Ideal R) {u : R} (hu : u ≠ 0) (a b : ℕ) (hA : A ≤ span {u ^ a}) (hB : B ≤ span {u ^ b}) : Submodule.colon (A * B) {u ^ (a + b)} = Submodule.colon A {u ^ a} * Submodule.colon B {u ^ b}

The product rule for colons by powers of a nonzero element: for A ⊆ (u^a) and B ⊆ (u^b), (A B : u^{a+b}) = (A : u^a) (B : u^b). The stalk form of the product of marked ideals (I₁, m₁) · (I₂, m₂) = (I₁ I₂, m₁ + m₂) [Kol07, Definition 59].

theorem Ideal.colon_pow_pow_mul {R : Type u_1} [CommRing R] [IsDomain R] (A : Ideal R) {u : R} (hu : u ≠ 0) (k s : ℕ) (hA : A ≤ span {u ^ k}) : Submodule.colon (A ^ s) {u ^ (k * s)} = Submodule.colon A {u ^ k} ^ s

The power rule: for A ⊆ (u^k), (A^s : u^{ks}) = (A : u^k)^s. At a stalk this is the compatibility of the marked transform with powers, (Π_*^{-1} I)^s = Π_*^{-1}(I^s), used in the proof of [Kol07, Theorem 100].

theorem Ideal.colon_sup_pow {R : Type u_1} [CommRing R] [IsDomain R] (A B : Ideal R) {u : R} (hu : u ≠ 0) (k : ℕ) (hA : A ≤ span {u ^ k}) (hB : B ≤ span {u ^ k}) : Submodule.colon (A ⊔ B) {u ^ k} = Submodule.colon A {u ^ k} ⊔ Submodule.colon B {u ^ k}

The sum rule: for A, B ⊆ (u^k), (A + B : u^k) = (A : u^k) + (B : u^k). The stalk form of the sum of marked ideals with the same marking, (I₁, m) + (I₂, m) = (I₁ + I₂, m) [Kol07, Definition 59].

The colon by a power of a parameter of order ≤ m

theorem IsLocalRing.colon_span_singleton_pow_eq_top_of_ord_le {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hmul : ∀ (f g : R), ordElem (f * g) = ordElem f + ordElem g) {u : R} (hu : u ∈ maximalIdeal R) {J : Ideal R} {m : ℕ} (hle : J ≤ Ideal.span {u} ^ m) (hord : ord J ≤ ↑m) : Submodule.colon J ↑(Ideal.span {u} ^ m) = ⊤

In a Noetherian local ring with multiplicative order, if J ⊆ (u^m) for u ∈ 𝔪 and ord J ≤ m, the colon (J : u^m) is the unit ideal — J = u^m · (J : u^m) (Ideal.span_pow_mul_colon_of_le), so m + ord (J : u^m) ≤ ord (u^m) + ord (J : u^m) = ord J ≤ m. This is the algebra behind "the order of I along E^{jk} is reduced by m" in the proof of [Kol07, Lemma 102] and in the one-dimensional case of the induction of [Kol07, 70]; not stated in the sources.