The ideal sheaf of a closed submanifold depends only on the set

IsClosedSubmanifold.idealSheaf is defined from a witness hY : IsClosedSubmanifold ψ Y c of the statement that Y is a closed submanifold of codimension c, read in the model chart ψ, but the ideal sheaf it produces is intrinsic to the set Y: at a point of Y a germ lies in it iff its section vanishes on Y nearby (germ_mem_stalkIdeal_idealSheaf_iff), and off Y it is the unit ideal. So two witnesses (ψ, c), (ψ', c') for the same set, or for sets equal by hypothesis, give the same ideal sheaf (IsClosedSubmanifold.idealSheaf_congr).

The fact is needed because a finite succession of blowings-up chooses the witnesses of its centres (the model chart and the codimension) from its monoidal-transformation clauses, while the proofs work at a fixed model chart and codimension; Hironaka.Manifold.FiniteSuccession.DerivTransform and the restriction and transport modules of Hironaka.Manifold.Sequence use it. A bookkeeping lemma, not in the sources.

theorem Manifold.IsClosedSubmanifold.idealSheaf_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n n' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y Y' : Set M} {c c' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ' Y' c') (hYY' : Y = Y') : hY.idealSheaf = hY'.idealSheaf

The ideal sheaf of a closed submanifold depends only on the set: two witnesses (ψ, c), (ψ', c') of IsClosedSubmanifold for the same set Y (or for equal sets) give the same idealSheaf, stalk by stalk: at a point of Y a germ lies in the stalk ideal iff its section vanishes on Y nearby (germ_mem_stalkIdeal_idealSheaf_iff), and off Y the stalk ideal is the unit ideal.