The stalk of a product of ideal sheaves with disjoint supports

A stalk computation used by the embedded desingularization at a point of an isolated strict transform, where the ideal to be resolved further is the colon I : I_Γ by the reduced ideal I_Γ of the union of the strict transforms already isolated, the product of the pairwise disjoint strict transforms (the isolation of the components in the proof of [Wlo05, Theorem 4.7.1]; compare the factorization I = M(I) · N(I) of [Kol07, Definition–Lemma 110]). The lemma stalkIdeal_finset_prod_eq_of_mem_of_pairwise_disjoint says that the stalk of a product of ideal sheaves with pairwise disjoint supports at a point of one member's support is that member's stalk (the other factors are the unit ideal there); it is the indexed form, on any scheme, of Hironaka.Resolution.stalkIdeal_prod_eq_of_mem. The stalk of the colon itself is stalkIdeal_colon_of_isLocallyNoetherian (Hironaka/Scheme/BlowUp/FlatColon.lean), imported here for the modules of the embedded desingularization.

theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_finset_prod_eq_of_mem_of_pairwise_disjoint {X : Scheme} {ι : Type u_1} (A : Finset ι) (I : ι → X.IdealSheafData) (hdisj : (↑A).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) {a : ι} (ha : a ∈ A) {x : ↥X} (hx : x ∈ (I a).support) : (∏ b ∈ A, I b).stalkIdeal x = (I a).stalkIdeal x

The stalk of a product of ideal sheaves with pairwise disjoint supports at a point of one member's support is that member's stalk; the other factors have the unit stalk there (the indexed form of Hironaka.Resolution.stalkIdeal_prod_eq_of_mem, on any scheme).