The exit of the monomial phase, and the composite of the rounds with the monomial phase

The monomial phase (Step2bPhase.lean, Step2bFamily.lean, Step2bFunctor.lean) blows up the positive locus of the top active member until no member is active ([Wlo09, Theorem 7.4.1]; [Wlo09, §6, Step 2b]). This module proves what its value leaves behind, in the two forms which the next step of the modified algorithm (the restriction to a hypersurface of maximal contact) needs ("we arrive at the purely nonmonomial case I′ = N(I′), where max{ord_x(I) : x ∈ supp(I′)} = 1", [Wlo09, Theorem 7.4.1]):

• the first exit property: at the induced triple of the value of the phase no member is active (activeMembers_induced_step2bPhase_eq_empty, activeMembers_induced_step2bFam_eq_empty), since the measure step2bMeasure drops by one per step (step2bMeasure_stepTriple_add_one_le) and at measure 0 no member is active. Hence M(𝓘) = ⊤ (monomialPart_eq_top_of_activeMembers_eq_empty: every component exponent is 0) and N(𝓘) = 𝓘 (nonmonomialTriple_I_eq_of_monomialPart_eq_top, the colon by the unit ideal): "no active member" means "the ideal is its own nonmonomial part".
• the second exit property: the pointwise bound ord N(𝓘) ≤ d survives every step (nonmonomialOrdLe_stepTriple) and the whole phase (nonmonomialOrdLe_induced_step2bPhase). One step is the blow-up of a centre of codimension one, a local analytic isomorphism π (isLocalDiffeomorph_blowUpπ_of_codimOne); N(π^*𝓘) = π^* N(𝓘) (nonmonomialPart_comap, the observation of [Kol07, 111, Step 1]); the ideal after the step is the division of π^*𝓘 by one power of the ideal of the new member (stalkIdeal_stepIdeal; at the stalk π^*𝓘 = 𝓘_{π⁻¹Z} · 𝓘′, stalkIdeal_comap_stepπ_eq_mul, the transform (60.1) of [Kol07, Definition 60] at the mark 1), which the fine nonmonomial part ignores (nonmonomialPart_componentIdeal_pow_mul, the uniqueness of the decomposition of [Kol07, Definition–Lemma 110]). The boundary after the step is stepFamily (the strict transforms and the new member π⁻¹(Z) last) while the pull-back lemmas speak of F.comap π; their fine parts agree pointwise (stalkIdeal_monomialPart_stepFamily_eq): at a point the components through it correspond member by member (stepMemberOf: inl k ↦ k, inr ↦ top; injective on the members through the point, stepMemberOf_injective_of_mem, and onto, exists_mem_stepFamily_of_mem_comap) with equal stalks (stalkIdeal_idealSheaf_stepFamily_eq; over Z the new member and the pulled-back top member have the same stalk, Z being open in E^top, stalkIdeal_idealSheaf_stepFamily_inr_eq) and hence equal exponents; globally nonmonomialPart_stepFamily_eq_comap. No global correspondence of component sets is used.

Together, under the bound 1 on the nonmonomial part of the restricted triple, the triple induced by the value of the phase on every open lies in BOClass 1 (boClass_one_induced_step2bFam).

Then the composite of the rounds with the monomial phase: stepACFunctor, the composeInduced of ComposeInducedFunctor.lean of stepAFunctor at m = 1, t = 2 and step2bFunctor, with the class hypotheses of BMOClass 1 (bmoClass_inducedTriple, bmoClass_classPullbackClosed, bmoClass_classInducedEraseEmptyClosed); its order clause stepACFunctor_isOfOrderGe; and the fact the next step needs, that the triple induced by its value on every open lies in BOClass 1 (boClass_one_induced_stepACFunctor): the terminal bound of the rounds at the value (nonmonomialOrdLe_induced_stepAFamOn: stepAChainState_bound transported along the restriction, induced_pullback and nonmonomialOrdLe_pullback, and the deletion of empty blow-ups, nonmonomialOrdLe_induced_eraseEmpty), the exit of the monomial phase at the induced triple, and the transport of BOClass along the shrinkAppend, restriction and deletion of the composite (boClass_induced_concat_aux, AnalyticFamilyFunctor.boClass_induced_alongList, AnalyticFamilyFunctor.boClass_induced_composeAlong).

The parameters hcomp and hid enter only through the rounds (stepAFunctor, nonmonomialOrdLe_pullback).

theorem Manifold.AnalyticTriple.bmoClass_inducedTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) {m : ℕ} (hT : BMOClass m T) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) : BMOClass m (T.induced s L hL)

The induced triple of a BMOClass m triple along any list of order ≥ s is in BMOClass m: the mark is kept, the nonempty members are finite (finite_nonempty_totalTransformSeqFrom). Named apart from Hironaka.MarkedTriple.bmoClass_induced, its scheme-theoretic counterpart.

theorem Manifold.AnalyticTriple.induced_congr_list {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (P : {N : AnalyticManifold 𝕜 E} → AnalyticTriple ψ₀ N → Prop) (m : ℕ) {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (e : L₁ = L₂) (h₂ : L₂.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (h : P (T.induced m L₂ h₂)) (h₁ : L₁.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : P (T.induced m L₁ h₁)

Substituting an equal inducing list inside a predicate on the induced triple: the two last stages are only propositionally equal, so this is a substitution, not a rewrite.

theorem Hironaka.Manifold.BMOmod.monomialPart_eq_top_of_activeMembers_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (h : activeMembers T = ∅) : BMO.monomialPart T.F ⋯ T.I = ⊤

No active member implies that every component exponent is 0 (ordAlong_eq_zero_of_notMem_positiveLocus, componentExponent_eq_toNat_ordAlongIdeal), hence that the fine monomial part is the unit ideal (stalkIdeal_monomialPart, the product of the factors of the components through the point).

theorem Hironaka.Manifold.BMOmod.nonmonomialTriple_I_eq_of_monomialPart_eq_top {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (h : BMO.monomialPart T.F ⋯ T.I = ⊤) : (BMO.nonmonomialTriple T).I = T.I

M(𝓘) = ⊤ implies N(𝓘) = 𝓘 (the colon by the unit ideal, stalkIdeal_nonmonomialPart).

theorem Hironaka.Manifold.BMOmod.headTriple_stepCenter_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (h₁ : (AnalyticManifold.BlowUpSequence.cons ⋯ (AnalyticManifold.BlowUpSequence.nil (Manifold.blowUp ψ₀ ⋯))).toSuccession.IsOfOrderGe T.I 1 T.F.idealSheaf) : T.headTriple 1 ⋯ h₁ = stepTriple T hfin hne

The head triple of a step of the monomial phase (the induced triple of the one-element list, headTriple of InducedConcat.lean) is the triple after the step: the ideals by headTriple_I and the definition of stepIdeal, the boundaries by headTriple_F and the definition of stepFamily (the centre is the cosupport of its ideal sheaf). The order clause h₁ is a hypothesis here; at the uses it is the head clause of isOfOrderGe_step2bPhase, read off through induced_cons.

theorem Hironaka.Manifold.BMOmod.activeMembers_induced_step2bPhase_eq_empty_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) : step2bMeasure T hT ≤ ↑k → activeMembers (T.induced 1 (step2bPhase k T hT) ⋯) = ∅

The recursion of the first exit property: at a fuel k ≥ step2bMeasure T, the triple induced by the phase has no active member (induction on k with induced_cons and headTriple_stepCenter_eq; the measure is lowered by one per step, step2bMeasure_stepTriple_add_one_le, and at measure 0 no member is active, one_le_step2bMeasure_of_nonempty).

theorem Hironaka.Manifold.BMOmod.activeMembers_induced_step2bPhase_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (k : ℕ) (hk : step2bMeasure T hT ≤ ↑k) : activeMembers (T.induced 1 (step2bPhase k T hT) ⋯) = ∅

The first exit property: at a fuel k ≥ step2bMeasure T, the triple induced by the phase has no active member (induction on k with induced_cons and headTriple_stepCenter_eq; the measure is lowered by one per step, step2bMeasure_stepTriple_add_one_le, and at measure 0 no member is active, one_le_step2bMeasure_of_nonempty).

theorem Hironaka.Manifold.BMOmod.activeMembers_induced_step2bFam_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : activeMembers ((T.pullback (M.inclusion U) ⋯).induced 1 ((step2bFam T hT).seqOn U hU) ⋯) = ∅

The first exit property at the value of the family: the triple induced by the value of step2bFam on U has no active member (step2bFam_seqOn, step2bMeasure_restrict_le_famFuel, activeMembers_induced_step2bPhase_eq_empty).

theorem Hironaka.Manifold.BMOmod.ord_congr_stalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N : AnalyticManifold 𝕜 E} {J₁ J₂ : N.IdealSheaf} {x : N.carrier} (h : Manifold.IdealSheaf.stalkIdeal J₁ x = Manifold.IdealSheaf.stalkIdeal J₂ x) : Manifold.IdealSheaf.ord J₁ x = Manifold.IdealSheaf.ord J₂ x

The pointwise order is a function of the stalk (IdealSheaf.ord J x := IsLocalRing.ord (J.stalkIdeal x)).

theorem Hironaka.Manifold.BMOmod.nonmonomialPart_stalkIdeal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (G : Manifold.HypersurfaceFamily N.carrier) (hG : Manifold.HypersurfaceFamily.IsSnc ψ₀ G) {J₁ J₂ : N.IdealSheaf} (x : N.carrier) (h : Manifold.IdealSheaf.stalkIdeal J₁ x = Manifold.IdealSheaf.stalkIdeal J₂ x) : (BMO.nonmonomialPart G hG J₁).stalkIdeal x = (BMO.nonmonomialPart G hG J₂).stalkIdeal x

For any boundary with simple normal crossings, the stalk of the nonmonomial part at a point depends only on the stalk of the ideal there: the exponents of the components through the point are orders along them at that point (componentExponent_eq_toNat_ordAlongIdeal, ordAlongIdeal_congr_stalk), and the colon is stalkwise (stalkIdeal_nonmonomialPart).

The fine parts for stepFamily and for F.comap π agree stalkwise

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.BMOmod.stepComapFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.HypersurfaceFamily (stepStage T hfin hne).carrier

The pulled-back boundary along the step's blow-down.

Equations

• Hironaka.Manifold.BMOmod.stepComapFamily T hfin hne = Manifold.HypersurfaceFamily.comap (⇑(Hironaka.Manifold.BMOmod.stepπ T hfin hne)) T.F

theorem Hironaka.Manifold.BMOmod.isSnc_stepComapFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (stepComapFamily T hfin hne)

noncomputable def Hironaka.Manifold.BMOmod.stepMemberOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (i : (stepFamily T hfin hne).ι) : T.F.ι

The member of F.comap π a member of stepFamily lies over: inl k ↦ k, inr ↦ top.

Equations

• Hironaka.Manifold.BMOmod.stepMemberOf T hfin hne i = Sum.elim id (fun (x : PUnit.{?u.2 + 1}) => Hironaka.Manifold.BMOmod.topMember T hfin hne) (ofLex i)

theorem Hironaka.Manifold.BMOmod.mem_stepComapFamily_of_mem_stepFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {i : (stepFamily T hfin hne).ι} {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepFamily T hfin hne).hyp i) : x' ∈ (stepComapFamily T hfin hne).hyp (stepMemberOf T hfin hne i)

A point of a member of stepFamily lies on the member of F.comap π it lies over (mem_hyp_of_mem_strictTransform, step2bCenter_subset).

theorem Hironaka.Manifold.BMOmod.stepMemberOf_injective_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {i₁ i₂ : (stepFamily T hfin hne).ι} {x' : (stepStage T hfin hne).carrier} (h₁ : x' ∈ (stepFamily T hfin hne).hyp i₁) (h₂ : x' ∈ (stepFamily T hfin hne).hyp i₂) (h : stepMemberOf T hfin hne i₁ = stepMemberOf T hfin hne i₂) : i₁ = i₂

Two members of stepFamily through a common point over the same member of F coincide: the strict transform of the top member and the new member π⁻¹(Z) never meet (notMem_step2bCenter_of_mem_stepFamily_top).

theorem Hironaka.Manifold.BMOmod.exists_mem_stepFamily_of_mem_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {k : T.F.ι} {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepComapFamily T hfin hne).hyp k) : ∃ (i : (stepFamily T hfin hne).ι), x' ∈ (stepFamily T hfin hne).hyp i ∧ stepMemberOf T hfin hne i = k

Every point of a member of F.comap π lies on a member of stepFamily over it: the other members' strict transforms are their preimages (stepFamily_hyp_inl_of_ne); over the top member, the new member π⁻¹(Z) over Z, the strict transform off Z (stepFamily_hyp_inl_inter_compl).

theorem Hironaka.Manifold.BMOmod.stalkIdeal_idealSheaf_stepFamily_inr_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : (stepπ T hfin hne) x' ∈ step2bCenter T hfin hne) : ⋯.idealSheaf.stalkIdeal x' = ⋯.idealSheaf.stalkIdeal x'

At a point over the centre, the ideal sheaf of the new member π⁻¹(Z) and the ideal sheaf of the pulled-back top member π⁻¹(E^j) have the same stalk: Z is open in E^j (exists_isOpen_inter_subset_positiveLocus), so the two closed hypersurfaces agree near the point (stalkIdeal_idealSheaf_congr_nhds).

theorem Hironaka.Manifold.BMOmod.stalkIdeal_idealSheaf_stepFamily_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {i : (stepFamily T hfin hne).ι} {x' : (stepStage T hfin hne).carrier} (hx' : x' ∈ (stepFamily T hfin hne).hyp i) : ⋯.idealSheaf.stalkIdeal x' = ⋯.idealSheaf.stalkIdeal x'

The ideal sheaves of the members of stepFamily and of F.comap π have the same stalks at a common point: inl k, k ≠ top, by idealSheaf_stepFamily_inl_of_ne; inl top at a point of the strict transform by stalkIdeal_idealSheaf_stepFamily_inl_top; inr by stalkIdeal_idealSheaf_stepFamily_inr_eq; the ideal sheaf of the pulled-back member is the pull-back (comap_idealSheaf_of_isLocalDiffeomorph).

theorem Hironaka.Manifold.BMOmod.stalkIdeal_monomialPart_stepFamily_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (J : (stepStage T hfin hne).IdealSheaf) (x' : (stepStage T hfin hne).carrier) : (BMO.monomialPart (stepFamily T hfin hne) ⋯ J).stalkIdeal x' = (BMO.monomialPart (stepComapFamily T hfin hne) ⋯ J).stalkIdeal x'

The stalks of the fine monomial parts with respect to stepFamily and to F.comap π agree: the components through x' correspond member by member (Finset.prod_bij, as in monomialPart_comap; stepMemberOf is injective on the members through x', stepMemberOf_injective_of_mem, and onto, exists_mem_stepFamily_of_mem_comap); the factors agree by stalkIdeal_idealSheaf_stepFamily_eq through componentIdeal_stalkIdeal_eq, the exponents by componentExponent_eq_toNat_ordAlongIdeal at x' and ordAlongIdeal_congr_stalk_left.

theorem Hironaka.Manifold.BMOmod.stalkIdeal_nonmonomialPart_stepFamily_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (J : (stepStage T hfin hne).IdealSheaf) (x' : (stepStage T hfin hne).carrier) : (BMO.nonmonomialPart (stepFamily T hfin hne) ⋯ J).stalkIdeal x' = (BMO.nonmonomialPart (stepComapFamily T hfin hne) ⋯ J).stalkIdeal x'

theorem Hironaka.Manifold.BMOmod.stalkIdeal_comap_stepπ_eq_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {x' : (stepStage T hfin hne).carrier} (hx' : (stepπ T hfin hne) x' ∈ step2bCenter T hfin hne) : (Manifold.IdealSheaf.pullback ⇑(stepπ T hfin hne) ⋯ T.I).stalkIdeal x' = (BMO.componentIdeal (stepComapFamily T hfin hne) ⋯ ⟨topMember T hfin hne, ConnectedComponents.mk ⟨x', ⋯⟩⟩ ^ 1 * stepIdeal T hfin hne).stalkIdeal x'

At a point over the centre, the pulled-back ideal is the ideal after the step times the ideal of the new member (the transform (60.1) of [Kol07, Definition 60] at the mark 1): stalkIdeal_stepIdeal is the colon by the principal ideal (u) of π⁻¹(Z) (stalkIdeal_idealSheaf_eq_span_singleton, transported by the germ map), (π^*𝓘)_{x'} ⊆ (u) from 𝓘 ⊆ 𝓘_Z along Z (one_le_ordAlong_step2bCenter), and Ideal.span_singleton_mul_colon_of_le recovers the product; the component of the pulled-back top member through x' has the stalk of π⁻¹(Z) there (stalkIdeal_idealSheaf_stepFamily_inr_eq, componentIdeal_stalkIdeal_eq).

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_stepTriple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) {d : ℕ} (h : NonmonomialOrdLe T d) : NonmonomialOrdLe (stepTriple T hfin hne) d

The second exit property for one step: the pointwise bound on the nonmonomial part survives a step of the monomial phase. The blow-down π is a local analytic isomorphism (isLocalDiffeomorph_blowUpπ_of_codimOne), N(π^*𝓘) = π^* N(𝓘) (nonmonomialPart_comap), the ideal after the step is the division of π^*𝓘 by one power of the ideal of the new member (stalkIdeal_stepIdeal, stalkIdeal_comap_stepπ_eq_mul), which N ignores (nonmonomialPart_componentIdeal_pow_mul, the uniqueness of the decomposition of Kol07, Definition–Lemma 110), with the boundary re-indexed by stepFamily pointwise (stalkIdeal_nonmonomialPart_stepFamily_eq). The transform identity of the rounds does not enter here; it is first needed in the composite with the rounds.

theorem Hironaka.Manifold.BMOmod.nonmonomialPart_stepFamily_eq_comap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hfin : (activeMembers T).Finite) (hne : (activeMembers T).Nonempty) (J : (stepStage T hfin hne).IdealSheaf) : BMO.nonmonomialPart (stepFamily T hfin hne) ⋯ J = BMO.nonmonomialPart (Manifold.HypersurfaceFamily.comap (⇑(stepπ T hfin hne)) T.F) ⋯ J

The re-indexing, proved pointwise: the nonmonomial part with respect to the boundary stepFamily after the step (the components of the centre moved to the new member) equals the nonmonomial part with respect to the pulled-back boundary F.comap π; at every point the components through it correspond member by member with the same stalks and exponents, hence the same fine monomial part and the same colon.

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_induced_step2bPhase_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (k : ℕ) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) {d : ℕ} : NonmonomialOrdLe T d → NonmonomialOrdLe (T.induced 1 (step2bPhase k T hT) ⋯) d

The recursion of the second exit property along the phase: the bound survives the phase at every fuel (induction with induced_cons, headTriple_stepCenter_eq and nonmonomialOrdLe_stepTriple).

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_induced_step2bPhase {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (k : ℕ) {d : ℕ} (h : NonmonomialOrdLe T d) : NonmonomialOrdLe (T.induced 1 (step2bPhase k T hT) ⋯) d

The second exit property along the phase: the bound survives the phase at every fuel (induction with induced_cons, headTriple_stepCenter_eq and nonmonomialOrdLe_stepTriple).

theorem Hironaka.Manifold.BMOmod.boClass_one_induced_step2bFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (hN : NonmonomialOrdLe (T.pullback (M.inclusion U) ⋯) 1) : Manifold.AnalyticTriple.BOClass 1 ((T.pullback (M.inclusion U) ⋯).induced 1 ((step2bFam T hT).seqOn U hU) ⋯)

Under the bound 1 on the nonmonomial part of the restricted triple, the triple induced by the value of step2bFam on U is in BOClass 1: the mark; the order (M = ⊤ by the first exit property, N = 𝓘 by nonmonomialTriple_I_eq_of_monomialPart_eq_top, ord N ≤ 1 by the second); and the finiteness (bmoClass_inducedTriple).

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {d : ℕ} (h : NonmonomialOrdLe (T.induced s L hL) d) : NonmonomialOrdLe (T.induced s L.eraseEmpty hLe) d

The pointwise bound on the nonmonomial part at the induced triple survives the deletion of empty blow-ups from the inducing list: the ideals agree through eraseEmptyLast⁻¹ (markedTransformSeq_last_eraseEmpty), the boundary of the induced triple of the cleaned list is an empty extension of the other's (isEmptyExtension_eraseEmptyIdx_induced), which N ignores (nonmonomialPart_eq_of_isEmptyExtension), and N pulls back along the diffeomorphism (nonmonomialPart_comap).

theorem Hironaka.Manifold.BMOmod.boClass_induced_concat_aux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (L' : AnalyticManifold.BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) (m : ℕ) (hL : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (hL' : L'.toSuccession.IsOfOrderGe (T.induced m L hL).I m (T.induced m L hL).F.idealSheaf) (hC : (L.concat L').toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) : Manifold.AnalyticTriple.BOClass m ((T.induced m L hL).induced m L' hL') → Manifold.AnalyticTriple.BOClass m (T.induced m (L.concat L') hC)

The BOClass form of nonmonomialOrdLe_induced_concat, by recursion on the second list.

The class of the induced triple of a composite

theorem Hironaka.Manifold.AnalyticFamilyFunctor.boClass_induced_alongList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hAV : (F.appendValue G s ⋯ ⋯ T hT W hW V hV hVW).toSuccession.IsOfOrderGe ((F.inducedOfFirst s ⋯ T hT W hW).pullback (((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length)).inclusion (F.firstReadOpen T hT W hW V hVW)) ⋯).I s ((F.inducedOfFirst s ⋯ T hT W hW).pullback (((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length)).inclusion (F.firstReadOpen T hT W hW V hVW)) ⋯).F.idealSheaf) (hA : Manifold.AnalyticTriple.BOClass s (((F.inducedOfFirst s ⋯ T hT W hW).pullback (((F.firstList T hT W hW).stage (Fin.last (F.firstList T hT W hW).length)).inclusion (F.firstReadOpen T hT W hW V hVW)) ⋯).induced s (F.appendValue G s ⋯ ⋯ T hT W hW V hV hVW) hAV)) (hAL : (F.alongList G s ⋯ ⋯ T hT W hW V hV hVW).toSuccession.IsOfOrderGe (T.pullback (M.inclusion V) ⋯).I s (T.pullback (M.inclusion V) ⋯).F.idealSheaf) : Manifold.AnalyticTriple.BOClass s ((T.pullback (M.inclusion V) ⋯).induced s (F.alongList G s ⋯ ⋯ T hT W hW V hV hVW) hAL)

The class BOClass s of the triple induced by the list alongList of the link over (W, V), from the class of the triple induced by the appended value (G at the induced triple of the first list of F, restricted to the reading open): the shrinkAppend is a concatenation of the pulled-back first list and the pulled-back appended value (induced_pullback, boClass_classPullbackClosed, boClass_induced_concat_aux), the restricted triple rewritten by pullback_inclusion_restrictLE.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.boClass_induced_composeAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom₁ Dom₂ : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} (F : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₁) (G : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom₂) (s : ℕ) (hF : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), ((F.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) (hFG : ∀ {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)), Dom₂ ((T.pullback (M.inclusion U) ⋯).induced s ((F.fam T hT).seqOn U hU) ⋯)) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (hT : Dom₁ T) (W : TopologicalSpace.Opens M.carrier) (hW : IsCompact (closure ↑W)) (V : TopologicalSpace.Opens M.carrier) (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (U : TopologicalSpace.Opens M.carrier) (hUV : U ≤ V) (hAL : (F.alongList G s ⋯ ⋯ T hT W hW V hV hVW).toSuccession.IsOfOrderGe (T.pullback (M.inclusion V) ⋯).I s (T.pullback (M.inclusion V) ⋯).F.idealSheaf) (hA : Manifold.AnalyticTriple.BOClass s ((T.pullback (M.inclusion V) ⋯).induced s (F.alongList G s ⋯ ⋯ T hT W hW V hV hVW) hAL)) (hC : (F.composeAlong G s ⋯ ⋯ T hT W V hW hV hVW U hUV).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I s (T.pullback (M.inclusion U) ⋯).F.idealSheaf) : Manifold.AnalyticTriple.BOClass s ((T.pullback (M.inclusion U) ⋯).induced s (F.composeAlong G s ⋯ ⋯ T hT W V hW hV hVW U hUV) hC)

The class BOClass s of the triple induced by the value composeAlong of the composite over (W, V) ∋ U, from the class at alongList: the restriction to U (induced_pullback, boClass_classPullbackClosed, pullback_inclusion_restrictLE) and the deletion of the empty blow-ups (boClass_induced_eraseEmpty).

At the standard model: the terminal bound of the rounds at the value, and the composite

theorem Hironaka.Manifold.BMOmod.nonmonomialOrdLe_induced_stepAFamOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : NonmonomialOrdLe ((T.pullback (M.inclusion U) ⋯).induced 1 (stepAFamOn T 1 hT bo ⋯ ⋯ 2 ⋯ ⋯ U hU) ⋯) 1

The terminal bound of the rounds at the value: the nonmonomial part of the triple induced by the value of the rounds on U at m = 1, t = 2 has order ≤ 1 everywhere ("until we drop max ord N(I) to 1", [Wlo09, Theorem 7.4.1]): stepAChainState_bound (the bound at the induced triple of the chain state) transported along the restriction (induced_pullback, nonmonomialOrdLe_pullback) and the deletion of empty blow-ups (nonmonomialOrdLe_induced_eraseEmpty).

noncomputable def Hironaka.Manifold.BMOmod.stepACFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1

The composite of the rounds with the monomial phase: the rounds at m = 1, t = 2, then the monomial phase at the induced triple, as the composeInduced of the two family functors, with the class hypotheses of BMOClass 1 (bmoClass_inducedTriple, bmoClass_classPullbackClosed, bmoClass_classInducedEraseEmptyClosed). This is the modified second step of [Wlo09, Theorem 7.4.1].

Equations

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

theorem Hironaka.Manifold.BMOmod.stepACFunctor_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (((stepACFunctor bo ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 (T.pullback (M.inclusion U) ⋯).F.idealSheaf

The order clause of the composite at the mark 1.

theorem Hironaka.Manifold.BMOmod.boClass_one_induced_stepACFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : Manifold.AnalyticTriple.BOClass 1 ((T.pullback (M.inclusion U) ⋯).induced 1 (((stepACFunctor bo ⋯ ⋯).fam T hT).seqOn U hU) ⋯)

The triple induced by the value of the composite on U is in BOClass 1 (the hypothesis of the next step of the modified algorithm): the value is the shrinkAppend of alongList restricted and cleaned (boClass_induced_composeAlong, boClass_induced_alongList); boClass_one_induced_step2bFam at the induced triple of the first list of the rounds, whose bound on the nonmonomial part is nonmonomialOrdLe_induced_stepAFamOn pulled back to the reading open (nonmonomialOrdLe_pullback).