Kollár's Theorem 97 in marked form, on lists of centres

Two blow-up sequences L, L' of M (lists of centres) that are local-isomorphism equivalent for (I, m) through ψ, ψ' : U ⇉ M ([Kol07, Definition 96], with local analytic isomorphisms in place of étale surjections), whose common pull-back C = ψ^*L = ψ'^*L' is of order ≥ 1 for (MC(ψ^*I), 1) and whose centres lie in the images of the lifts, are equal (BlowUpSequence.eq_of_locallyIsoEquivalentSequences) — Kollár's uniqueness of blow-up sequences [Kol07, Theorem 97], with the hypothesis "of order m = max-ord I" replaced by the marked form his induction actually uses (his "Z_i^U ⊆ W_i by (77)"). It is the induction BlowUpSequence.eq_of_pullback_eq_of_step (Hironaka/Resolution/Analytic/MaximalContact/Theorem97Induction.lean) fed with the one-step descent lemma agreeOnSubspace_blowUpLift (Hironaka/Resolution/Analytic/MaximalContact/OneStepDescent.lean) at the list's model chart ψ₀ at every stage. Włodarczyk's descent of the canonical resolution through the glueing automorphism is the same statement [Wlo09, Lemma 5.5.3 (5); §6, Step 1bb of the proof of Theorem 6.0.6]. It is what makes the order-reduction algorithm independent of the choice of the hypersurface of maximal contact (Hironaka/Resolution/Analytic/OrderReduction/FamilyIndependence.lean).

theorem AnalyticManifold.BlowUpSequence.eq_of_locallyIsoEquivalentSequences {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {I : M.IdealSheaf} {m : ℕ} {L L' : BlowUpSequence ψ₀ M} (e : Hironaka.Manifold.LocallyIsoEquivalentSequences I m L L') (hW : (L.pullback e.ψ ⋯).toSuccession.IsMarkedOne ((Manifold.IdealSheaf.pullback ⇑e.ψ ⋯ I).iteratedDeriv (m - 1))) (h3 : ∀ (i : Fin L.length), Manifold.IdealSheaf.support (L.toSuccession.center i) ⊆ Set.range ⇑(L.pullbackLift e.ψ ⋯ i.castSucc)) (h3' : ∀ (i : Fin L'.length), Manifold.IdealSheaf.support (L'.toSuccession.center i) ⊆ Set.range ⇑(L'.pullbackLift e.ψ' ⋯ i.castSucc)) : L = L'

Kollár's Theorem 97 in marked form [Kol07, Theorem 97]: two local-isomorphism equivalent lists of centres whose common pull-back is of order ≥ 1 for (MC(ψ^*I), 1), with centres in the images of the lifts, are equal — the induction eq_of_pullback_eq_of_step with the one-step descent lemma agreeOnSubspace_blowUpLift.