The value of the monomial procedure on a relatively compact open set

The value of the monomial procedure of [Kol07, 111, Step 3] on a relatively compact open U of a triple T of the class BMOClass m (monomialStep3SeqOn) is the realisation, on M.restrict U, of the combinatorial run from the state of the input piece family of the traces (BMO/Step3Monomial/Input.lean, BMO/Step3Monomial/Realize.lean). Its three properties are stated in the form the interface MonomialStep3Fam of Modified/MonomialStep3Fam.lean reads: no empty centre ([Kol07, 32]); a smooth blow-up sequence of order ≥ m for the monomial part M(𝓘|_U) of the restricted triple with the restricted boundary ([Kol07, Definition 66 (2′)–(4′)]); and order < m of the last marked transform of (M(𝓘|_U), m) at every point ("at the end of Step 3.n we are done"). The realisation's properties are stated for the monomial ideal of the input family, which is the monomial part of the restricted triple (BMO/Step3Monomial/InputMonomial.lean).

noncomputable def Hironaka.Manifold.BMO.monomialStep3SeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (M.restrict U)

The value of the monomial procedure on U: Kollár's Step 3 [Kol07, 111, Step 3] on the traces of the ambient boundary components meeting closure U, read on M.restrict U — the realisation of the combinatorial run from the state of the input family.

Equations

• Hironaka.Manifold.BMO.monomialStep3SeqOn T m hT U hU = (Hironaka.Manifold.BMO.inputFamily T U hU).realize ⋯ ⋯ ⋯

theorem Hironaka.Manifold.BMO.monomialStep3SeqOn_noEmptyCenters {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (monomialStep3SeqOn T m hT U hU).NoEmptyCenters

No centre of the value is empty ([Kol07, 32]): the loci are nonempty by construction.

theorem Hironaka.Manifold.BMO.monomialStep3SeqOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (monomialStep3SeqOn T m hT U hU).toSuccession.IsOfOrderGe (monomialPart (T.pullback (M.inclusion U) ⋯).F ⋯ (T.pullback (M.inclusion U) ⋯).I) m (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The value is a smooth blow-up sequence of order ≥ m for the monomial part of the restricted triple with the restricted boundary ([Kol07, Definition 66 (2′)–(4′)]).

theorem Hironaka.Manifold.BMO.ord_lt_monomialStep3SeqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (m : ℕ) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : ((monomialStep3SeqOn T m hT U hU).toSuccession.stage (Fin.last (monomialStep3SeqOn T m hT U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((monomialStep3SeqOn T m hT U hU).toSuccession.markedTransformSeq (monomialPart (T.pullback (M.inclusion U) ⋯).F ⋯ (T.pullback (M.inclusion U) ⋯).I) m (Fin.last (monomialStep3SeqOn T m hT U hU).toSuccession.length)) x < ↑m

At every point of the last stage the marked transform of (M(𝓘|_U), m) has order < m ([Kol07, 111, Step 3]: "at the end of Step 3.n we are done").