Clause (1) of the principalization family: the centres have snc with the boundary

Clause (1) of [Kol07, Theorem 35], per open, for the value on U: every centre of principalizationValue bmo T U hU has simple normal crossings with the total transform of the restricted boundary F|U at its stage ([Kol07, Definition 25] from F|U), in the given codimension.

The route: clause (1) at stage i follows from clause (3′) of [Kol07, Definition 66] at the stages ≤ i — "E_i has only normal crossings with Z_i" for the boundary ideal sheaf E_i = boundarySeq (red F|U) i — by hasSncWith_totalTransformSeqFrom_center_of_forall_lt. Clause (3′) at every stage is the m = 0 instance of IsOfOrderGe (its order half 0 ≤ ord is vacuous), and IsOfOrderGe is available along every piece of the value:

• the disjoining list (its centres have snc with the running total transform in the given codimension, disjoinList_center_hasSncWith; converted to (3′) at each stage by hasOnlyNormalCrossingsWith_boundarySeq_of_forall_hasSncWith);
• the appended order-reduction value: the input family's isOfOrderGe at mark 1 on the disjoined triple, pulled back along the corestricted lift (isOfOrderGe_pullback) and weakened to mark 0; its boundary is the boundary of the disjoining list at its last stage (the junction identity support_comap_liftCorestrict_collapsed: the collapse does not change the support, support_collapse);
• the concatenation (isOfOrderGe_concat) and the deletion of the empty rounds (isOfOrderGe_eraseEmpty; [Kol07, 34.1]).

Clause (3′) alone is IsOfOrderGe at mark 0

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_zero_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (I E₀ : M.IdealSheaf) : S.IsOfOrderGe I 0 E₀ ↔ ∀ (i : Fin S.length), (S.boundarySeq E₀ i.castSucc).HasOnlyNormalCrossingsWith (S.center i)

IsOfOrderGe at mark 0 is clause (3′) at every stage: the order half is vacuous.

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.zero {𝕜 : 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₀) (J : M.IdealSheaf) : S.IsOfOrderGe J 0 E₀

A sequence of order ≥ m is of order ≥ 0 for any marked ideal sheaf (clause (3′) alone).

theorem AnalyticManifold.FiniteSuccession.hasOnlyNormalCrossingsWith_boundarySeq_of_forall_hasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (h1 : ∀ (i : Fin S.length), Manifold.HypersurfaceFamily.HasSncWith ψ (S.totalTransformSeqFrom F i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (k : ℕ) (i : Fin S.length) : ↑i < k → (S.boundarySeq F.idealSheaf i.castSucc).HasOnlyNormalCrossingsWith (S.center i)

If every centre has snc with the running total transform of an snc start F (Kollár's form of clause (1)), then the boundary ideal sheaf starting with red F has only normal crossings with every centre (clause (3′) of [Kol07, Definition 66]) — by induction on the stage, the boundary ideal sheaf at stage i being the reduced ideal sheaf of the total transform there (isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt).

theorem AnalyticManifold.FiniteSuccession.isOfOrderGe_zero_of_forall_hasSncWith {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (h1 : ∀ (i : Fin S.length), Manifold.HypersurfaceFamily.HasSncWith ψ (S.totalTransformSeqFrom F i.castSucc) (Manifold.IdealSheaf.support (S.center i)) (S.codim i)) (J : M.IdealSheaf) : S.IsOfOrderGe J 0 F.idealSheaf

Kollár's clause (1) at every stage gives IsOfOrderGe at mark 0 for the boundary starting with red F.

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_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₂) {I E₀ : M.IdealSheaf} {m : ℕ} (h : L₁.toSuccession.IsOfOrderGe I m E₀) : L₂.toSuccession.IsOfOrderGe I m E₀

Transport of the order clause along an equality of lists.

The disjoining list restricted to U

theorem Hironaka.Manifold.meetLocus_restrictTriple_disjoinBound_eq_empty_of_le {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) {U W : TopologicalSpace.Opens M.carrier} (hW : IsCompact (closure ↑W)) (hUW : U ≤ W) : (restrictTriple T U).F.meetLocus (disjoinBound T W + 1) = ∅

Over the smaller open U ⋐ W the restricted boundary has no (k+1)-fold points for the bound k of W.

theorem Hironaka.Manifold.disjoinListOn_pullback_restrictLE {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) {U W : TopologicalSpace.Opens M.carrier} (hW : IsCompact (closure ↑W)) (hUW : U ≤ W) : (disjoinListOn T W hW).pullback (M.restrictLE hUW) ⋯ = disjoinList (disjoinBound T W) (restrictTriple T U).F ⋯ ⋯

The disjoining list over W, restricted to U ⋐ W, is the disjoining list of the boundary restricted to U, at W's bound (functoriality of the disjoining for open embeddings, [Kol07, 34.1]).

The junction: the appended value's boundary is the disjoining list's boundary

theorem Hironaka.Manifold.support_comap_liftCorestrict_collapsed {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) {U W : TopologicalSpace.Opens M.carrier} (hW : IsCompact (closure ↑W)) (hUW : U ≤ W) : (Manifold.HypersurfaceFamily.comap (⇑((disjoinListOn T W hW).liftCorestrict (M.restrictLE hUW) ⋯)) ((disjoinedTriple (restrictTriple T W) ⋯).pullback (((disjoinListOn T W hW).stage (Fin.last (disjoinListOn T W hW).length)).inclusion ((disjoinListOn T W hW).liftRange (M.restrictLE hUW) ⋯)) ⋯).F).support = (((disjoinListOn T W hW).pullback (M.restrictLE hUW) ⋯).toSuccession.totalTransformSeqFrom (restrictTriple T U).F (Fin.last ((disjoinListOn T W hW).pullback (M.restrictLE hUW) ⋯).toSuccession.length)).support

The boundary of the disjoined triple, restricted to the reading open and pulled back along the corestricted lift, has the support of the total transform of F|U at the last stage of the restricted disjoining list (the collapse keeps the support, support_collapse; the pull-back of a total transform along the lift, totalTransformSeqFrom_last_pullbackLiftLast, as in [Kol07, 30.1]).

Clause (1) for the value

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

The value on U is of order ≥ 0 for the boundary red (F|U) — clause (3′) of [Kol07, Definition 66] at every stage — along the disjoining part (clause (1) of the disjoining in the given codimension), the appended order-reduction value (the input family's isOfOrderGe, weakened), the concatenation and the deletion of the empty rounds.

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

Clause (1) of [Kol07, Theorem 35], per open: every centre of the value on U has snc with the total transform of F|U at its stage, in the given codimension (hasSncWith_totalTransformSeqFrom_center_of_forall_lt from clause (3′) at every stage).