Clause (3) of the principalization family: an isomorphism off cosupp 𝓘 ∪ Sing E

Clause (3) of [Kol07, Theorem 35] in the form that holds with the disjoining blow-ups included, per open: the composite blow-down of the value on U is an analytic isomorphism over U ∖ (cosupp 𝓘|U ∪ Sing E|U) (Kollár's "over X ∖ cosupp I" fails for the disjoining blow-ups, whose centres lie in the multiple locus Sing E). By isAnalyticIsoOver_stageMap (condition (1) of Bierstone–Milman's blowing-up [BM88, Definition 4.1], iterated) it suffices that every centre lies over cosupp 𝓘|U ∪ Sing E|U:

• the disjoining centres lie over Sing E|U (centersOver_disjoinList; [Kol07, 72]);
• the order-reduction centres lie over cosupp 𝓘|U: a centre of a sequence of order ≥ 1 for (𝓘, 1) lies in the cosupport of the marked transform there (clause (4′) of [Kol07, Definition 66], 1 ≤ ord_Z I_i at every point of Z, read by le_ordAlongIdeal_iff at p = 1), and the cosupport of the marked transform lies over the cosupport of 𝓘 (cosupport_markedTransformSeqAux_subset: the birational transform contains the total transform, cosupport_birationalTransform_I_subset, whose cosupport is the preimage, cosupport_pullback) — CentersOver.of_isOfOrderGe;
• the concatenation (centersOver_concat) and the deletion of the empty rounds — the composite blow-downs of a list and of its cleaned list agree through eraseEmptyLast (stageMap_last_eraseEmptyLast), so the analytic-isomorphism-over predicate transports (IsIsoOver.of_comp_diffeomorph).

Włodarczyk's corresponding statement is that the canonical principalization is an isomorphism over M_Z ∖ V(I) [Wlo09, Lemma 4.0.3].

The cosupport of the marked transforms

theorem Hironaka.Manifold.cosupport_birationalTransform_I_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (J : Manifold.MarkedIdealSheaf (Manifold.structureSheaf 𝕜 E M.carrier)) : (Manifold.MarkedIdealSheaf.birationalTransform hY h J).I.support ⊆ π ⁻¹' J.I.support

The birational transform of a marked ideal sheaf contains the total transform, so its cosupport lies in the preimage of the cosupport (the unit ideal when no exceptional divisor exists).

theorem AnalyticManifold.FiniteSuccession.cosupport_markedTransformSeqAux_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (m i : ℕ) (h : i < S.length + 1) : Manifold.IdealSheaf.support (S.markedTransformSeqAux J m i h) ⊆ ⇑(S.stageMapAux i h) ⁻¹' Manifold.IdealSheaf.support J

The cosupport of the marked transform at stage i lies over the cosupport of 𝓘.

theorem AnalyticManifold.FiniteSuccession.CentersOver.of_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrderGe I m E₀) (hm : 1 ≤ m) : S.CentersOver (Manifold.IdealSheaf.support I)

Clause (4′) of [Kol07, Definition 66] read on the cosupports: the centres of a sequence of order ≥ m ≥ 1 lie over the cosupport of 𝓘 — a centre lies in the cosupport of the marked transform at its stage (ord_Z I_i ≥ 1 at every point of Z), which lies over the cosupport of 𝓘.

Transport of IsAnalyticIsoOver along an analytic isomorphism of the source

theorem AnalyticMap.IsIsoOver.of_comp_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A B M : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) (f : AnalyticMap B M) (g : AnalyticMap A M) (hfg : ∀ (a : A.carrier), f (φ a) = g a) {U : Set M.carrier} (hg : g.IsIsoOver U) : f.IsIsoOver U

If f ∘ φ = g for an analytic isomorphism φ of the sources, then f is an analytic isomorphism over U when g is.

theorem AnalyticManifold.BlowUpSequence.isAnalyticIsoOver_stageMap_last_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {Z : Set M.carrier} (h : (L.toSuccession.stageMap (Fin.last L.toSuccession.length)).IsIsoOver Zᶜ) : (L.eraseEmpty.toSuccession.stageMap (Fin.last L.eraseEmpty.toSuccession.length)).IsIsoOver Zᶜ

The composite blow-down of the cleaned list is an analytic isomorphism over Zᶜ when the composite blow-down of the list is (stageMap_last_eraseEmptyLast).

theorem AnalyticManifold.BlowUpSequence.centersOver_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {L₁ L₂ : BlowUpSequence ψ₀ M} (e : L₁ = L₂) {Z : Set M.carrier} (h : L₁.toSuccession.CentersOver Z) : L₂.toSuccession.CentersOver Z

Transport of CentersOver along an equality of lists.

Clause (3) for the value

theorem Hironaka.Manifold.principalizationValue_centersOver_concat {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((disjoinListOn T (shrinkOpen U hU) ⋯).shrinkAppend (M.restrictLE ⋯) ⋯ ((bmo.functor.fam (disjoinedTriple (restrictTriple T (shrinkOpen U hU)) ⋯) ⋯).seqOn ((disjoinListOn T (shrinkOpen U hU) ⋯).liftRange (M.restrictLE ⋯) ⋯) ⋯)).toSuccession.CentersOver (Manifold.IdealSheaf.support (restrictTriple T U).I ∪ (restrictTriple T U).F.singularLocus)

The centres of the value on U, before the deletion of the empty rounds, lie over cosupp 𝓘|U ∪ Sing E|U.

theorem Hironaka.Manifold.principalizationValue_isAnalyticIsoOver {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (bmo : BMOanFam 𝕜 n 1) (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((principalizationValue bmo T U hU).toSuccession.stageMap (Fin.last (principalizationValue bmo T U hU).toSuccession.length)).IsIsoOver (Manifold.IdealSheaf.support (restrictTriple T U).I ∪ (restrictTriple T U).F.singularLocus)ᶜ

Clause (3) of [Kol07, Theorem 35] with the disjoining blow-ups included: the composite blow-down of the value on U is an analytic isomorphism over U ∖ (cosupp 𝓘|U ∪ Sing E|U).