The monomial phase as a family functor: commutation and indifference

The monomial phase (step2bFam, Step2bFamily.lean) packaged as a family functor on the marked class BMOClass 1 (AnalyticFamilyFunctor), with the two properties on each open that the assembly of the modified algorithm asks of it:

• step2bFunctor_commutesWithLocalIsos, the two conditions of [Kol07, 34.1] in one clause per open (the functoriality of [Wlo09, Theorem 2.0.2 (4)]): for a local analytic isomorphism g : N → M and a triple T' carrying the pull-back data of T, the value on a relatively compact U' ⊆ N is the pull-back along g|_{U'} : U' → g(U') of the value on g(U'), with the empty blow-ups deleted. This is step2bPhase_pullback_eraseEmpty applied to the restricted triple T|_{g(U')} and the restricted map g|_{U'}, the two restrictions composing to the restriction of T' to U' (pullback_pullback), the fuels reconciled as in the compatibility of step2bFam.
• step2bFunctor_indifferentToEmptyMembers, the counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], on each open: deleting empty boundary members does not change any value. The restricted boundaries differ by an empty extension (IsEmptyExtension), the phase is indifferent to it at equal fuel (step2bPhase_eq_of_isEmptyExtension, Step2bEmpty.lean), and the two fuels give the same complete phase (step2bPhase_eq_of_step2bMeasure_le'; the measure of the smaller boundary is at most the measure of the larger, step2bMeasure_le_of_isEmptyExtension).

The module ends with the support clause: the centres of the phase lie in the support of the current controlled transform, as [Wlo09, Definition 3.2.4 (1)] requires of a multiple test blow-up.

noncomputable def Hironaka.Manifold.BMOmod.step2bFunctor {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ₀ : E ≃L[𝕜] Fin n → 𝕜) : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Manifold.AnalyticTriple.BMOClass 1

The monomial phase as a family functor on the marked class BMOClass 1: the compatible family step2bFam for every triple of the class.

Equations

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

theorem Hironaka.Manifold.BMOmod.step2bFunctor_fam {𝕜 : 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) : (step2bFunctor ψ₀).fam T hT = step2bFam T hT

theorem Hironaka.Manifold.BMOmod.step2bFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : (step2bFunctor ψ₀).CommutesWithLocalIsos

[Kol07, 34.1] (the functoriality of [Wlo09, Theorem 2.0.2 (4)]), on each open: the monomial phase commutes with local analytic isomorphisms, by step2bPhase_pullback_eraseEmpty on the restricted triple along the restricted map, the restriction of the pull-back being the pull-back of the restriction.

theorem Hironaka.Manifold.BMOmod.step2bFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} : (step2bFunctor ψ₀).IndifferentToEmptyMembers

The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], on each open: the monomial phase is indifferent to empty boundary members. The restricted boundaries differ by an empty extension, the phase is indifferent to it at equal fuel, and the two fuels give the same complete phase.

The support clause from the order clause

theorem Hironaka.Manifold.BMOmod.ordAlongIdeal_le_ord_of_mem_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (D J : M.IdealSheaf) {a : M.carrier} (ha : a ∈ Manifold.IdealSheaf.support D) : Manifold.IdealSheaf.ordAlongIdeal D J a ≤ Manifold.IdealSheaf.ord J a

The order of J along any centre D at a point of the support of D is at most the order of J there: D_a ≠ 𝒪_a lies in the maximal ideal, so J_a ⊆ D_a^p ⊆ 𝔪_a^p (the general form of ordAlong_le_ord).

theorem Hironaka.Manifold.BMOmod.center_support_subset_of_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hS : S.IsOfOrderGe I m E₀) (hm : 1 ≤ m) (i : Fin S.length) : Manifold.IdealSheaf.support (S.center i) ⊆ {x : ↑↧(M.finStages S.later i.castSucc).carrier | 1 ≤ Manifold.IdealSheaf.ord (S.markedTransformSeq I m i.castSucc) x}

The support clause of [Wlo09, Definition 3.2.4 (1)] ("C_i ⊂ supp(M_i, Z_i, I_i, E_i, µ)") from the order clause of [Kol07, Definition 66]: the centres of a sequence of order ≥ m ≥ 1 lie in the support {x | 1 ≤ ord_x 𝓘_i} of the current marked transform.

theorem Hironaka.Manifold.BMOmod.step2bFam_center_mem_support {𝕜 : 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)) (i : Fin ((step2bFam T hT).seqOn U hU).toSuccession.length) : Manifold.IdealSheaf.support (((step2bFam T hT).seqOn U hU).toSuccession.center i) ⊆ {x : ↑↧((M.restrict U).finStages ((step2bFam T hT).seqOn U hU).toSuccession.later i.castSucc).carrier | 1 ≤ Manifold.IdealSheaf.ord (((step2bFam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I 1 i.castSucc) x}

The support clause of [Wlo09, Definition 3.2.4 (1)] at µ = 1 for the monomial phase: every centre of the phase lies in the support of the current controlled transform.