Colon ideals of ideal sheaves have local generators

For ideal sheaves J, I of finite type on an analytic K-space, the stalkwise colon (J_x : I_x) has local generators (in the spirit of [Fre17, Ch. I, 10.6 and 10.8]). With I_x = (h₁, …, h_l) and J_x = (f₁, …, f_m) near x, r ∈ (J_x : I_x) iff r h_j ∈ J_x for every j, iff r extends to a relation (r, b) of the augmented matrix with rows (h_j | −f in block j); by coherence the relations are generated near x by finitely many sections R_n, and the first components R_{n,0} generate the colon at every point near x (hasLocalGenerators_colon_idealSheaf). This is the bookkeeping for the saturation ⋃_k (J : I^k), which describes the strict transform of a closed subspace under a blow-up ([BM97, Proposition 3.13] and the sentence after it, 𝓘_{X'} = ⋃_k [𝓘 : y_exc^k]): the colon ideal sheaves (J : I^k) form an increasing chain of ideal sheaves of finite type, whose local stationarity is the Noether lemma (Hironaka/AnalyticSpace/NoetherDerived.lean, Hironaka/AnalyticSpace/ModelTransport.lean).

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

The stalkwise colon (J_x : I_x) of two ideal sheaves of finite type on an analytic K-space has local generators.