The total transform of 𝓘|_U along the resolution rounds is a normal-crossings divisor

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 pull-back of 𝓘|_U along the composite blow-down is at every point a monomial in the final total transform of the boundary E|_U, and the final boundary is a simple normal crossing family, so the pull-back is the ideal sheaf of a normal-crossings divisor: clause (2) of [Kol07, Theorem 35], clause (3) of [Wlo09, Theorem 2.0.3], [BM97, Theorem 1.10], proved from the fields of the functors bo alone. Round by round the pull-back is Kollár's explicit formula [Kol07, 72] at the round's own mark (Principalization/MonomialSeqMark.lean), with residual the derived triple's ideal; the residual closes at the last round's mark 1.

• isOfOrderGe_zero_resolveFrom: the invariant of the recursion for clause (3′) of [Kol07, Definition 66]: every centre of the rounds has only normal crossings with the boundary sequence from E read along ι (order ≥ 0 for the pulled-back triple). The round's isOfOrderGe weakened to mark 0, isOfOrderGe_concat at mark 0, the boundary at the junction identified through isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt and totalTransformSeqFrom_last_pullbackLiftLast.
• pullbackIsMonomialAtLast_resolveFrom: the total transform of the current ideal along the rounds, read on N along ι, is a boundary monomial at every point of the last stage. The residual identity at mark d + 1 on the pulled-back round list, whose residual is the derived ideal along the last-stage lift (markedTransformSeq_last_pullbackLiftLast), the induction hypothesis on the derived triple, pullbackIsMonomialAtLast_of_isBoundaryMonomialAt and pullbackIsMonomialAtLast_concat; at d = 0 the ideal is the unit ideal and the list is empty.
• isOfOrderGe_zero_resolveSeqOn: clause (3′) for the value (the invariant at the canonical chain, the deletion of the empty rounds by isOfOrderGe_eraseEmpty); the final boundary's normal crossings, in the family form and in the ideal-sheaf form, are each one line from it.
• pullbackIsMonomialAtLast_resolveSeqOn: Kollár's formula [Kol07, 72] for the value.
• resolveSeqOn_comap_last_isNormalCrossingsDivisor: the normal-crossings divisor.
• cosupport_comap_last_resolveSeqOn_subset_boundary: the cosupport of the pull-back lies in the final boundary grown from E|_U.

The glued form on the whole manifold is resolveFamExt_comap_map_isNormalCrossingsDivisor (Hironaka/Resolution/Analytic/BM97/JacobianAssembly.lean), by CompatibleFamily.isNormalCrossingsDivisor_comap_limitBlowDown (Hironaka/Resolution/Analytic/Functor/LimitGluing.lean).

theorem Hironaka.Manifold.isOfOrderGe_zero_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.IsOfOrderGe (cur.pullback ι hι).I 0 (cur.pullback ι hι).F.idealSheaf

The invariant of the recursion resolveFrom for clause (3′) of [Kol07, Definition 66]: every centre of the rounds from d on the current triple cur, read on N along ι, has only normal crossings with the boundary sequence from E, stated as order ≥ 0 for the pulled-back triple, which is clause (3′) alone.

theorem Hironaka.Manifold.pullbackIsMonomialAtLast_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).PullbackIsMonomialAtLast (cur.pullback ι hι).F (cur.pullback ι hι).I

Kollár's formula for the pull-back [Kol07, 72] along the rounds: the total transform of the current ideal along the rounds from d, read on N along ι, is at every point of the last stage a boundary monomial in the final total transform of the boundary. Round by round: the residual identity at the round's mark d + 1 on the pulled-back round list, whose residual at the last stage is the derived triple's ideal pulled back along the last-stage lift; the induction hypothesis on the derived triple; the multiplicativity and the concatenation of PullbackIsMonomialAtLast. At d = 0 the ideal has order 0 everywhere, so it is the unit ideal, and the list is empty. The residual closes at the last round's mark 1 ((bo 1).ord_lt through derivedTriple_ord_le).

theorem Hironaka.Manifold.isOfOrderGe_zero_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.IsOfOrderGe (restrictTriple T U).I 0 (restrictTriple T U).F.idealSheaf

Clause (3′) of [Kol07, Definition 66] for the value resolveSeqOn bo T U hU: it is of order ≥ 0 for (𝓘|_U, 0, red E|_U), the invariant at the canonical chain (AnalyticTriple.pullback_inclusion_restrictLE) and the deletion of the empty rounds (isOfOrderGe_eraseEmpty, [Kol07, 34.1]). The final boundary's normal crossings, in the family form IsSnc of the final total transform and in the ideal-sheaf form HasOnlyNormalCrossings of the boundary sequence (clause (iv) of [Hir64, Main Theorem II′(N), p. 156]), are each one line from it (isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt, hasOnlyNormalCrossings_idealSheaf).

theorem Hironaka.Manifold.pullbackIsMonomialAtLast_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).PullbackIsMonomialAtLast (restrictTriple T U).F (restrictTriple T U).I

Kollár's formula [Kol07, 72] for the value: the pull-back of 𝓘|_U along the composite blow-down of resolveSeqOn bo T U hU is at every point of the last stage a boundary monomial in the final total transform of E|_U (pullbackIsMonomialAtLast_resolveFrom at the canonical chain, the deletion of the empty rounds by pullbackIsMonomialAtLast_eraseEmpty).

theorem Hironaka.Manifold.resolveSeqOn_comap_last_isNormalCrossingsDivisor {𝕜 : 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)) : AnalyticManifold.IdealSheaf.IsNormalCrossingsDivisor (Manifold.IdealSheaf.pullback ⇑((resolveSeqOn bo T U hU).toSuccession.stageMap (Fin.last (resolveSeqOn bo T U hU).toSuccession.length)) ⋯ (restrictTriple T U).I)

The pull-back of 𝓘|_U along the composite blow-down of resolveSeqOn bo T U hU is the ideal sheaf of a normal-crossings divisor ([Kol07, Theorem 35 (2)]; [Wlo09, Theorem 2.0.3 (3)]; [BM97, Theorem 1.10]): a boundary monomial at every point (pullbackIsMonomialAtLast_resolveSeqOn) in the final total transform of E|_U, which is a simple normal crossing family (clause (3′) of the value, at every step), hence isNormalCrossingsDivisor_of_forall_monomial.

theorem Hironaka.Manifold.cosupport_comap_last_resolveSeqOn_subset_boundary {𝕜 : 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)) : (Manifold.IdealSheaf.pullback ⇑((resolveSeqOn bo T U hU).toSuccession.stageMap (Fin.last (resolveSeqOn bo T U hU).toSuccession.length)) ⋯ (restrictTriple T U).I).support ⊆ Manifold.IdealSheaf.support ((resolveSeqOn bo T U hU).toSuccession.boundarySeq (restrictTriple T U).F.idealSheaf (Fin.last (resolveSeqOn bo T U hU).toSuccession.length))

The cosupport of the pull-back of 𝓘|_U along the composite blow-down of resolveSeqOn bo T U hU lies in the final boundary grown from E|_U, boundarySeq (E|_U) (Fin.last _): a point of the cosupport lies on a member of the final total transform through which the monomial of pullbackIsMonomialAtLast_resolveSeqOn has a factor (an empty product is the unit ideal). When E ≠ ∅ this is weaker than Włodarczyk's clause that the total transform is supported on the exceptional divisors ([Wlo09, Theorem 2.0.3 (3)]); the two coincide when E = ∅, the case of the principalization theorem with the Jacobian clause, whose boundary is empty. The exceptional-divisor form would need the boundary monomial in the exceptional sub-family, that is, the descent of clause (3′) to the empty boundary along the sequence; it is not proved in this library. Not used elsewhere in the library.