The modified marked resolution: the functor at dimension n and the tower

The modified marked resolution of [Wlo09, Theorem 7.4.1] runs, on each relatively compact open, three phases in succession, the rounds on the nonmonomial part (stepAFunctor), the monomial phase (step2bFunctor) and the modified first step with the stop rule (stepBFunctor), and recurses on the dimension inside the last (the restriction to the hypersurface H⁺). This module assembles the functor and the tower over the dimension, in the form which carries all the properties of the structure BMOmodFam except the two about the stop predicate (the output is locally the ideal of a smooth submanifold transversal to the boundary, and a point at which this holds off the boundary is never blown up again), which are proved of the tower afterwards:

• stepACFunctor_commutesWithLocalIsos, stepACFunctor_indifferentToEmptyMembers: the two naturality properties of the composite of the rounds with the monomial phase (stepACFunctor of StepCExit.lean), from those of the generic composite (composeInduced_commutesWithLocalIsos, composeInduced_indifferentToEmptyMembers with stepAFunctor_indifferentToEmptyMembers);
• modFunctor R hRo hRc hRi bmo₁ bo hcomp hid : AnalyticFamilyFunctor (refl 𝕜 (Fin n → 𝕜)) (BMOClass 1), the modified functor at dimension n: the composeInduced of stepACFunctor bo hcomp hid (on BMOClass 1) with stepBFunctor R hRo hRc hRi bmo₁ (on BOClass 1), the class transport being boClass_one_induced_stepACFunctor of StepCExit.lean; R is the modified functor one dimension down with its order clause and two naturality properties, bmo₁ the unmodified marked order reduction one dimension down, bo the order reductions at dimension n, hcomp and hid the two facts about the nonmonomial part which the rounds use. Its properties: modFunctor_isOfOrderGe (from composeInduced_isOfOrderGe and stepBFunctor_isOfOrderGe), modFunctor_center_mem_support (the support clause, from the order clause at the mark 1, center_support_subset_of_isOfOrderGe), modFunctor_commutesWithLocalIsos, modFunctor_indifferentToEmptyMembers;
• BMOmodPre 𝕜 n, the structure without the two clauses about the stop predicate: the fields of BMOmodFam 𝕜 n other than output_isSmoothSubmanifoldIdeal and stopped_never_blownUp, with the same types; BMOmodPre.ofModFunctor packages the functor with its four properties; BMOmodPre.zero 𝕜 : BMOmodPre 𝕜 0 is the level 0, 𝕜⁰ a point and the value the empty sequence on every open ("if M is 0-dimensional … all resolutions are trivial", the proof of Wlo09, Theorem 6.0.6): nilFamilyFunctor with its properties, the support clause with no centre to check;
• modTower bo bmo hid : ∀ n, BMOmodPre 𝕜 n, the tower by recursion on n (as towerOf): level 0 is BMOmodPre.zero, level n + 1 is BMOmodPre.ofModFunctor at dimension n + 1 with R the functor of level n and its properties, bmo n, bo (n + 1), nonmonomialComap_inhabitant as hcomp and hid (n + 1); modTower_zero and modTower_succ are its two defining equations, which the inductions for the two remaining clauses unfold.

The transform identity hid : ∀ n, NonmonomialTransformIdentity (refl 𝕜 (Fin n → 𝕜)) is a parameter of the tower, discharged by nonmonomialTransformIdentity_inhabitant when the structure BMOmodFam is assembled. The marked order reduction bmo enters only through the modified first step, the order reductions bo only through the rounds.

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

The structure of the modified marked resolution without the two clauses about the stop predicate: the fields of BMOmodFam 𝕜 n other than output_isSmoothSubmanifoldIdeal and stopped_never_blownUp, i.e. the functor on BMOClass 1 with its order clause, the support clause and the two naturality properties, with the same types. The tower modTower is built in it level by level; the two remaining clauses are proved of the tower afterwards, and the structure BMOmodFam assembles both.

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

  The family functor on the marked class of mark 1 at the standard model 𝕜ⁿ.

• isOfOrderGe {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((self.functor.fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (M.inclusion U) ⋯).I 1 (T.pullback (M.inclusion U) ⋯).F.idealSheaf

  The value on U is a smooth blow-up sequence of order ≥ 1 starting with the restricted (M, 𝓘, 1, E).

• center_mem_support {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin ((self.functor.fam T hT).seqOn U hU).toSuccession.length) : Manifold.IdealSheaf.support (((self.functor.fam T hT).seqOn U hU).toSuccession.center i) ⊆ {x : ↑↧((M.restrict U).finStages ((self.functor.fam T hT).seqOn U hU).toSuccession.later i.castSucc).carrier | 1 ≤ Manifold.IdealSheaf.ord (((self.functor.fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I 1 i.castSucc) x}

  Every centre lies in the support of the current controlled transform.

• commutesWithLocalIsos : self.functor.CommutesWithLocalIsos

  The functor commutes with local analytic isomorphisms.

• indifferentToEmptyMembers : self.functor.IndifferentToEmptyMembers

  The functor is indifferent to empty boundary members.

theorem Hironaka.Manifold.BMOmod.stepACFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (stepACFunctor bo ⋯ ⋯).CommutesWithLocalIsos

The composite of the rounds with the monomial phase commutes with local analytic isomorphisms (composeInduced_commutesWithLocalIsos).

theorem Hironaka.Manifold.BMOmod.stepACFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (stepACFunctor bo ⋯ ⋯).IndifferentToEmptyMembers

The composite of the rounds with the monomial phase is indifferent to empty boundary members (composeInduced_indifferentToEmptyMembers with stepAFunctor_indifferentToEmptyMembers).

noncomputable def Hironaka.Manifold.BMOmod.modFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (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 modified functor at dimension n ([Wlo09, Theorem 7.4.1]: the three phases in succession on each open): the composite along induced triples of the rounds with the monomial phase (stepACFunctor, on BMOClass 1) and of the modified first step (stepBFunctor R hRo hRc hRi bmo₁, on BOClass 1), the class transport being boClass_one_induced_stepACFunctor. R is the modified functor one dimension down (the recursion on the dimension of the modified first step), bo the order reductions at dimension n (the rounds), bmo₁ the unmodified marked order reduction one dimension down (the resolution of Z_{-1} in the modified first step).

Equations

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

theorem Hironaka.Manifold.BMOmod.modFunctor_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (((modFunctor R ⋯ ⋯ ⋯ bmo₁ 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 modified functor: composeInduced_isOfOrderGe with stepBFunctor_isOfOrderGe.

theorem Hironaka.Manifold.BMOmod.modFunctor_center_mem_support {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (i : Fin (((modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.length) : Manifold.IdealSheaf.support ((((modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.center i) ⊆ {x : ↑↧((M.restrict U).finStages (((modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.later i.castSucc).carrier | 1 ≤ Manifold.IdealSheaf.ord ((((modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).fam T hT).seqOn U hU).toSuccession.markedTransformSeq (T.pullback (M.inclusion U) ⋯).I 1 i.castSucc) x}

The support clause of the modified functor, from the order clause at the mark 1 (center_support_subset_of_isOfOrderGe).

theorem Hironaka.Manifold.BMOmod.modFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).CommutesWithLocalIsos

The modified functor commutes with local analytic isomorphisms (composeInduced_commutesWithLocalIsos).

theorem Hironaka.Manifold.BMOmod.modFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯).IndifferentToEmptyMembers

The modified functor is indifferent to empty boundary members (composeInduced_indifferentToEmptyMembers with stepACFunctor_indifferentToEmptyMembers).

noncomputable def Hironaka.Manifold.BMOmod.BMOmodPre.ofModFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) (bmo₁ : BMOanFam 𝕜 (n - 1) 1) (bo : (d : ℕ) → BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : BMOmodPre 𝕜 n

The structure at dimension n from the modified functor and its four properties.

Equations

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

noncomputable def Hironaka.Manifold.BMOmod.BMOmodPre.zero (𝕜 : Type) [RCLike 𝕜] : BMOmodPre 𝕜 0

The level 0: 𝕜⁰ is a point, the recursion bottoms out ("if M is 0-dimensional … all resolutions are trivial", the proof of [Wlo09, Theorem 6.0.6]), and the value is the empty sequence on every open: the trivial functor nilFamilyFunctor with its properties (nilFamilyFunctor_isOfOrderGe, no centres for the support clause, nilFamilyFunctor_commutesWithLocalIsos, nilFamilyFunctor_indifferentToEmptyMembers).

Equations

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

def Hironaka.Manifold.BMOmod.modTower {𝕜 : Type} [RCLike 𝕜] (bo : (n d : ℕ) → BOanFam 𝕜 n d) (bmo : (n : ℕ) → BMOanFam 𝕜 n 1) (hid : ∀ (n : ℕ), NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (n : ℕ) : BMOmodPre 𝕜 n

The tower n ↦ BMOmodPre 𝕜 n (the recursion on the dimension of [Wlo09, Theorem 7.4.1]; as towerOf): level 0 is BMOmodPre.zero, level n + 1 is the modified functor at dimension n + 1 with R the functor of level n (and its properties), bmo n and bo (n + 1); hcomp is nonmonomialComap_inhabitant, hid a parameter at each level.

Equations

• Hironaka.Manifold.BMOmod.modTower bo bmo hid 0 = Hironaka.Manifold.BMOmod.BMOmodPre.zero 𝕜
• Hironaka.Manifold.BMOmod.modTower bo bmo hid n.succ = Hironaka.Manifold.BMOmod.BMOmodPre.ofModFunctor (Hironaka.Manifold.BMOmod.modTower bo bmo hid n).functor ⋯ ⋯ ⋯ (bmo n) (bo (n + 1)) ⋯ ⋯

theorem Hironaka.Manifold.BMOmod.modTower_zero {𝕜 : Type} [RCLike 𝕜] (bo : (n d : ℕ) → BOanFam 𝕜 n d) (bmo : (n : ℕ) → BMOanFam 𝕜 n 1) (hid : ∀ (n : ℕ), NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : modTower bo bmo hid 0 = BMOmodPre.zero 𝕜

The level 0 of the tower.

theorem Hironaka.Manifold.BMOmod.modTower_succ {𝕜 : Type} [RCLike 𝕜] (bo : (n d : ℕ) → BOanFam 𝕜 n d) (bmo : (n : ℕ) → BMOanFam 𝕜 n 1) (hid : ∀ (n : ℕ), NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (n : ℕ) : modTower bo bmo hid (n + 1) = BMOmodPre.ofModFunctor (modTower bo bmo hid n).functor ⋯ ⋯ ⋯ (bmo n) (bo (n + 1)) ⋯ ⋯

The level n + 1 of the tower (the equation which the inductions for the two remaining clauses unfold).