A blow-up sequence is an isomorphism off the images of its centres

Kollár's principalization theorem asserts that the composite Π : X_r → X "is an isomorphism over X ∖ cosupp I" [Kol07, Theorem 35 (3)]. For a triple with a boundary E the isomorphism holds over the complement of cosupp I ∪ Sing E, because the preliminary blow-ups that make the components of the boundary disjoint have their centres in the multiple locus of E [Kol07, 72]; the real-analytic principalization theorem (exists_extensionCompatibleFamily_isNormalCrossingsDivisor_jacobianIdeal_mul_pullback, Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean) has E = ∅ and asserts it off cosupp I. The mechanism is that each π_i is a blow-up with centre Z_i [Kol07, Definition 29], hence an analytic isomorphism off Z_i (condition (1) of [BM88, Definition 4.1], IsBlowUp.isLocalDiffeomorphOn_compl and IsBlowUp.bijOn_compl). This module iterates that along a finite succession whose centres all lie over a set Z ⊆ X (CentersOver Z: Z_i ⊆ Π_i⁻¹(Z)): every partial composite Π_i = π_0 ∘ ⋯ ∘ π_{i-1} is an analytic isomorphism over X ∖ Z (isAnalyticIsoOver_stageMap), by induction on i — off Π_{i+1}⁻¹(Z) the blow-up π_i lands off Z_i, where it is a local diffeomorphism and a bijection onto Π_i⁻¹(X ∖ Z), and the composite of local diffeomorphisms (Mathlib's IsLocalDiffeomorphAt.comp) and of bijections (Set.BijOn.comp) is one. The isomorphism clauses of the principalization and resolution theorems are this with Z = cosupp I ∪ Sing E, once the centres are so placed (Hironaka/Resolution/Analytic/Wlo09/IsoOverReg.lean).

def AnalyticManifold.FiniteSuccession.CentersOver {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (Z : Set M.carrier) : Prop

The centres of the succession all lie over Z: Z_i ⊆ Π_i⁻¹(Z) for every i (for the principalization, Z = cosupp I ∪ Sing E, the set over which nothing is blown up).

Equations

• S.CentersOver Z = ∀ (i : Fin S.length), Manifold.IdealSheaf.support (S.center i) ⊆ ⇑(S.stageMap i.castSucc) ⁻¹' Z

theorem AnalyticManifold.FiniteSuccession.isAnalyticIsoOver_stageMapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {Z : Set M.carrier} (hZ : S.CentersOver Z) (i : ℕ) (hi : i < S.length + 1) : (S.stageMapAux i hi).IsIsoOver Zᶜ

[Kol07, Theorem 35 (3)] along the partial composites (condition (1) of [BM88, Definition 4.1] iterated): when every centre lies over Z, the composite Π_i : X_i → X is an analytic isomorphism over X ∖ Z — stated on the auxiliary composite indexed by ℕ, by induction.

theorem AnalyticManifold.FiniteSuccession.isAnalyticIsoOver_stageMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {Z : Set M.carrier} (hZ : S.CentersOver Z) (i : Fin (S.length + 1)) : (S.stageMap i).IsIsoOver Zᶜ

[Kol07, Theorem 35 (3)] along the partial composites: when every centre lies over Z, the composite Π_i : X_i → X is an analytic isomorphism over X ∖ Z.

theorem AnalyticManifold.FiniteSuccession.CentersOver.mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {Z Z' : Set M.carrier} (hZ : S.CentersOver Z) (h : Z ⊆ Z') : S.CentersOver Z'

Centres over a smaller set are over a larger one.