The disjoining list is natural under local analytic isomorphisms

Functoriality for smooth morphisms [Kol07, 34.1] for the preliminary blow-ups of [Kol07, 72]: the meet loci of the pulled-back family are the preimages of the meet loci (meetLocus_comap), the strict transforms under the lift of a local analytic isomorphism to the blow-ups are the strict transforms of the pulled-back family (strictTransforms_comap_liftStep, from strictTransformSet_preimage_of_square), so the pull-back of the disjoining list along h is the disjoining list of the pulled-back family (disjoinList_pullback, by recursion on the multiplicity with pullback_cons; the pull-back of a blow-up sequence, [Kol07, 30.1]). This is the disjoining half of the compatibility clause of the principalization family (the independence of the shrinking open, Canonicity.lean).

theorem Manifold.HypersurfaceFamily.meetLocus_comap {M N : Type u} (F : HypersurfaceFamily M) (h : N → M) (m : ℕ) : (comap h F).meetLocus m = h ⁻¹' F.meetLocus m

The meet loci of the pulled-back family are the preimages of the meet loci.

theorem Hironaka.Manifold.strictTransforms_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (F : Manifold.HypersurfaceFamily M.carrier) : Manifold.HypersurfaceFamily.comap (⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY)) (Manifold.HypersurfaceFamily.strictTransforms (⇑(Manifold.blowUpπ ψ₀ hY)) Y F) = Manifold.HypersurfaceFamily.strictTransforms (⇑(Manifold.blowUpπ ψ₀ ⋯)) (⇑h ⁻¹' Y) (Manifold.HypersurfaceFamily.comap (⇑h) F)

The strict transforms of F under the blowing-up with centre Y, pulled back along the lift of a local analytic isomorphism h, are the strict transforms of h^* F under the blowing-up with centre h⁻¹(Y) (strictTransformSet_preimage_of_square).

theorem Hironaka.Manifold.disjoinList_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {F F' : Manifold.HypersurfaceFamily M.carrier} (e : F = F') (m : ℕ) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) (hF' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (hm' : F'.meetLocus (m + 1) = ∅) : disjoinList m F hF hm = disjoinList m F' hF' hm'

disjoinList respects an equality of families (the hypotheses transported).

theorem Hironaka.Manifold.disjoinList_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M N : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : (disjoinList m F hF hm).pullback h hh = disjoinList m (Manifold.HypersurfaceFamily.comap (⇑h) F) ⋯ ⋯

Functoriality of the disjoining blow-ups for local analytic isomorphisms ([Kol07, 34.1]): the pull-back of the disjoining list along a local analytic isomorphism h is the disjoining list of the pulled-back family.