The centres of the resolution rounds lie over the cosupport

For the value resolveSeqOn bo T U hU of the resolution family on a relatively compact open U (the rounds d_U, …, 1 of the order-reduction functors bo d, Hironaka/Resolution/Analytic/Wlo09/Rounds.lean), the composite blow-down is an analytic isomorphism over U ∖ V(𝓘|_U): clause (3) of [Kol07, Theorem 35] and [Wlo09, Lemma 4.0.3], proved from the fields of the functors bo alone.

• centersOver_resolveFrom, the invariant of the recursion resolveFrom: every centre of the rounds from d on the current triple cur, read on N along the local analytic isomorphism ι, lies over ι⁻¹(V(cur.I)). Round by round: the value of the round bo (d + 1) on Ω d is a sequence of order ≥ d + 1 for the restricted marked ideal ([Kol07, Definition 66 (4′)], the field isOfOrderGe), so its centres lie in the cosupport of the current marked transform, which lies over the cosupport of cur.I (FiniteSuccession.CentersOver.of_isOfOrderGe, cosupport_markedTransformSeqAux_subset); the pull-back along the corestriction of ι transports the invariant (IdealSheaf.support_pullback); the derived triple's ideal is the marked transform at mark d + 1 (AnalyticTriple.induced; Hironaka's weak transform [Hir64, p. 142], see Hironaka/Resolution/Analytic/Wlo09/HironakaClauses.lean), whose cosupport lies over the previous one; the last-stage lift of ι lies over ι (stageMap_last_pullbackLiftLast); centersOver_concat splits the concatenation at the round's last stage.
• isAnalyticIsoOver_stageMap_last_resolveSeqOn: the composite blow-down of resolveSeqOn bo T U hU is an analytic isomorphism over U ∖ V(𝓘|_U) (FiniteSuccession.isAnalyticIsoOver_stageMap on the invariant along the canonical chain, the deletion of the empty rounds transporting the predicate, isAnalyticIsoOver_stageMap_last_eraseEmpty).

The glued form on the whole manifold is isAnalyticIsoOver_resolveFamExt_map (Hironaka/Resolution/Analytic/Wlo09/FamilyExt.lean), by CompatibleFamily.isAnalyticIsoOver_limitBlowDown (Hironaka/Resolution/Analytic/Functor/LimitGluing.lean).

theorem Hironaka.Manifold.centersOver_resolveFrom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑d) (hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) : (resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange).toSuccession.CentersOver (⇑ι ⁻¹' Manifold.IdealSheaf.support cur.I)

The invariant of the recursion resolveFrom: every centre of the rounds from d on the current triple cur, read on N along ι, lies over the cosupport of cur.I. The round's centres lie in the cosupport of the current marked transform (the order bound isOfOrderGe, [Kol07, Definition 66 (4′)]), the cosupport of the marked transform lies over the previous one, and the last-stage lift of ι lies over ι.

theorem Hironaka.Manifold.isAnalyticIsoOver_stageMap_last_resolveSeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((resolveSeqOn bo T U hU).toSuccession.stageMap (Fin.last (resolveSeqOn bo T U hU).toSuccession.length)).IsIsoOver (Manifold.IdealSheaf.support (restrictTriple T U).I)ᶜ

The composite blow-down of the value resolveSeqOn bo T U hU is an analytic isomorphism over U ∖ V(𝓘|_U) ([Kol07, Theorem 35 (3)]; [Wlo09, Lemma 4.0.3]): the centres of the rounds lie over the cosupport (centersOver_resolveFrom along the canonical chain), FiniteSuccession.isAnalyticIsoOver_stageMap, and the deletion of the empty rounds transports the predicate (isAnalyticIsoOver_stageMap_last_eraseEmpty).