The saturation of an ideal sheaf of finite type is of finite type

For ideal sheaves of finite type J, I on a K-analytic space X, the saturation ⨆_k (J_x : I_x^k) of J by I is again an ideal sheaf of finite type (saturation_hasLocalGenerators). This is the finite type of the ideal of the strict transform asserted in [BM97, Proposition 3.13 and the sentence after it] ("I_{X'} is an ideal of finite type (since X is locally Noetherian)"), proved here over K = ℝ or ℂ at once and without the Noether lemma. The argument uses only the recurrence of the colon chain C_k := (J : I^k), which is stationary near every point with a uniform index (colonChain_locallyStationary):

• (a) C_{k+1} = (C_k : I), the associativity of colons (colon_pow_succ);
• (b) the stalk 𝒪_{X,x} is Noetherian (AnalyticSpace.isNoetherianRing_stalk; Rückert's basis theorem [Dem12, Ch. II, (2.7)], carried to the stalks of an analytic space through its local models), so the chain is stationary at x (exists_colon_pow_stationary_at);
• (c) one equality C_{N,x} = C_{N+1,x} of ideal sheaves of finite type propagates to a neighbourhood (exists_opens_stalkIdeal_eq_of_le_of_eq: an identity between finitely many germs holds nearby, [Fre17, Ch. I, 10.5]);
• (d) the recurrence carries the equality up the chain on that neighbourhood (colonChain_locallyStationary).

Hence the saturation has local generators (saturation_hasLocalGenerators, through the bridge hasLocalGenerators_iSup_colon_pow_of_colonChain_locallyStationary). What the argument uses of the chain is the recurrence, which an arbitrary increasing chain of ideal sheaves lacks; for those one needs the Noether lemma. The theorem is the finite-type input of the strict transform (Hironaka.Manifold.BlowUp.Transform.SaturationFiniteType).

theorem AnalyticSpace.colon_pow_succ {R : Type u_1} [CommRing R] (J I : Ideal R) (k : ℕ) : Submodule.colon J ↑(I ^ (k + 1)) = Submodule.colon (Submodule.colon J ↑(I ^ k)) ↑I

In a commutative ring, (J : I^{k+1}) = ((J : I^k) : I): the associativity of colons.

theorem AnalyticSpace.exists_opens_stalkIdeal_eq_of_le_of_eq {Y : TopCat} {𝒪 : TopCat.Sheaf CommRingCat Y} {A B : Manifold.IdealSheaf 𝒪} (hAB : A ≤ B) {x : ↑Y} (hx : A.stalkIdeal x = B.stalkIdeal x) : ∃ (W : TopologicalSpace.Opens ↑Y) (_ : x ∈ W), ∀ y ∈ W, A.stalkIdeal y = B.stalkIdeal y

For ideal sheaves of finite type A ≤ B of a sheaf of rings with A_x = B_x, A = B on a neighbourhood of x [Fre17, Ch. I, 10.5]: the finitely many local generators of B have germs in A_x, hence are germs of sections of A (mem_stalkIdeal_iff), which agree with them near x; so they generate stalks of A on the common neighbourhood. This uses that IdealSheaf carries finite type.

theorem AnalyticSpace.exists_colon_pow_stationary_at {K : Type} [RCLike K] (X : AnalyticSpace K) (J I : Manifold.IdealSheaf X.𝒪) (x : ↑↑X.toPresheafedSpace) : ∃ (N : ℕ), ∀ m ≥ N, Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ m) = Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ N)

At a point x the increasing chain k ↦ (J_x : I_x^k) of ideals of the Noetherian stalk is stationary (monotone_stabilizes_iff_noetherian).

theorem AnalyticSpace.hasLocalGenerators_iSup_colon_pow_of_colonChain_locallyStationary {K : Type} [RCLike K] (X : AnalyticSpace K) (J I : Manifold.IdealSheaf X.𝒪) (hloc : ∀ (x : ↑↑X.toPresheafedSpace), ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ V) (N : ℕ), ∀ m ≥ N, ∀ y ∈ V, Submodule.colon (J.stalkIdeal y) ↑(I.stalkIdeal y ^ m) = Submodule.colon (J.stalkIdeal y) ↑(I.stalkIdeal y ^ N)) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => ⨆ (k : ℕ), Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ k)

The finite type of the saturation from the local stationarity of the one colon chain k ↦ (J_x : I_x^k), proved by the argument of hasLocalGenerators_iSup_colon_pow_of_locallyStationary (Hironaka.AnalyticSpace.NoetherDerived), which cannot be invoked here because its hypothesis quantifies over every chain.

theorem AnalyticSpace.colonChain_locallyStationary {K : Type} [RCLike K] (X : AnalyticSpace K) (J I : Manifold.IdealSheaf X.𝒪) (x : ↑↑X.toPresheafedSpace) : ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ V) (N : ℕ), ∀ m ≥ N, ∀ y ∈ V, Submodule.colon (J.stalkIdeal y) ↑(I.stalkIdeal y ^ m) = Submodule.colon (J.stalkIdeal y) ↑(I.stalkIdeal y ^ N)

The colon chain k ↦ (J_y : I_y^k) of two ideal sheaves of finite type on a K-analytic space is stationary with a uniform index near every point (the conclusion asserted in BM97, Proposition 3.13 and the sentence after it): (b) gives the index N at x, (c) propagates C_N = C_{N+1} to a neighbourhood, and (a) carries it up the chain by induction.

theorem AnalyticSpace.saturation_hasLocalGenerators {K : Type} [RCLike K] (X : AnalyticSpace K) (J I : Manifold.IdealSheaf X.𝒪) : Manifold.IdealSheaf.HasLocalGenerators fun (x : ↑↑X.toPresheafedSpace) => ⨆ (k : ℕ), Submodule.colon (J.stalkIdeal x) ↑(I.stalkIdeal x ^ k)

The saturation ⨆_k (J_x : I_x^k) of an ideal sheaf of finite type by another is of finite type, over K = ℝ or ℂ [BM97, Proposition 3.13 and the sentence after it]: the bridge applied to colonChain_locallyStationary. This is the finite-type input of the strict transform of a closed subspace.