The family functors of Step 2.2 commute with local analytic isomorphisms

Step 2.3 of the proof of Theorem 103 ([Kol07, 104, Step 2.3]) obtains the functoriality of Step 2.1 "by the corresponding functoriality in (102)", and that of Step 2.2 through the choice of the hypersurface (Theorems 92 and 97). For the family functors of Step 2.2 (Step22Fam.lean), which apply Lemma 102's data at the greatest member of the boundary, the commutation with local analytic isomorphisms (both clauses of [Kol07, 34.1], in the per-open form of AnalyticFamilyFunctor.CommutesWithLocalIsos) comes from the commutation of the data:

• BO.greatestIdx_pullback — the pulled-back triple keeps the index set of the boundary, hence its greatest member;
• HFamData.hstepFunctor_commutesWithLocalIsos, stepHFamFunctor_commutesWithLocalIsos — the family at the greatest member commutes with local analytic isomorphisms because the data do, the member index being kept;
• hfStepH_tuned_pullback_seqOn, BO.stepH_tuned_pullback_seqOn — the value of the data at the re-tuned mark on the tuned pulled-back triple, at its greatest member, is the pull-back of the value on the tuned triple at its greatest member: the tuning commutes with pull-back (tuned_pullback, TunedLemmas.lean) and the greatest member is kept;
• hfStep22Functor_commutesWithLocalIsos — the family functor of Step 2.2 commutes with local analytic isomorphisms.

The hf… declarations are the general forms over data hf : HFamData ψ₀ (tuningParam s) for the hypersurface step (HFamData.lean); the plain forms are their instances at Lemma 102's data. The result enters the transport of the Step 2.2 link along local analytic isomorphisms (Step2LinkPrep.lean).

theorem Hironaka.Manifold.BO.greatestIdx_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {s : ℕ} (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : stepHClass s T) (hT' : stepHClass s (T.pullback g hg)) : greatestIdx hT' = greatestIdx hT

The greatest member of a pulled-back triple of the class stepHClass s is the greatest member of the triple: the pull-back keeps the ordered index set of the boundary, and a linear order has at most one greatest element.

theorem Hironaka.Manifold.HFamData.hstepFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (hf : HFamData ψ₀ s) : hf.hstepFunctor.CommutesWithLocalIsos

The family at the greatest member commutes with local analytic isomorphisms, for data hf for the hypersurface step: the pulled-back triple is the pull-back, its greatest member is the greatest member (greatestIdx_pullback), and the data commute with the member index kept.

theorem Hironaka.Manifold.stepHFamFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd₀ : BDanFamData ψ₀ s) : (BO.stepHFamFunctor bd₀).CommutesWithLocalIsos

Lemma 102's family at the greatest member commutes with local analytic isomorphisms (the functoriality of the application of Lemma 102 in Step 2.2, [Kol07, 104, Step 2.3]): the pulled-back triple is the pull-back, its greatest member is the greatest member (greatestIdx_pullback), and the data of Lemma 102 commute with the member index kept.

theorem Hironaka.Manifold.hfStepH_tuned_pullback_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (hf : HFamData ψ₀ (IsLocalRing.tuningParam s)) (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : BO.stepHClass s T) (hT' : BO.stepHClass s (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : (hf.fam ((T.pullback g hg).tuned s ⋯) ⋯ (BO.greatestIdx ⋯)).seqOn U' hU' = (((hf.fam (T.tuned s ⋯) ⋯ (BO.greatestIdx ⋯)).seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

The value of the data hf at the re-tuned mark on the tuned pulled-back triple, at its greatest member, is the pull-back of the value on the tuned triple at its greatest member, with empty blow-ups deleted ([Kol07, 104, Step 2.3]): the tuning commutes with pull-back (tuned_pullback), the greatest member is kept (greatestIdx_pullback), and the data commute with the member index kept. BO.stepH_tuned_pullback_seqOn is the instance at Lemma 102's data.

theorem Hironaka.Manifold.BO.stepH_tuned_pullback_seqOn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {s : ℕ} (bd : (s : ℕ) → BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT : stepHClass s T) (hT' : stepHClass s (T.pullback g hg)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : ((bd (IsLocalRing.tuningParam s)).fam ((T.pullback g hg).tuned s ⋯) ⋯ (greatestIdx ⋯)).seqOn U' hU' = ((((bd (IsLocalRing.tuningParam s)).fam (T.tuned s ⋯) ⋯ (greatestIdx ⋯)).seqOn (AnalyticMap.imageOpens g hg U') ⋯).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

The value of Lemma 102's data at the re-tuned mark on the tuned pulled-back triple, at its greatest member, is the pull-back of the value on the tuned triple at its greatest member, with empty blow-ups deleted ([Kol07, 104, Step 2.3]): the tuning commutes with pull-back (tuned_pullback), the greatest member is kept (greatestIdx_pullback), and the data commute with the member index kept.

theorem Hironaka.Manifold.hfStep22Functor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} [FiniteDimensional 𝕜 E] (hf : HFamData ψ₀ (IsLocalRing.tuningParam s)) : (hfStep22Functor hf).CommutesWithLocalIsos

The family functor of Step 2.2 over data hf for the hypersurface step commutes with local analytic isomorphisms ([Kol07, 104, Step 2.3]; [Kol07, 34.1]).