The value of the principalization family restricts

The compatibility clause of the compatible-family form ([Wlo09, Theorem 2.0.3 (4)]; Kollár's functoriality for smooth morphisms, [Kol07, 34.1], per open) for the value of Assembly.lean at a fixed shrinking open W: for U ≤ V both relatively compact with closures in W, the value on U computed with W is the value on V computed with W, pulled back along the open inclusion U → V and with the empty rounds erased (principalizationValueOn_restrict). The proof is the restriction law of the shrink-and-append step (shrinkAppend_pullback_eraseEmpty): the disjoining list over W is the same on both sides, the open inclusions compose (restrictLE), and the order-reduction values on the two reading opens are related by the input family's own compatibility clause (the reading open over U lying in the reading open over V). The independence of W is Canonicity.lean.

theorem Hironaka.Manifold.restrictLE_comp_restrictLE {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {U V W : TopologicalSpace.Opens M.carrier} (hUV : U ≤ V) (hVW : V ≤ W) : ContMDiffMap.comp (M.restrictLE hVW) (M.restrictLE hUV) = M.restrictLE ⋯

The open inclusions of the chain compose: U → V → W is U → W.

theorem Hironaka.Manifold.principalizationValueOn_restrict {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) {U V W : TopologicalSpace.Opens M.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hW : IsCompact (closure ↑W)) (hUW : closure ↑U ⊆ ↑W) (hVW : closure ↑V ⊆ ↑W) (hUV : U ≤ V) : principalizationValueOn bmo T U hU W hW hUW = ((principalizationValueOn bmo T V hV W hW hVW).pullback (M.restrictLE hUV) ⋯).eraseEmpty

The value restricts at a fixed shrinking open ([Wlo09, Theorem 2.0.3 (4)]; [Kol07, 34.1] per open): for U ≤ V with closures in W, the value on U computed with W is the value on V computed with W, pulled back along U → V, with the empty rounds erased.