The monomial procedure as an interface: MonomialStep3Fam

The last step of Kollár's proof of the marked order reduction theorem [Kol07, Theorem 107] is the monomial procedure [Kol07, 111, Step 3]: with E = ∪ Eʲ a simple normal crossing divisor with ordered index set and M(I) = 𝒪(−∑ aⱼ Eʲ) the monomial part of I, it blows up, in an order dictated by the indices, the intersections of members along which the sum of the coefficients is at least m, until every such sum is below m ("at the end of Step 3.n we are done" [Kol07, 111, Step 3]).

This module states the properties of that procedure which the assembly of the theorem on an analytic manifold uses, as a structure MonomialStep3Fam 𝕜 n m: a family functor on the marked class BMOClass m at the standard model Fin n → 𝕜 whose value on a relatively compact open U is a smooth blow-up sequence of order ≥ m for (M(𝓘|U), m) [Kol07, Definition 66 (2′)–(4′)], whose last marked transform of (M(𝓘|U), m) has order < m at every point, and which commutes with local analytic isomorphisms [Kol07, Theorem 107 (2)] and is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]). The monomial part is the fine one, Hironaka.Manifold.BMO.monomialPart, the product over the connected components of the boundary members.

The structure is inhabited by Hironaka.Manifold.BMO.monomialStep3Fam, which realises the combinatorial run Hironaka.Monomial.MonomialState.step3 on the piece families of the boundary; the assembly (SState.step3Link) takes an arbitrary inhabitant as a parameter. This module holds only the structure, so that both sides can import it.

structure Hironaka.Manifold.BMO.MonomialStep3Fam (𝕜 : Type) [RCLike 𝕜] (n m : ℕ) : Type (u + 1)

The monomial procedure in family form. A family functor on the marked class BMOClass m at the standard model whose values are read on the fine monomial part M(𝓘) = monomialPart T.F T.isSnc T.I of the restricted triple in place of 𝓘: on a relatively compact open U the value is a smooth blow-up sequence of order ≥ m for (M(𝓘|U), m), the marked transform of (M(𝓘|U), m) at its last stage has order < m at every point (the exit condition of the procedure, [Kol07, 111, Step 3]), and the functor commutes with local analytic isomorphisms [Kol07, Theorem 107 (2)] and is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]).

In the assembly of the theorem the procedure runs on (M(𝓘), m, E) on the whole last stage of the separation step, and clause (1) of the theorem for 𝓘 itself follows in SState.step3Link_ord_lt.

• functor : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BMOClass m

  The family functor of the monomial procedure on the marked class at the standard model.

• isOfOrderGe {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((self.functor.fam T hT).seqOn 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

  On every relatively compact open U the value is a smooth blow-up sequence of order ≥ m for the monomial part of the restricted triple, with respect to its boundary [Kol07, Definition 66 (2′)–(4′)].

• ord_lt {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (x : (((self.functor.fam T hT).seqOn U hU).toSuccession.stage (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (((self.functor.fam T hT).seqOn U hU).toSuccession.markedTransformSeq (monomialPart (T.pullback (M.inclusion U) ⋯).F ⋯ (T.pullback (M.inclusion U) ⋯).I) m (Fin.last ((self.functor.fam T hT).seqOn U hU).toSuccession.length)) x < ↑m

  The exit condition of the monomial procedure ("at the end of Step 3.n we are done", [Kol07, 111, Step 3]): the marked transform of (M(𝓘|U), m) at the last stage of the value over U has order < m at every point.

• commutesWithLocalIsos : self.functor.CommutesWithLocalIsos

  The functor commutes with local analytic isomorphisms [Kol07, Theorem 107 (2)].

• indifferentToEmptyMembers : self.functor.IndifferentToEmptyMembers

  The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32]: deleting or adding empty members of the boundary does not change the value.