The loci of Hironaka's Corollary 1 and the descent of the order to the base

The proof of [Hir64, Corollary 1 to Main Theorem II] (the simultaneous reduction of a finite system of ideal sheaves J_1, …, J_e) works on the open subscheme X ∖ S of the points where no J_j is trivial or ν(∏ J_j) < d, and reads off clause (ii) of Main Theorem II that the centers of the resulting sequence "are mapped into the closed subset T − S" of X.

• trivializationLoci_closed: T − S = {x : ν((∏ J_j)_x) ≥ d ∧ ∀ j, x ∈ supp J_j} is closed, as the intersection of {ord ≥ d}, closed by the upper semicontinuity of the order (isClosed_setOf_le_ord, characteristic zero), with the closed supports. Hironaka asserts T, S and T − S closed without proof ("we can prove"); T − S is proved closed here and S in Hironaka/Resolution/Algebraic/Hir64/Corollary1.lean (isClosed_trivialLocus); both are used.
• le_ord_stageMap_of_le_ord_weakTransformSeq (and its general form without the setting of the Corollary): along a sequence whose centers carry weak-transform order ≥ d (clause (ii) of Main Theorem II), a point of a stage at which the weak transform has order ≥ d lies over a point of X at which J has order ≥ d. By induction on the sequence: over a point off the center the blow-up is a local isomorphism and the weak transform has the order of J there (ord_weakTransform_of_notMem); over a point of the center, (ii) gives ν(J_i) ≥ d at that point. Applied to the centers themselves it is Hironaka's "all the D(i) are mapped into T − S".

The locus T − S is closed

theorem Hironaka.Sequence.trivializationLoci_closed {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] (hN : ∃ (N : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension N (X ↘ AlgebraicGeometry.Spec ↧k)) {e : ℕ} (J : Fin e → X.IdealSheafData) (d : ℕ) : IsClosed {x : ↥X | ↑d ≤ (∏ j : Fin e, J j).ord x ∧ ∀ (j : Fin e), x ∈ (J j).support}

T − S is closed (asserted without proof in the proof of Hir64, Corollary 1 to Main Theorem II): {ord (∏ J_j) ≥ d} is closed by the upper semicontinuity of the order (isClosed_setOf_le_ord) and the supports are closed.

Points of order ≥ d lie over points of order ≥ d

theorem Hironaka.Sequence.le_ord_stageMap_of_le_ord_weakTransformSeq_gen {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (d : ℕ) : (∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, ↑d ≤ (S.weakTransformSeq J i.castSucc).ord x) → ∀ (i : Fin (S.length + 1)) (z : ↥(S.stage i)), ↑d ≤ (S.weakTransformSeq J i).ord z → ↑d ≤ J.ord ((S.stageMap i) z)

The general form, on any scheme: along a sequence whose centers have weak-transform order ≥ d, a point of order ≥ d of a weak transform lies over a point of order ≥ d of J. Induction on the sequence, off the center by ord_weakTransform_of_notMem, on the center by the hypothesis on the centers.

theorem Hironaka.Sequence.le_ord_stageMap_of_le_ord_weakTransformSeq {k : Type u} [Field k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] (_hN : ∃ (N : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension N (X ↘ AlgebraicGeometry.Spec ↧k)) (S : X.BlowUpSequence) (J : X.IdealSheafData) (d : ℕ) (hii : ∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, ↑d ≤ (S.weakTransformSeq J i.castSucc).ord x) (i : Fin (S.length + 1)) (z : ↥(S.stage i)) (hz : ↑d ≤ (S.weakTransformSeq J i).ord z) : ↑d ≤ J.ord ((S.stageMap i) z)

A point of order ≥ d of a weak transform lies over a point of order ≥ d of J, in the setting of [Hir64, Corollary 1 to Main Theorem II] (by clause (ii) of Main Theorem II, all the centers D(i) "are mapped into the closed subset T − S"); the general form is le_ord_stageMap_of_le_ord_weakTransformSeq_gen.