The stopped clause along the chain of Step 2.1

The modified first step of [Wlo09, Theorem 7.4.1] runs Step 1a "as before": the family of the proof of [Kol07, Lemma 102] at the mark 1, read from the unmodified marked order reduction one dimension down (bdanFamDataOne), is applied to the nonempty boundary members in turn along a shrinking chain of relatively compact opens (step21FamAux, hfStep2FamChain; this is [Kol07, Theorem 103, Step 2.1]). The stopped clause of ClauseTools.lean (the field stopped_never_blownUp of BMOmodFam) must hold along that chain. This module proves it.

The core of the proof of [Kol07, Lemma 102] (BDan.coreOfListOf, coreFamOn) blows up Z_{-1} ⊆ Eʲ, then pushes forward the lower run on S_0 = π_{-1}^{-1}(Eʲ); every centre of the pushed-forward run lies in the strict transform of S_0, which is inside the strict transform of the member Eʲ together with the exceptional divisor. So the centres of the core lie in the boundary at every stage, and StoppedClause.of_forall_center_subset_support gives the stopped clause (the predicate of the clause, present for the stop rule, is not needed when the centres lie in the boundary); the deletion of the empty first blow-up keeps the clause (stoppedClause_eraseEmpty).

• exists_hyp_totalTransformSeqFrom_eq_strictTransformSeq, strictTransformSeq_union, strictTransformSeq_hyp_subset_support: the iterated strict transform of a member is a member of the total-transform boundary; that of a union of two sets is the union.
• center_support_subset_cons_of_centersIn: the centres of cons hZ R lie in the boundary when Z lies in a member and the centres of R lie in the strict transforms of a subset of that member's preimage (centersIn_pushforward).
• BDan.coreOfListOf_transformS_stoppedClause, BDan.coreOfListOf_stoppedClause, BDan.coreFamOn_stoppedClause: the stopped clause of the core over a list (through the order clause cons_isOfOrder_of_bridge of the core before the deletion of the empty blow-up), over an arbitrary centre and transform, and per open (the transported value of coreFamOn_eq_coreOfListOf).
• BDanFamData.StoppedClauseFam, BDanFam_stoppedClause, BMOmod.bdanFamDataOne_stoppedClauseFam: the clause for the family data of [Kol07, Lemma 102], for BD^{an}_{n,1,j} on an open (the tuning is the identity at the mark 1, tuned_one, tuned_pullback), and for the data of Step 1a.
• ChainState.link_stoppedClause, step21FamAux_stoppedClause, BO.hfStep2FamChain_stoppedClause: one link keeps the clause (stoppedClause_shrinkAppend), the chain by induction on the member list, and the chain of Step 2.1 at its state over the open M_{n₀+1} of the assembly of Step 2.

Sources: [Kol07, Theorem 103, Step 2.1] and the proof of [Kol07, Lemma 102]; the modified first step of [Wlo09, Theorem 7.4.1]. The statements themselves are not in the sources.

theorem AnalyticManifold.FiniteSuccession.exists_hyp_totalTransformSeqFrom_eq_strictTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (j : F.ι) (i : Fin (S.length + 1)) : ∃ (j' : (S.totalTransformSeqFrom F i).ι), (S.totalTransformSeqFrom F i).hyp j' = S.strictTransformSeq (F.hyp j) i

The strict transforms of a member are members: at every stage the i-fold strict transform of the member F.hyp j is a member of the total-transform boundary (the index toLex (Sum.inl …) iterated; the member of totalTransform at inl is the strict transform of the member, strictTransformSeq_succ).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_union {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (A B : Set M.carrier) (i : Fin (S.length + 1)) : S.strictTransformSeq (A ∪ B) i = S.strictTransformSeq A i ∪ S.strictTransformSeq B i

The iterated strict transform of a union of two sets is the union (closure_union, Set.union_sdiff_distrib, Set.preimage_union at every stage).

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_hyp_subset_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (j : F.ι) (i : Fin (S.length + 1)) : S.strictTransformSeq (F.hyp j) i ⊆ (S.totalTransformSeqFrom F i).support

The iterated strict transform of a member lies in the support of the total-transform boundary (exists_hyp_totalTransformSeqFrom_eq_strictTransformSeq).

theorem AnalyticManifold.FiniteSuccession.center_support_subset_cons_of_centersIn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) (R : (Manifold.blowUp ψ₀ hZ).FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (j : F.ι) (hZj : Z ⊆ F.hyp j) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : S' ⊆ ⇑(Manifold.blowUpπ ψ₀ hZ) ⁻¹' F.hyp j) (hc : R.CentersIn S') (i : Fin (cons ψ₀ hZ R).length) : Manifold.IdealSheaf.support ((cons ψ₀ hZ R).center i) ⊆ ((cons ψ₀ hZ R).totalTransformSeqFrom F i.castSucc).support

The centres of a cons over a push-forward lie in the boundary: for a first centre Z ⊆ F.hyp j and a succession R on its blow-up whose centres lie in the strict transforms of a set S' ⊆ π⁻¹(F.hyp j) (CentersIn, as in centersIn_pushforward), every centre of cons hZ R lies in the support of the total-transform boundary at its stage: at stage 0 by Z ⊆ F.hyp j; at stage k + 1 since π⁻¹(F.hyp j) is the member's strict transform together with the exceptional divisor (cons_totalTransformSeqFromAux_succ, strictTransformSeq_mono, strictTransformSeq_union, strictTransformSeq_hyp_subset_support). This is the hypothesis of StoppedClause.of_forall_center_subset_support.

theorem Hironaka.Manifold.BDan.coreOfListOf_transformS_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hs : s = 1) (hT : BDClass s T) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) ⋯.toAnalyticManifold) (hLne : L.NoEmptyCenters) (hL : L.toSuccession.IsOfOrderGe (restrictedTriple T s j hT).I s (restrictedTriple T s j hT).F.idealSheaf) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (coreOfListOf ⋯ ⋯ L).toSuccession T.I T.F

The stopped clause of the core of [Kol07, Lemma 102] over a list, at the mark 1: the centres of the core before the deletion lie in the boundary (center_support_subset_cons_of_centersIn with Z_{-1} ⊆ Eʲ and S_0 = π_{-1}^{-1}(Eʲ), centersIn_pushforward through pushforwardBridge), so StoppedClause.of_forall_center_subset_support gives the clause (its predicate, present for the stop rule, is not needed once the centres lie in the boundary), and stoppedClause_eraseEmpty carries it through the deletion of the empty first blow-up (the order clause cons_isOfOrder_of_bridge).

theorem Hironaka.Manifold.BDan.coreOfListOf_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {Z : Set M.carrier} (hZ : Manifold.IsClosedSubmanifold ψ₀ Z 1) {S' : Set (Manifold.blowUp ψ₀ hZ).carrier} (hS' : Manifold.IsClosedSubmanifold ψ₀ S' 1) (hs : s = 1) (hT : BDClass s T) (hZeq : Z = BD.Zminus1 T.I s (T.F.hyp j)) (hSeq : S' = transformSOf T j hZ) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) hS'.toAnalyticManifold) (hLne : L.NoEmptyCenters) (hL : L.toSuccession.IsOfOrderGe (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).I s (restrictedTripleOf T s j hZ hS' hT hZeq hSeq).F.idealSheaf) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (coreOfListOf hZ hS' L).toSuccession T.I T.F

coreOfListOf_transformS_stoppedClause over an arbitrary centre and transform (a substitution, as in coreOfListOf_isOfOrderGe).

theorem Hironaka.Manifold.BDan.coreFamOn_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hs : s = 1) (inp : BMOanFam 𝕜 (n - 1) s) (hT : BDClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hT' : BDClass s (T.pullback (M.inclusion U) ⋯)) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (coreFamOn T s j inp hT U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of the per-open core, at the mark 1: the per-open core is the core over the transported value on the restricted data (coreFamOn_eq_coreOfListOf), so coreOfListOf_stoppedClause applies with the transported value's order clause (isOfOrderGe_transportedValue), as in coreFamOn_isOfOrderGe.

def Hironaka.Manifold.BDanFamData.StoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) : Prop

The stopped clause for the family data of [Kol07, Lemma 102] (the field stopped_never_blownUp of BMOmodFam per triple, member and relatively compact open, in the form of the data's own clauses).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.BDanFam_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (hm : m = 1) (inp : BMOanFam 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (BDanFam m inp T hT j U hU).toSuccession (T.pullback (M.inclusion U) ⋯).I (T.pullback (M.inclusion U) ⋯).F

The stopped clause of BD^{an}_{n,1,j} on an open: the core's clause at the mark 1! = 1 on the tuned triple (coreFamOn_stoppedClause with bdClass_tuned_pullback_inclusion), the tuning commuting with the restriction (tuned_pullback) and being the identity at the mark 1 (tuned_one), as in BDanFam_isOfOrder.

theorem Hironaka.Manifold.BMOmod.bdanFamDataOne_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo₁ : BMOanFam 𝕜 (n - 1) 1) : (bdanFamDataOne bmo₁).StoppedClauseFam

The stopped clause of the data of Step 1a (the family of [Kol07, Lemma 102] at the mark 1 from the unmodified marked order reduction one dimension down, bdanFamDataOne): BDanFam_stoppedClause at m = tuningParam 1 = 1.

theorem Hironaka.Manifold.ChainState.link_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hs : s = 1) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) (j : T.F.ι) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hbd : bd.StoppedClauseFam) (hst : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ st.L.toSuccession (T.pullback (M.inclusion W) ⋯).I (T.pullback (M.inclusion W) ⋯).F) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (link T s bd hT st j hV hVW).L.toSuccession (T.pullback (M.inclusion V) ⋯).I (T.pullback (M.inclusion V) ⋯).F

One link of the chain of Step 2.1 keeps the stopped clause (the analogue of the order clause of ChainState.link): the member's value on the induced triple at the lifted range has the clause by the data's clause, the list so far by hypothesis, and stoppedClause_shrinkAppend composes them; the restricted triple is rewritten by pullback_inclusion_restrictLE.

theorem Hironaka.Manifold.step21FamAux_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hs : s = 1) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (r : ℕ) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hbd : bd.StoppedClauseFam) (l : List T.F.ι) (hl : l.length ≤ r) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (step21FamAux T s bd hT W r hW hWsub l hl).L.toSuccession (T.pullback (M.inclusion (W l.length)) ⋯).I (T.pullback (M.inclusion (W l.length)) ⋯).F

The stopped clause along the chain of Step 2.1 (induction on the member list): the initial state is the empty list, each link is ChainState.link_stoppedClause.

theorem Hironaka.Manifold.BO.hfStep2FamChain_stoppedClause {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hs : s = 1) (d : HFData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hbd : d.bd₁.StoppedClauseFam) : AnalyticManifold.FiniteSuccession.StoppedClause ψ₀ (hfStep2FamChain T s d hT U hU).L.toSuccession (T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).I (T.pullback (M.inclusion (step2OpenW T s hT U hU)) ⋯).F

The stopped clause of the chain of Step 2.1 in the assembly of Step 2, at its state over the open M_{n₀+1} (step21FamAux_stoppedClause at the canonical chain of hfStep2FamChain, from the clause of the data d.bd₁).