The strict transform off the centre is an isomorphic copy; its points over ℂ

• Off the exceptional divisor the blowing-down π is a local analytic isomorphism (condition (1) of [BM88, Definition 4.1]), so its stalk maps are bijective (IsBlowUp.germMap_bijective_of_notMem: germMap π agrees with the stalk map of the partial diffeomorphism supplied by isLocalDiffeomorphOn_compl, bijective by germMapOn_partialDiffeomorph_bijective); hence the total transform of a subspace with radical stalks has radical stalks off the divisor (isRadical_stalkIdeal_totalTransform_of_notMem, via Ideal.map_radical_of_surjective).
• Over ℂ, |X'| = closure(π⁻¹(|X| ∖ Y)) ([BM97, Remark 3.15], with Rückert's Nullstellensatz). The inclusion ⊇ is general (closure_subset_cosupport_strictTransformSubspace_of_hasLocalGenerators). For ⊆: a point a' of |X'| outside the closure has a neighbourhood o meeting π⁻¹(|X| ∖ Y) in nothing, so on o the set |X'| lies in |F| (off F, |X'| = π⁻¹(|X|)); every germ f ∈ I_{F,a'} therefore vanishes on |X'| near a', i.e. f ∈ √(I_{X',a'}) by Rückert (vanishingStalkIdeal_cosupport_eq_radical at the analytic space of M'); the stalk being Noetherian, I_{F,a'}^k ⊆ I_{X',a'} = ⋃_j (π^*I : I_F^j) for some k, hence I_{F,a'}^{k+N} ⊆ π^*I_{a'} for some N, so 1 ∈ (π^*I : I_F^{k+N}) ⊆ I_{X',a'}, contradicting a' ∈ |X'|. The finite type of the saturation is the explicit hypothesis hex.

Rückert's Nullstellensatz for stalks and the Noetherianness of the stalks are proved in Hironaka.AnalyticSpace.Nullstellensatz and Hironaka.Manifold.Germ.StalkNoetherian.

theorem Manifold.IsBlowUp.germMap_bijective_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : IsBlowUp ψ Y c π) {a' : M'} (ha' : π a' ∉ Y) : Function.Bijective ⇑(germMap π ⋯ a')

At a point off the exceptional divisor the stalk map of the blowing-down is bijective — π is a local analytic isomorphism there.

theorem Manifold.isRadical_stalkIdeal_totalTransform_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (hI : ∀ (x : ↑↧M), (I.stalkIdeal x).IsRadical) {a' : M'} (ha' : π a' ∉ Y) : ((IdealSheaf.pullback π ⋯ I).stalkIdeal a').IsRadical

Off the exceptional divisor the total transform of a subspace with radical stalks has radical stalks (the stalk map is a ring isomorphism there).

theorem Manifold.radical_stalkIdeal_eq_vanishingStalkIdeal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} (ψ : E ≃L[ℂ] Fin n → ℂ) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf ℂ E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (J : IdealSheaf (structureSheaf ℂ E M')) (a' : M') : (J.stalkIdeal a').radical = AnalyticSpace.vanishingStalkIdeal (AnalyticSpace.toSpace ψ { carrier := M', top := inst✝, charted := inst✝¹, manifold := inst✝², t2 := inst✝³, secondCountable := inst✝⁴ }).toLocallyRingedSpace J.support a'

Rückert's Nullstellensatz at the analytic space Sp(M') of a complex manifold: the radical of a stalk ideal is the vanishing ideal of the cosupport.

theorem Manifold.mem_radical_stalkIdeal_of_cosupport_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} (ψ : E ≃L[ℂ] Fin n → ℂ) {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf ℂ E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (J F : IdealSheaf (structureSheaf ℂ E M')) {a' : M'} {o : TopologicalSpace.Opens M'} (ha'o : a' ∈ o) (ho : ∀ y' ∈ o, y' ∈ J.support → y' ∈ F.support) {f : ↑((structureSheaf ℂ E M').presheaf.stalk a')} (hf : f ∈ F.stalkIdeal a') : f ∈ (J.stalkIdeal a').radical

A germ of an ideal sheaf F at a' whose cosupport contains |J| near a' lies in the radical of J_{a'} (Rückert): it vanishes at every point of |J| near a'.

theorem Manifold.cosupport_strictTransformSubspace_eq_closure_of_hasLocalGenerators {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {n : ℕ} {ψ : E ≃L[ℂ] Fin n → ℂ} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf ℂ E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf ℂ E M)) (hex : IdealSheaf.HasLocalGenerators (saturationStalk hY h I)) : (strictTransformSubspace hY h I).support = closure (π ⁻¹' (I.support \ Y))

Over ℂ ([BM97, Remark 3.15], with Rückert's Nullstellensatz), given the finite type of the saturation: the strict transform is the closure of the transform off the centre, |X'| = closure(π⁻¹(|X| ∖ Y)).