The modified first step: the functor on BOClass 1

The third step of [Kol07, Theorem 103] at the level of families ("argue as in (37)", the descent along a finite shrunk cover by hypersurfaces of maximal contact, globalizeFam) extends the local functor of the modified first step (stepBLocalFunctorFam, StepBLocal.lean) from the local maximal-contact class to the whole of BOClass 1, exactly as BOanFamOfInputOf extends Kollár's local functor, with the same three properties descended on each open: the commutation with local analytic isomorphisms of the descent (globalizeFam_commutesWithLocalIsos), the order clause (isOfOrderGe_of_agreeFam) and the indifference to empty boundary members (indifferentToEmptyMembers_of_agreeFam). There is no clause bounding the order at the end: on the stopped components the modified run keeps the order at 1 ("the algorithm is stopped", [Wlo09, Theorem 7.4.1]); the output of the modified algorithm is described instead by the clause that the controlled transform is locally the ideal of a smooth submanifold transversal to the boundary.

• stepBFunctor R hRo hRc hRi bmo₁ : AnalyticFamilyFunctor (refl) (BOClass 1);
• stepBFunctor_commutesWithLocalIsos, stepBFunctor_isOfOrderGe, stepBFunctor_indifferentToEmptyMembers; stepBFunctor_fam_eq (the descent agrees with the local functor on the local class).

The composite on each open with the rounds and the monomial phase, the tower over n and the assembled structure are in ModifiedFam.lean.

noncomputable def Hironaka.Manifold.BMOmod.stepBFunctor {𝕜 : 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) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BOClass 1

The functor of the modified first step on the class of BO_{n,1} ([Wlo09, Theorem 7.4.1]; [Kol07, Theorem 103, Step 3]): the descent of the local functor along a finite shrunk cover by hypersurfaces of maximal contact, on each open.

Equations

• Hironaka.Manifold.BMOmod.stepBFunctor R hRo hRc hRi bmo₁ = (Hironaka.Manifold.BMOmod.stepBLocalFunctorFam R ⋯ ⋯ ⋯ bmo₁).globalizeFam ⋯

theorem Hironaka.Manifold.BMOmod.stepBFunctor_fam_eq {𝕜 : 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) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) : (stepBFunctor R ⋯ ⋯ ⋯ bmo₁).fam T ⋯ = (stepBLocalFunctorFam R ⋯ ⋯ ⋯ bmo₁).fam T hL

The descent agrees with the local functor on the local maximal-contact class (globalizeFam_fam_eq).

theorem Hironaka.Manifold.BMOmod.stepBFunctor_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) : (stepBFunctor R ⋯ ⋯ ⋯ bmo₁).CommutesWithLocalIsos

[Kol07, Theorem 103 (2)] for the functor of the modified first step: the descent commutes with local analytic isomorphisms (globalizeFam_commutesWithLocalIsos).

theorem Hironaka.Manifold.BMOmod.stepBFunctor_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) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) N) (hT : Manifold.AnalyticTriple.BOClass 1 T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : (((stepBFunctor R ⋯ ⋯ ⋯ bmo₁).fam T hT).seqOn U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I 1 (T.pullback (N.inclusion U) ⋯).F.idealSheaf

[Kol07, Definition 66 (2′)–(4′)] at the mark 1 on each open for the functor of the modified first step: the local clause stepBLocalFunctorFamOn_isOfOrderGe descended (isOfOrderGe_of_agreeFam).

theorem Hironaka.Manifold.BMOmod.stepBFunctor_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) : (stepBFunctor R ⋯ ⋯ ⋯ bmo₁).IndifferentToEmptyMembers

The counterpart, for boundary members, of the empty blow-up convention [Kol07, 32], for the functor of the modified first step: the descended indifference to empty boundary members (indifferentToEmptyMembers_of_agreeFam).