The modified first step: the data of the second step at the mark 1, and the local functor

The modified first step of [Wlo09, Theorem 7.4.1] is the second step of [Kol07, Theorem 103] at the mark 1 with two changes of data and nothing else. Its Step 1a "moves the old divisors as before": this is [Kol07, Theorem 103, Step 2.1] on the family data of [Kol07, Lemma 102] from the unmodified marked order reduction one dimension down, bmo (n−1), at the mark 1 (with the modified functor one dimension down the stopped points would stay on the strict transform of an old divisor, against the transversality to the old divisors which [Wlo09, Theorem 2.0.3] promises). Its Step 1b replaces the maximal-contact step at the greatest member by the modified core. The two are the components of one datum of the second step, stepBData : HFData (refl) (tuningParam 1): bd₁ = bdanFamDataOne bmo₁ (the data of [Kol07, Lemma 102], bdanFamDataOfInput, at the single mark 1 = tuningParam 1, tuningParam_one: the input at the mark 1 is the input at the mark 1!), and hf = hFamDataMod R hRo hRc hRi (the modified core as the data of the maximal-contact step at the mark 1). The local functor of the modified first step on the local maximal-contact class is the assembly of the second step at that datum, stated over HFData:

• stepBLocalFunctorFam = hfLocalFunctorFam 1 stepBData, an AnalyticFamilyFunctor (refl) (LocalMCClass 1);
• its three properties: stepBLocalFunctorFam_commutesWithLocalIsos (hfLocalFunctorFam_commutesWithLocalIsos, with the triviality of the family of [Kol07, Lemma 102] at an empty member, BDanFam_eq_nil_of_hyp_eq_empty), stepBLocalFunctorFam_indifferentToEmptyMembers, and stepBLocalFunctorFamOn_isOfOrderGe ([Kol07, Definition 66 (2′)–(4′)] at the mark 1 on each open, hfLocalFunctorFamOn_isOfOrderGe).

The descent from the local class to BOClass 1 is StepBGlobal.lean. The functor one dimension down enters as R with its three properties hRo, hRc, hRi as hypotheses, the unmodified marked order reduction one dimension down as bmo₁.

noncomputable def Hironaka.Manifold.BMOmod.bdanFamDataOne {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo₁ : BMOanFam 𝕜 (n - 1) 1) : BDanFamData (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (IsLocalRing.tuningParam 1)

The family data of [Kol07, Lemma 102] at the mark 1 from the unmodified marked order reduction one dimension down (Step 1a of the modified first step is [Kol07, Theorem 103, Step 2.1] "as before", [Wlo09, Theorem 7.4.1]): bdanFamDataOfInput at the single mark 1 = tuningParam 1, i.e. bdanFam on bmo₁ with its five properties (BDanFam_isOfOrder, BDanFam_compat, BDanFam_cosupp_disjoint, BDanFam_commutesWithLocalIsos, BDanFam_indifferentToEmptyMembers).

Equations

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

theorem Hironaka.Manifold.BMOmod.bdanFamDataOne_fam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo₁ : BMOanFam 𝕜 (n - 1) 1) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass (IsLocalRing.tuningParam 1) T) (j : T.F.ι) : (bdanFamDataOne bmo₁).fam T hT j = BO.bdanFam (IsLocalRing.tuningParam 1) bmo₁ T hT j

theorem Hironaka.Manifold.BMOmod.bdanFamDataOne_fam_eq_nil_of_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bmo₁ : BMOanFam 𝕜 (n - 1) 1) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass (IsLocalRing.tuningParam 1) T) (j : T.F.ι) (hj : T.F.hyp j = ∅) : (bdanFamDataOne bmo₁).fam T hT j = CompatibleFamily.nil T

At an empty member the family of the data at the mark 1 is the trivial one (BDanFam_eq_nil_of_hyp_eq_empty; [Kol07, 32]).

noncomputable def Hironaka.Manifold.BMOmod.stepBData {𝕜 : 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) : HFData (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (IsLocalRing.tuningParam 1)

The datum of the second step for the modified first step at the mark 1 ([Wlo09, Theorem 7.4.1]): the data of [Kol07, Theorem 103, Step 2.1] from the unmodified marked order reduction one dimension down at the mark 1 (bdanFamDataOne), and the modified core as the data of the maximal-contact step (hFamDataMod, at the mark 1 = tuningParam 1).

Equations

• Hironaka.Manifold.BMOmod.stepBData R hRo hRc hRi bmo₁ = { bd₁ := Hironaka.Manifold.BMOmod.bdanFamDataOne bmo₁, hf := Hironaka.Manifold.BMOmod.hFamDataMod R ⋯ ⋯ ⋯ }

theorem Hironaka.Manifold.BMOmod.stepBData_bd₁ {𝕜 : 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) : (stepBData R ⋯ ⋯ ⋯ bmo₁).bd₁ = bdanFamDataOne bmo₁

theorem Hironaka.Manifold.BMOmod.stepBData_hf {𝕜 : 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) : (stepBData R ⋯ ⋯ ⋯ bmo₁).hf = hFamDataMod R ⋯ ⋯ ⋯

noncomputable def Hironaka.Manifold.BMOmod.stepBLocalFunctorFam {𝕜 : 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.LocalMCClass 1

The local functor of the modified first step on the local maximal-contact class at the mark 1: the assembly of the second step (hfLocalFunctorFam) at the modified datum, i.e. the chain of [Kol07, Theorem 103, Step 2.1] from the marked order reduction one dimension down, the triple of Step 2.2 at its last stage, the modified core at the greatest member, read on the lifted range, restricted and cleaned; on each relatively compact open, compatible, without empty centres ([Wlo09, Theorem 7.4.1]).

Equations

• Hironaka.Manifold.BMOmod.stepBLocalFunctorFam R hRo hRc hRi bmo₁ = Hironaka.Manifold.BO.hfLocalFunctorFam 1 (Hironaka.Manifold.BMOmod.stepBData R ⋯ ⋯ ⋯ bmo₁)

theorem Hironaka.Manifold.BMOmod.stepBLocalFunctorFam_fam_seqOn {𝕜 : 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) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hL : Manifold.AnalyticTriple.LocalMCClass 1 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((stepBLocalFunctorFam R ⋯ ⋯ ⋯ bmo₁).fam T hL).seqOn U hU = BO.hfLocalFunctorFamOn 1 (stepBData R ⋯ ⋯ ⋯ bmo₁) T hL U hU

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

[Kol07, Theorem 103 (2)] for the local functor of the modified first step: it commutes with local analytic isomorphisms (hfLocalFunctorFam_commutesWithLocalIsos; the data of Step 2.1 is trivial at an empty member, bdanFamDataOne_fam_eq_nil_of_hyp_eq_empty).

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

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

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

[Kol07, Definition 66 (2′)–(4′)] at the mark 1 on each open for the local functor of the modified first step: the value on U is of order ≥ 1 for the restricted triple (hfLocalFunctorFamOn_isOfOrderGe: the order clause of Step 2.1 and coreModOn_isOfOrderGe of the modified core through [Kol07, Corollary 85]).