The two stop clauses of the modified functor and of the tower; the structure BMOmodFam

The modified marked resolution of [Wlo09, Theorem 7.4.1] at dimension n is the composite of the three phases along induced triples: the rounds on the nonmonomial part and the monomial phase, then the modified first step (modFunctor, ModifiedFam.lean); the tower modTower over all dimensions recurses on n, the recursion of the modified first step on the hypersurface of maximal contact, level 0 being the trivial functor (𝕜⁰ is a point; the case of dimension 0 in [Kol07, 70]). This module proves the two remaining fields of the structure BMOmodFam 𝕜 n, the stopped clause stopped_never_blownUp (the stop rule of the modified first step) and the output clause output_isSmoothSubmanifoldIdeal (the form of the output of [Wlo09, Theorem 7.4.1]), for the composite and for every level of the tower, and assembles the structure: BMOmodFamOfInput_of_hid, the modified marked resolution at every dimension, with the transform identity of the nonmonomial part hid (NonmonomialTransformIdentity, StepARound.lean) as a parameter at every level; concreteBMOmodFam (Hironaka/Resolution/Analytic/Wlo09/Concrete.lean) supplies it as nonmonomialTransformIdentity_refl.

• nilFamilyFunctor_stoppedClauseFam, nilFamilyFunctor_outputClauseFam: the two clauses of the trivial family functor. The stopped clause holds with nothing to check (the empty sequence has no centre); the output clause holds with nothing to check at dimension 0, where the order of every ideal sheaf of a triple is 0 (ord_lt_of_dim_zero). General facts beside nilFamilyFunctor_isOfOrderGe.
• BMOmodFam.ofPre: the structure from a pre-structure BMOmodPre (the order and support clauses of the centres and the two naturality clauses) and the two clauses of its functor (OutputClauseFam, StoppedClauseFam, which are the fields definitionally, ClauseTools.lean).
• modFunctor_stoppedClauseFam, modFunctor_outputClauseFam: the composite's clauses from the stopped clause of the rounds and the monomial phase (stepACFunctor_stoppedClauseFam) and the two clauses of the modified first step (stepBFunctor_stoppedClauseFam, stepBFunctor_outputClauseFam, from the clauses of the functor one dimension down), by the composition lemmas composeInduced_stoppedClauseFam and composeInduced_outputClauseFam (ClauseCompose.lean); the output clause needs the modified first step's only, the last stage of the composite being its.
• modTower_stoppedClauseFam, modTower_outputClauseFam: every level, by induction on n.
• BMOmodFamOfInput_of_hid, BMOmodFamOfInput_of_hid_functor: the structure at every level and its functor (the tower's, by definition).

Sources: the proof of [Wlo09, Theorem 7.4.1] (the modified algorithm, its stop rule, the form of its output and the recursion on the dimension); [Kol07, 70] for dimension 0. The statements themselves are not in the sources.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_stoppedClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} : StoppedClauseFam ψ₀ (nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom)

The stopped clause of the trivial family functor nilFamilyFunctor ("everything is resolved without blow-ups", the case of dimension 0 in [Kol07, 70]): the empty sequence has no centre, so there is nothing to check: the stage bound of the clause reads i + k < 0.

theorem Hironaka.Manifold.AnalyticFamilyFunctor.nilFamilyFunctor_outputClauseFam {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin 0 → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} : OutputClauseFam ψ₀ (nilFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom)

The output clause of the trivial family functor at dimension 0 (the case dim X = 0, I = 𝒪_X, of [Kol07, 70]): on a manifold modelled on 𝕜⁰ the order of the ideal sheaf is 0 at every point (ord_lt_of_dim_zero), so no point of the last stage (the manifold itself) has order ≥ 1 and the clause has nothing to check.

def Hironaka.Manifold.BMOmodFam.ofPre {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (P : BMOmodPre 𝕜 n) (h1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) P.functor) (h8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) P.functor) : BMOmodFam 𝕜 n

The structure from a pre-structure and the two clauses: BMOmodFam 𝕜 n (ModifiedMarkedFam.lean) from BMOmodPre 𝕜 n (the order and support clauses of the centres and the two naturality clauses) and the output clause OutputClauseFam and stopped clause StoppedClauseFam of its functor, which are the fields output_isSmoothSubmanifoldIdeal and stopped_never_blownUp definitionally.

Equations

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

theorem Hironaka.Manifold.BMOmod.modFunctor_stoppedClauseFam {𝕜 : 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 → 𝕜))) (hR8 : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.StoppedClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯)

The stopped clause of the modified functor at dimension n (the stop rule of the modified first step of [Wlo09, Theorem 7.4.1], along the three phases): composeInduced_stoppedClauseFam on the composite of modFunctor from the clause of the rounds and the monomial phase (stepACFunctor_stoppedClauseFam) and that of the modified first step (stepBFunctor_stoppedClauseFam, from the clause hR8 of the functor one dimension down), with the order clause stepBFunctor_isOfOrderGe.

theorem Hironaka.Manifold.BMOmod.modFunctor_outputClauseFam {𝕜 : 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 → 𝕜))) (hR1 : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) R) : AnalyticFamilyFunctor.OutputClauseFam (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (modFunctor R ⋯ ⋯ ⋯ bmo₁ bo ⋯ ⋯)

The output clause of the modified functor at dimension n (the form of the output of [Wlo09, Theorem 7.4.1]): composeInduced_outputClauseFam. The last stage of the composite is the last stage of the run of the modified first step on the induced triple, so only its clause (stepBFunctor_outputClauseFam, from the clause hR1 of the functor one dimension down) enters, with its order clause.

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

The stopped clause of every level of the tower (the recursion on the dimension of [Wlo09, Theorem 7.4.1]): by induction on n; level 0 is the trivial functor (nilFamilyFunctor_stoppedClauseFam), level n + 1 is modFunctor_stoppedClauseFam with the level-n clause as hR8.

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

The output clause of every level of the tower: by induction on n; level 0 is the trivial functor at dimension 0 (nilFamilyFunctor_outputClauseFam), level n + 1 is modFunctor_outputClauseFam with the level-n clause as hR1.

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

The modified marked resolution at every dimension, with the transform identity as a parameter (the proof of [Wlo09, Theorem 7.4.1]): the tower modTower with its two clauses (modTower_outputClauseFam, modTower_stoppedClauseFam) at every level. The parameter hid is the transform identity of the nonmonomial part at every dimension (NonmonomialTransformIdentity); concreteBMOmodFam in Hironaka/Resolution/Analytic/Wlo09/Concrete.lean supplies it as nonmonomialTransformIdentity_refl.

Equations

• Hironaka.Manifold.BMOmod.BMOmodFamOfInput_of_hid 𝕜 bo bmo hid n = Hironaka.Manifold.BMOmodFam.ofPre (Hironaka.Manifold.BMOmod.modTower bo bmo hid n) ⋯ ⋯

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

The functor of the structure at level n is the tower's (by definition).