The birational transform commutes with restriction to an open subset

For the blowing-up π' : π⁻¹(U) → U restricted over an open subset U ⊆ M (Hironaka.Manifold.BlowUp.Restrict), the birational transform of the restriction of (I, m) to U is the restriction to π⁻¹(U) of the birational transform of (I, m) (birationalTransform_restrict); this is the compatibility of the birational transform with restriction to open subsets [Kol07, Definition 30, 30.1]. The trace Y ∩ U of the centre is a closed submanifold of U, and its ideal sheaf is the pullback of I_Y along the inclusion (Hironaka.Manifold.BlowUp.Transform.Object). Hence the total transform and the exceptional ideal on π⁻¹(U) are the restrictions of those on M' (pullbacks compose, and π ∘ val = val ∘ π'), and the colon stalks of the birational transform on π⁻¹(U) are the images of the colon stalks on M' under the stalk isomorphism of the inclusion (Hironaka.Manifold.BlowUp.Transform.GermIso), so the two ideal sheaves have the same colon specification and coincide (IsDivExceptional.unique).

theorem Manifold.birationalTransform_restrict {𝕜 : Type} [RCLike 𝕜] {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] {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 π) {U : TopologicalSpace.Opens M} {U' : TopologicalSpace.Opens M'} (_hU' : ↑U' = π ⁻¹' ↑U) {π' : ↥U' → ↥U} (hπ' : ∀ (p : ↥U'), ↑(π' p) = π ↑p) (hY' : IsClosedSubmanifold ψ (Subtype.val ⁻¹' Y) c) (h' : IsBlowUp ψ (Subtype.val ⁻¹' Y) c π') (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) : (MarkedIdealSheaf.birationalTransform hY' h' { I := IdealSheaf.pullback Subtype.val ⋯ I, m := m }).I = IdealSheaf.pullback Subtype.val ⋯ (MarkedIdealSheaf.birationalTransform hY h { I := I, m := m }).I

The birational transform commutes with restriction to an open subset [Kol07, Definition 30, 30.1]: for the restricted blowing-up π' : π⁻¹(U) → U of Hironaka.Manifold.BlowUp.Restrict, the birational transform of the restriction of (I, m) to U is the restriction to π⁻¹(U) of the birational transform of (I, m). The total transform and the exceptional ideal restrict (pullbacks compose and π ∘ val = val ∘ π'), the colon stalks restrict along the stalk isomorphism of the inclusion, and the colon specification determines the sheaf.