The local functor of Theorem 103 in the compatible-family form: its clauses

The local functor of Steps 1 and 2 of the proof of [Kol07, Theorem 103], in the compatible-family form, is BO.localFunctorFamOn (Step22Fam.lean): on a triple with a global hypersurface of maximal contact and a relatively compact open U, Step 2 at the mark s = tuningParam m on the tuned triple (Step 1), with the hypersurface of maximal contact chosen from the class. This module proves its clauses, each by transporting the clause of Step 2 (Step22FamFull.lean, Step22FamOrdLt.lean, Step2Assembly.lean, Step2AssemblyComm.lean) across the tuning:

• localFunctorFamOn_isOfOrderGe — the value on U is a smooth blow-up sequence of order ≥ m starting with the restricted triple ([Kol07, Definition 66]): the clause of Step 2 at the mark s on the tuned triple, the tuning commuting with the restriction (tuned_pullback), carried back to the mark m by orderReduction_tuned_iff (TunedLemmas.lean);
• localFunctorFamOn_ord_lt — Theorem 103 (1) on U: the order of the final transform is < m, from the clause of Step 2 at the mark s by ord_lt_of_tuned;
• hfLocalFunctorFamOn_commutesWithLocalIsos — Theorem 103 (2), both clauses of [Kol07, 34.1] per open, on the class LocalMCClass m: the tuning commutes with the pull-back, the hypersurface of maximal contact chosen for the pulled-back triple may be replaced by the pull-back of the one chosen for the triple (hfStep2SeqFamOn_indep, FamilyIndependence.lean: Step 2.3 of the proof), and Step 2 commutes with local analytic isomorphisms, given that Lemma 102's data take the empty value at an empty member (hnil);
• hfLocalFunctorFamOn_indifferentToEmptyMembers — the value does not see empty boundary members: the tuning does not see the boundary, and the chosen hypersurface is the same on both sides, the tuned ideal sheaves being equal;
• hfLocalFunctorFamOn_compat — the values are compatible under restriction ([Wlo09, Theorem 2.0.3 (4)]).

Each statement is proved first in the general form hf… over the data HFData ψ₀ s of Step 2 (HFamData.lean: Lemma 102's data for Step 2.1 and the data of the hypersurface step of Step 2.2 at the re-tuned mark), and then stated for Lemma 102's data bd : ∀ s, BDanFamData ψ₀ s as the instance at HFData.ofBDanFamData bd; the general form is what Włodarczyk's modified algorithm (the proof of [Wlo09, Theorem 7.4.1]) uses with its own data for the hypersurface step (Modified/). The clauses are assembled into the order-reduction family in BOanFamOfInput.lean (localFunctorFam, descended by globalizeFam).

theorem Hironaka.Manifold.BO.hfStep2FamOn_congr_triple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (s : ℕ) (d : HFData ψ₀ s) {N : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ N} (e : T₁ = T₂) (h₁ : Manifold.AnalyticTriple.LocalMCClass s T₁) (h₂ : Manifold.AnalyticTriple.LocalMCClass s T₂) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : hfStep2FamOn s d T₁ h₁ U hU = hfStep2FamOn s d T₂ h₂ U hU

Step 2 with the chosen hypersurface of maximal contact depends on the triple only: the proof of membership in the class is irrelevant, the chosen hypersurface being a choice from it (general form over the data HFData of Step 2).

theorem Hironaka.Manifold.hfLocalFunctorFamOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (d : HFData ψ₀ (IsLocalRing.tuningParam m)) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : (BO.hfLocalFunctorFamOn m d T hL U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I m (T.pullback (N.inclusion U) ⋯).F.idealSheaf

The value of the local functor on U is a smooth blow-up sequence of order ≥ m starting with the restricted triple ([Kol07, Definition 66]; the order clause of [Kol07, Theorem 103]), in the general form over the data HFData of Step 2: the clause of Step 2 at the mark s = tuningParam m on the tuned triple (hfStep2SeqFamOn_isOfOrderGe), the tuning commuting with the restriction (tuned_pullback), carried back to the mark m by orderReduction_tuned_iff.

theorem Hironaka.Manifold.localFunctorFamOn_isOfOrderGe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (bd : (s : ℕ) → BDanFamData ψ₀ s) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : (BO.localFunctorFamOn bd m T hL U hU).toSuccession.IsOfOrderGe (T.pullback (N.inclusion U) ⋯).I m (T.pullback (N.inclusion U) ⋯).F.idealSheaf

The value of the local functor on U is a smooth blow-up sequence of order ≥ m starting with the restricted triple ([Kol07, Definition 66]; the order clause of [Kol07, Theorem 103]): the clause of Step 2 at the mark s = tuningParam m on the tuned triple, carried back to the mark m by orderReduction_tuned_iff.

theorem Hironaka.Manifold.localFunctorFamOn_ord_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (bd : (s : ℕ) → BDanFamData ψ₀ s) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) (x : ((BO.localFunctorFamOn bd m T hL U hU).toSuccession.stage (Fin.last (BO.localFunctorFamOn bd m T hL U hU).toSuccession.length)).carrier) : Manifold.IdealSheaf.ord ((BO.localFunctorFamOn bd m T hL U hU).toSuccession.weakTransformSeq (T.pullback (N.inclusion U) ⋯).I (Fin.last (BO.localFunctorFamOn bd m T hL U hU).toSuccession.length)) x < ↑m

Theorem 103 (1) for the value of the local functor on U: the final weak transform of 𝓘|_U has order < m at every point. The clause of Step 2 at the mark s = tuningParam m on the tuned triple (step2SeqFamOn_ord_lt) is carried back to (𝓘, m) by ord_lt_of_tuned.

theorem Hironaka.Manifold.hfLocalFunctorFamOn_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (d : HFData ψ₀ (IsLocalRing.tuningParam m)) (hnil : ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass (IsLocalRing.tuningParam m) T') (j : T'.F.ι), T'.F.hyp j = ∅ → d.bd₁.fam T' hT' j = CompatibleFamily.nil T') {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (hL' : Manifold.AnalyticTriple.LocalMCClass m (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : BO.hfLocalFunctorFamOn m d (T.pullback g hg) hL' U' hU' = ((BO.hfLocalFunctorFamOn m d T hL (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

Theorem 103 (2) for the local functor, both clauses of [Kol07, 34.1] per open, on the class LocalMCClass m, in the general form over the data HFData of Step 2: the tuning commutes with the pull-back (tuned_pullback, passed through the class proof by hfStep2FamOn_congr_triple), the hypersurface of maximal contact chosen for the pulled-back triple is replaced by the pull-back of the one chosen for the triple (hfStep2SeqFamOn_indep, Step 2.3 of the proof of Theorem 103), and Step 2 commutes with local analytic isomorphisms (hfStep2SeqFamOn_commutesWithLocalIsos), given that the data of Step 2.1 take the empty value at an empty member (hnil).

theorem Hironaka.Manifold.hfLocalFunctorFamOn_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (d : HFData ψ₀ (IsLocalRing.tuningParam m)) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (F' : Manifold.HypersurfaceFamily N.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o T.F.ι) (he : ∀ (i : F'.ι), T.F.hyp (e i) = F'.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hL : Manifold.AnalyticTriple.LocalMCClass m T) (hL' : Manifold.AnalyticTriple.LocalMCClass m { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) (U : TopologicalSpace.Opens N.carrier) (hU : IsCompact (closure ↑U)) : BO.hfLocalFunctorFamOn m d T hL U hU = BO.hfLocalFunctorFamOn m d { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hL' U hU

The value of the local functor on U does not see empty boundary members, in the general form over the data HFData of Step 2: the clause of Step 2 on the tuned triples (hfStep2SeqFamOn_indifferentToEmptyMembers); the tuning does not see the boundary, and the chosen hypersurface of maximal contact is the same on both sides, the tuned ideal sheaves being equal.

theorem Hironaka.Manifold.hfLocalFunctorFamOn_compat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} (d : HFData ψ₀ (IsLocalRing.tuningParam m)) {N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ N) (hL : Manifold.AnalyticTriple.LocalMCClass m T) {U V : TopologicalSpace.Opens N.carrier} (hU : IsCompact (closure ↑U)) (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : BO.hfLocalFunctorFamOn m d T hL U hU = ((BO.hfLocalFunctorFamOn m d T hL V hV).pullback (N.restrictLE hUV) ⋯).eraseEmpty

The values of the local functor are compatible under restriction ([Wlo09, Theorem 2.0.3 (4)]; the second clause of [Kol07, 34.1]), in the general form over the data HFData of Step 2: the clause of Step 2 on the tuned triple (hfStep2SeqFamOn_compat).