Hironaka's clauses (i)–(iv) on the resolution family

The dictionary between Kollár's smooth blow-up sequence of order ≥ m for a marked ideal (Kol07, Definition 66; the field isOfOrderGe of BOanFam, on the marked transforms) and the clauses (i)–(iv) of Hironaka's Main Theorem II′(N) [Hir64, p. 156] on the value resolveSeqOn bo T U hU of the resolution family (Hironaka/Resolution/Analytic/Wlo09/Rounds.lean): the rounds BO_{n,d}, …, BO_{n,1} of [Hir64, Main Theorem II(N), p. 176] with the empty blow-ups erased.

The dictionary on one round

• BOanFam.isOfOrder_seqOn: the value of B : BOanFam 𝕜 n m on a triple of its class over a relatively compact open is a sequence of order exactly m on the weak transforms (isOfOrder_of_isOfOrderGe_of_ord_le; [Kol07, Remark 67]: along a sequence of order ≥ m starting with max-ord I = m, every blow-up has order exactly m); BOanFam.markedTransformSeq_seqOn_eq_weakTransformSeq: along the round the marked transform is the weak transform (Kollár's birational transform of (I, m) when ord_Z I = m, [Kol07, Definition 48]; Hironaka's weak transform, [Hir64, p. 142]); BOanFam.ord_weakTransformSeq_seqOn_eq_of_mem_center: the order of the weak transform is m at every point of every centre (clause (2) of [Hir64, Main Theorem II(N), p. 176]).
• FiniteSuccession.IsOfOrder.ord_weakTransformSeq_eq_of_mem_center (the pointwise form on any succession: ≥ from the order along the centre, ≤ from [Kol07, Lemma 61] iterated) and FiniteSuccession.center_isNonsingular (clause (i): every centre is the ideal sheaf of a closed submanifold, hence non-singular).

Clause (ii) in Hironaka's weak spelling

• FiniteSuccession.HasConstantPositiveOrderAlongCenters S J (Hironaka/Manifold/Resolution/Defs.lean): at every stage the order of the weak transform of J is a positive constant on the centre, clause (ii) as a predicate; hasConstantPositiveOrderAlongCenters_nil, hasConstantPositiveOrderAlongCenters_cons_iff, IsOfOrder.hasConstantPositiveOrderAlongCenters (a round satisfies it with the constant m), and the transports along a concatenation, a pull-back along any local analytic isomorphism (the weak transform's exponent is the generic order along the component through the point, which a local isomorphism preserves; no surjectivity is needed), a diffeomorphism and the deletion of the empty blow-ups (hasConstantPositiveOrderAlongCenters_{concat,pullback,map,eraseEmpty}).
• hasConstantPositiveOrderAlongCenters_resolveFrom, the invariant of the recursion resolveFrom (on the pattern of centersOver_resolveFrom, Hironaka/Resolution/Analytic/Wlo09/CentersOver.lean): the round pulled back along the corestriction of ι, the junction identity (the head's last weak transform of ι^* 𝓘 is the pull-back along pullbackLiftLast of the derived ideal, the weak transform being the marked transform at the round's mark) and the induction hypothesis on the derived triple; hasConstantPositiveOrderAlongCenters_resolveSeqOn at the canonical chain, through the erasure.

Clauses (iii) and (iv)

• Clause (iii) is the first conjunct of isOfOrderGe_zero_resolveSeqOn (Hironaka/Resolution/Analytic/Wlo09/Monomial.lean, clause (3′) of [Kol07, Definition 66] for the erased value) read through the identification restrictTriple_F_idealSheaf of the restricted triple's boundary ideal sheaf (idealSheaf_comap_of_isSnc at the inclusion); center_resolveSeqOn_hasSncWith is its family form, a corollary through hasSncWith_totalTransformSeqFrom_center_of_forall_lt.
• The first half of clause (iv): FiniteSuccession.hasOnlyNormalCrossings_boundarySeq_last_of_isOfOrderGe_zero (along a sequence of order ≥ 0 for (I, 0, red F) with F a simple normal crossing family, the last boundary has only normal crossings: isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt then hasOnlyNormalCrossings_idealSheaf), at isOfOrderGe_zero_resolveSeqOn. Hironaka remarks that this half follows from (iii) (the remark after [Hir64, Main Theorem II, p. 143]).
• The second half of clause (iv): weakTransformSeq_last_eq_top_{concat,pullback,eraseEmpty} (the transports of the statement that the last weak transform is the unit ideal), weakTransformSeq_last_resolveFrom_eq_top (the exit of the recursion in the weak spelling: at d = 0 the list is empty and cur.I = ⊤ from ord ≤ 0; clause (1) of [Kol07, Theorem 68] at the last round's mark 1) and weakTransformSeq_last_resolveSeqOn_eq_top.

Restatements

The last section restates the clauses under the names resolveSeqOn_clause_ii, resolveSeqOn_clause_iii and resolveSeqOn_boundarySeq_last_hasOnlyNormalCrossings. Each docstring says which theorem it restates and how the predicate is unfolded; Hironaka/Resolution/Analytic/Wlo09/HironakaAssembly.lean uses resolveSeqOn_clause_ii, and the other two are not used elsewhere.

theorem AnalyticManifold.FiniteSuccession.hasConstantPositiveOrderAlongCenters_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) : (nil M).HasConstantPositiveOrderAlongCenters J

The empty succession satisfies clause (ii).

theorem AnalyticManifold.FiniteSuccession.hasConstantPositiveOrderAlongCenters_cons_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (J : M.IdealSheaf) : (cons ψ hY rest).HasConstantPositiveOrderAlongCenters J ↔ (∃ (c' : ℕ), 0 < c' ∧ ∀ y ∈ Y, Manifold.IdealSheaf.ord J y = ↑c') ∧ rest.HasConstantPositiveOrderAlongCenters (IdealSheaf.weakTransform (Manifold.blowUpπ ψ hY) J hY.idealSheaf)

The constructor form (the analogue of isOfOrderGe_cons_iff): the head clause on Y for J and the tail for the weak transform of J along the head.

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.ord_weakTransformSeq_eq_of_mem_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) (hI : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) (i : Fin S.length) {y : (S.stage i.castSucc).carrier} (hy : y ∈ Manifold.IdealSheaf.support (S.center i)) : Manifold.IdealSheaf.ord (S.weakTransformSeq I i.castSucc) y = ↑m

The pointwise form of the round dictionary: along a sequence of order exactly m with ord I ≤ m everywhere, the weak transform has order m at every point of every centre (≥ from the order along the centre, ≤ from [Kol07, Lemma 61] iterated).

theorem AnalyticManifold.FiniteSuccession.IsOfOrder.hasConstantPositiveOrderAlongCenters {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S : M.FiniteSuccession} {I E₀ : M.IdealSheaf} {m : ℕ} (h : S.IsOfOrder I E₀ m) (hm : 1 ≤ m) (hI : ∀ (y : ↑↧M.carrier), Manifold.IdealSheaf.ord I y ≤ ↑m) : S.HasConstantPositiveOrderAlongCenters I

The round dictionary on any succession: Hironaka's sequence of order exactly m ≥ 1 with ord I ≤ m everywhere satisfies clause (ii) with the constant m (IsOfOrder.ordAlong_eq, ordAlongIdeal_le_ord_of_mem_support, ord_markedTransformSeq_le through IsOfOrder.markedTransformSeq_eq_weakTransformSeq).

theorem AnalyticManifold.FiniteSuccession.center_isNonsingular {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : (S.center i).IsNonsingular

Clause (i) of [Hir64, Main Theorem II′(N), p. 156]: every centre of a finite succession is non-singular (idealSheaf_center and isNonsingular_idealSheaf).

theorem AnalyticManifold.FiniteSuccession.hasOnlyNormalCrossings_boundarySeq_last_of_isOfOrderGe_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {I : M.IdealSheaf} (h : S.IsOfOrderGe I 0 F.idealSheaf) : (S.boundarySeq F.idealSheaf (Fin.last S.length)).HasOnlyNormalCrossings

The first half of clause (iv) of [Hir64, Main Theorem II′(N), p. 156], in general form (Hironaka remarks after Main Theorem II, p. 143, that it follows from (iii)): along a succession of order ≥ 0 for (I, 0, red F) with F a simple normal crossing family, that is, under clause (3′) of [Kol07, Definition 66] alone, the last boundary has only normal crossings (isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt and hasOnlyNormalCrossings_idealSheaf).

theorem AnalyticManifold.BlowUpSequence.hasConstantPositiveOrderAlongCenters_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) (J : M.IdealSheaf) : L.toSuccession.HasConstantPositiveOrderAlongCenters J → L'.toSuccession.HasConstantPositiveOrderAlongCenters (L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length)) → (L.concat L').toSuccession.HasConstantPositiveOrderAlongCenters J

Clause (ii) along a concatenation (the analogue of isOfOrderGe_concat): the tail starts at the head's last weak transform.

theorem AnalyticManifold.BlowUpSequence.hasConstantPositiveOrderAlongCenters_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (hL : L.toSuccession.HasConstantPositiveOrderAlongCenters J) : (L.pullback h hh).toSuccession.HasConstantPositiveOrderAlongCenters (Manifold.IdealSheaf.pullback ⇑h ⋯ J)

Clause (ii) pulls back along any local analytic isomorphism, surjective or not (center_pullback, weakTransformSeq_pullback, ord_comap_of_isLocalDiffeomorphAt at the lifts).

theorem AnalyticManifold.BlowUpSequence.hasConstantPositiveOrderAlongCenters_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) (Z : BlowUpSequence ψ₀ M) (J : N.IdealSheaf) (h : Z.toSuccession.HasConstantPositiveOrderAlongCenters (Manifold.IdealSheaf.pullback ⇑φ.toAnalyticMap ⋯ J)) : (map φ Z).toSuccession.HasConstantPositiveOrderAlongCenters J

Clause (ii) transports along a diffeomorphism (map_eq_pullback_symm, hasConstantPositiveOrderAlongCenters_pullback, comap_comap_symm).

theorem AnalyticManifold.BlowUpSequence.hasConstantPositiveOrderAlongCenters_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (J : M.IdealSheaf) : L.toSuccession.HasConstantPositiveOrderAlongCenters J → L.eraseEmpty.toSuccession.HasConstantPositiveOrderAlongCenters J

Clause (ii) survives the deletion of the empty blow-ups ([Kol07, 34.1]; the pattern of isOfOrderGe_eraseEmpty: a kept step by hasConstantPositiveOrderAlongCenters_cons_iff, a deleted step by hasConstantPositiveOrderAlongCenters_map along emptyBlowUpDiffeomorph with weakTransform_blowUpπ_of_eq_empty). No boundary is involved, so no simple-normal-crossings hypothesis.

theorem AnalyticManifold.BlowUpSequence.weakTransformSeq_last_eq_top_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) (J : M.IdealSheaf) : L'.toSuccession.weakTransformSeq (L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length)) (Fin.last L'.toSuccession.length) = ⊤ → (L.concat L').toSuccession.weakTransformSeq J (Fin.last (L.concat L').toSuccession.length) = ⊤

The last weak transform is the unit ideal along a concatenation, from the tail started at the head's last weak transform (stated as a transport of the proposition, so no cast across stage_last_concat).

theorem AnalyticManifold.BlowUpSequence.weakTransformSeq_last_eq_top_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (J : M.IdealSheaf) (hL : L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length) = ⊤) : (L.pullback h hh).toSuccession.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) (Fin.last (L.pullback h hh).toSuccession.length) = ⊤

The same along a pull-back (weakTransformSeq_pullback at the last stage, comap ⊤ = ⊤).

theorem AnalyticManifold.BlowUpSequence.weakTransformSeq_last_eq_top_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (J : M.IdealSheaf) (hL : L.toSuccession.weakTransformSeq J (Fin.last L.toSuccession.length) = ⊤) : L.eraseEmpty.toSuccession.weakTransformSeq J (Fin.last L.eraseEmpty.toSuccession.length) = ⊤

The same after the deletion of the empty blow-ups (weakTransformSeq_last_eraseEmpty).

theorem Hironaka.Manifold.BOanFam.isOfOrder_seqOn {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (B : BOanFam 𝕜 n m) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((B.functor.fam T hT).seqOn U hU).toSuccession.IsOfOrder (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F.idealSheaf m

The value of B on a triple of its class over a relatively compact open is a sequence of order exactly m ([Kol07, Remark 67]): isOfOrder_of_isOfOrderGe_of_ord_le on the field B.isOfOrderGe with the class bound restricted to U (ord_comap_of_isLocalDiffeomorphAt).

theorem Hironaka.Manifold.BOanFam.markedTransformSeq_seqOn_eq_weakTransformSeq {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (B : BOanFam 𝕜 n m) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin (((B.functor.fam T hT).seqOn U hU).toSuccession.length + 1)) : ((B.functor.fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I m i = ((B.functor.fam T hT).seqOn U hU).toSuccession.weakTransformSeq (T.pullback (M.inclusion U) ⋯).I i

Along the value of B the marked transform at mark m is the weak transform: Kollár's birational transform of (I, m) coincides with the unmarked one when ord_Z I = m (Kol07, Definition 48), and that is Hironaka's weak transform ([Hir64, p. 142]).

theorem Hironaka.Manifold.BOanFam.ord_weakTransformSeq_seqOn_eq_of_mem_center {𝕜 : Type} [RCLike 𝕜] {n m : ℕ} (B : BOanFam 𝕜 n m) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin ((B.functor.fam T hT).seqOn U hU).toSuccession.length) {y : (((B.functor.fam T hT).seqOn U hU).toSuccession.stage i.castSucc).carrier} (hy : y ∈ Manifold.IdealSheaf.support (((B.functor.fam T hT).seqOn U hU).toSuccession.center i)) : Manifold.IdealSheaf.ord (((B.functor.fam T hT).seqOn U hU).toSuccession.weakTransformSeq (T.pullback (M.inclusion U) ⋯).I i.castSucc) y = ↑m

Along the value of B the weak transform has order m at every point of every centre (clause (2) of [Hir64, Main Theorem II(N), p. 176]).

theorem Hironaka.Manifold.restrictTriple_F_idealSheaf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (U : TopologicalSpace.Opens M.carrier) : (T.pullback (M.inclusion U) ⋯).F.idealSheaf = AnalyticManifold.IdealSheaf.restrict T.F.idealSheaf U

The restricted triple's boundary ideal sheaf is the restriction of the boundary ideal sheaf (HypersurfaceFamily.idealSheaf_comap_of_isSnc at the inclusion).

theorem Hironaka.Manifold.hasConstantPositiveOrderAlongCenters_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.HasConstantPositiveOrderAlongCenters (Manifold.IdealSheaf.pullback ⇑ι ⋯ cur.I)

The invariant of the recursion resolveFrom for clause (ii) (Hir64, Main Theorem II′(N), p. 156, (ii) round by round, on the pattern of centersOver_resolveFrom): the round pulled back along the corestriction of ι by hasConstantPositiveOrderAlongCenters_pullback and IsOfOrder.hasConstantPositiveOrderAlongCenters (AnalyticTriple.isOfOrderGe_pullback, isOfOrder_of_isOfOrderGe_of_ord_le with the class bound transported), the tail by the induction hypothesis on the derived triple with the junction identity (the head's last weak transform of ι^* cur.I is the pull-back along pullbackLiftLast of the derived ideal: markedTransformSeq_seqOn_eq_weakTransformSeq at the round, markedTransformSeq_last_pullbackLiftLast), glued by hasConstantPositiveOrderAlongCenters_concat.

theorem Hironaka.Manifold.weakTransformSeq_last_resolveFrom_eq_top {𝕜 : 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.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑ι ⋯ cur.I) (Fin.last (resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange).toSuccession.length) = ⊤

The invariant of the recursion resolveFrom for the second half of clause (iv), in the weak spelling ([Hir64, Main Theorem II′(N), p. 156, (iv)]; clause (1) of [Kol07, Theorem 68] at the last round's mark 1): the last weak transform of ι^* cur.I along the rounds from d is the unit ideal. The recursion of hasConstantPositiveOrderAlongCenters_resolveFrom with weakTransformSeq_last_eq_top_concat and weakTransformSeq_last_eq_top_pullback at the junction; at d = 0 the list is empty and cur.I = ⊤ from ∀ x, ord x ≤ 0, the same exit as inside pullbackIsMonomialAtLast_resolveFrom.

theorem Hironaka.Manifold.hasConstantPositiveOrderAlongCenters_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.HasConstantPositiveOrderAlongCenters (T.I.restrict U)

Clause (ii) for the value resolveSeqOn bo T U hU: hasConstantPositiveOrderAlongCenters_resolveFrom at the canonical chain (resolveSeqOn = (resolveFrom …).eraseEmpty by rfl), hasConstantPositiveOrderAlongCenters_eraseEmpty, and the reading map's identity comap (restrictLE _) (outerTriple).I = T.I.restrictOpens U (IdealSheaf.pullback_comp).

theorem Hironaka.Manifold.weakTransformSeq_last_resolveSeqOn_eq_top {𝕜 : 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.weakTransformSeq (T.I.restrict U) (Fin.last (resolveSeqOn bo T U hU).toSuccession.length) = ⊤

The second half of clause (iv) for the value resolveSeqOn bo T U hU: the last weak transform of 𝓘|_U is the unit ideal (weakTransformSeq_last_resolveFrom_eq_top at the canonical chain, through the erasure weakTransformSeq_last_eq_top_eraseEmpty and the reading map's identity).

theorem Hironaka.Manifold.center_resolveSeqOn_hasSncWith {𝕜 : 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)) (i : Fin (resolveSeqOn bo T U hU).toSuccession.length) : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) ((resolveSeqOn bo T U hU).toSuccession.totalTransformSeqFrom (restrictTriple T U).F i.castSucc) (Manifold.IdealSheaf.support ((resolveSeqOn bo T U hU).toSuccession.center i)) ((resolveSeqOn bo T U hU).toSuccession.codim i)

The centres of resolveSeqOn bo T U hU have simple normal crossings with the accumulated family totalTransformSeqFrom (restrictTriple T U).F at their stage: clause (3′) of [Kol07, Definition 66] in the family form, from its ideal-sheaf form isOfOrderGe_zero_resolveSeqOn (Hironaka/Resolution/Analytic/Wlo09/Monomial.lean) through hasSncWith_totalTransformSeqFrom_center_of_forall_lt.

Restatements under the names of the clauses

theorem Hironaka.Manifold.resolveSeqOn_clause_ii (𝕜 : 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)) (i : Fin (resolveSeqOn bo T U hU).toSuccession.length) : ∃ (c : ℕ), 0 < c ∧ ∀ y ∈ Manifold.IdealSheaf.support ((resolveSeqOn bo T U hU).toSuccession.center i), Manifold.IdealSheaf.ord ((resolveSeqOn bo T U hU).toSuccession.weakTransformSeq (T.I.restrict U) i.castSucc) y = ↑c

Clause (ii) of [Hir64, Main Theorem II′(N), p. 156] for the value resolveSeqOn bo T U hU, with the predicate HasConstantPositiveOrderAlongCenters of hasConstantPositiveOrderAlongCenters_resolveSeqOn unfolded: at every stage there is a positive constant equal to the order of the weak transform of 𝓘|_U at every point of the centre. Used by resolveFamExt_mainTheoremIIpp.

theorem Hironaka.Manifold.resolveSeqOn_clause_iii (𝕜 : 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)) (i : Fin (resolveSeqOn bo T U hU).toSuccession.length) : ((resolveSeqOn bo T U hU).toSuccession.boundarySeq (AnalyticManifold.IdealSheaf.restrict T.F.idealSheaf U) i.castSucc).HasOnlyNormalCrossingsWith ((resolveSeqOn bo T U hU).toSuccession.center i)

Clause (iii) of [Hir64, Main Theorem II′(N), p. 156] for the value resolveSeqOn bo T U hU: at every stage the boundary sequence of the restricted boundary ideal sheaf has only normal crossings with the centre; clause (3′) isOfOrderGe_zero_resolveSeqOn read through restrictTriple_F_idealSheaf.

theorem Hironaka.Manifold.resolveSeqOn_boundarySeq_last_hasOnlyNormalCrossings (𝕜 : 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.boundarySeq (AnalyticManifold.IdealSheaf.restrict T.F.idealSheaf U) (Fin.last (resolveSeqOn bo T U hU).toSuccession.length)).HasOnlyNormalCrossings

The first half of clause (iv) for the value: the last boundary has only normal crossings (hasOnlyNormalCrossings_boundarySeq_last_of_isOfOrderGe_zero at isOfOrderGe_zero_resolveSeqOn, through restrictTriple_F_idealSheaf).