Step 2 on an open: commutation with local analytic isomorphisms and indifference to empty members

The two remaining clauses of Theorem 103 for the value of Step 2 on a relatively compact open (step2SeqFamOn, Step22Fam.lean), proved as for Step 2.1 (Step21FamIndep.lean, Step21FamIndiff.lean) with the link of Step 2.2 transported by hfStep22Link_rel (Step2LinkTransport.lean):

• hfStep2SeqFamOn_commutesWithLocalIsos — along a local analytic isomorphism g : N → M, Step 2 of the pulled-back triple on U' is the pull-back of Step 2 on g(U') with its empty blow-ups deleted, the analytic form of the functoriality clause of Step 2.3 of the proof of Theorem 103 ([Kol07, 104, Step 2.3]; the second clause of [Kol07, 34.1]). The chain of Step 2.1 over N for the members that stay nonempty is the chain over the full list of members along opens carried into the canonical chain of g(U') (step21FamAux_filter_rel; a member emptied by g contributes nothing, which needs the hypothesis hnil that the data are trivial at an empty member), and that chain is the pull-back of the canonical chain of g(U') link by link (step21FamAux_rel_along); the link of Step 2.2 is compared on N through the state over the intersection (hfStep22Link_rel along the identity) and transported along g (hfStep22Link_rel along g).
• hfStep2SeqFamOn_indifferentToEmptyMembers — deleting empty members of the boundary does not change the value ([Kol07, 32]): the chains of Step 2.1 for (M, 𝓘, E) and (M, 𝓘, F') agree on the intersection of the next-to-last opens (step21FamAux_indiff_rel), and the triples of Step 2.2 over the same sequence for two triples with the same ideal sheaf are the same triple (step22TripleOf_congr_I: the triple of Step 2.2 does not see the boundary), so the two links of Step 2.2 agree (hfStep22Link_indiff_I).

The hf… declarations are the general forms over data d : HFData ψ₀ s of Step 2 (HFamData.lean); the plain forms are their instances at Lemma 102's data. These are the clauses commutesWithLocalIsos and indifferentToEmptyMembers of the family structure BOanFam for the local functor (LocalFunctorFam.lean).

theorem Hironaka.Manifold.BO.step22TripleOf_eq_mk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) {H : Set X.carrier} (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : step22TripleOf T L hL hsnc = { I := L.toSuccession.markedTransformSeq T.I s (Fin.last L.toSuccession.length), isNonzeroEverywhere := ⋯, F := (exceptionalOf L).append (transformHOf L H), isSnc := hsnc }

The triple of Step 2.2 over a sequence, written as a structure literal (one unfolding; kept separate so that two triples of Step 2.2 with different boundaries are compared through their ideal sheaves rather than field by field).

theorem Hironaka.Manifold.BO.step22Mk_congr_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} {J₁ J₂ : X.IdealSheaf} (hJ : J₁ = J₂) (L : AnalyticManifold.BlowUpSequence ψ₀ X) {H : Set X.carrier} (p₁ : Manifold.IdealSheaf.IsNonzeroEverywhere (L.toSuccession.markedTransformSeq J₁ s (Fin.last L.toSuccession.length))) (p₂ : Manifold.IdealSheaf.IsNonzeroEverywhere (L.toSuccession.markedTransformSeq J₂ s (Fin.last L.toSuccession.length))) (hsnc₁ hsnc₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : { I := L.toSuccession.markedTransformSeq J₁ s (Fin.last L.toSuccession.length), isNonzeroEverywhere := p₁, F := (exceptionalOf L).append (transformHOf L H), isSnc := hsnc₁ } = { I := L.toSuccession.markedTransformSeq J₂ s (Fin.last L.toSuccession.length), isNonzeroEverywhere := p₂, F := (exceptionalOf L).append (transformHOf L H), isSnc := hsnc₂ }

Two triples of the shape of Step 2.2 over the same sequence with equal ideal sheaves are equal.

theorem Hironaka.Manifold.BO.step22TripleOf_congr_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ X} (hI : T₁.I = T₂.I) {H : Set X.carrier} (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL₁ : L.toSuccession.IsOfOrderGe T₁.I s T₁.F.idealSheaf) (hL₂ : L.toSuccession.IsOfOrderGe T₂.I s T₂.F.idealSheaf) (hsnc₁ hsnc₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : step22TripleOf T₁ L hL₁ hsnc₁ = step22TripleOf T₂ L hL₂ hsnc₂

The triple of Step 2.2 over a sequence depends on the triple only through its ideal sheaf (through the structure literals, so that only the ideal sheaves are compared).

theorem Hironaka.Manifold.BO.hfStep22Link_indiff_I {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {X : AnalyticManifold 𝕜 E} (T₁ T₂ : Manifold.AnalyticTriple ψ₀ X) (hI : T₂.I = T₁.I) (hT₁ : Manifold.AnalyticTriple.BOClass s T₁) (hT₂ : Manifold.AnalyticTriple.BOClass s T₂) {H : Set X.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle₁ : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T₁.I (s - 1)) (hle₂ : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T₂.I (s - 1)) {W : TopologicalSpace.Opens X.carrier} (st : ChainState T₁ s W) (st' : ChainState T₂ s W) (hL : st.L = st'.L) {V : TopologicalSpace.Opens X.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : st.L.shrinkAppend (X.restrictLE ⋯) ⋯ (hfStep22ValueOf d T₁ hT₁ hH hle₁ st hV hVW) = st'.L.shrinkAppend (X.restrictLE ⋯) ⋯ (hfStep22ValueOf d T₂ hT₂ hH hle₂ st' hV hVW)

The link of Step 2.2 does not see the boundary (over data d): two states of the chain with the same sequence, for triples with the same ideal sheaf, append the same value of Step 2.2, since the triple of Step 2.2 over a sequence depends on the triple only through its ideal sheaf (step22TripleOf_congr_I).

theorem Hironaka.Manifold.BO.hfStep2SeqFamAlong_indiff_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (F' : Manifold.HypersurfaceFamily M.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 = ∅) (hT' : Manifold.AnalyticTriple.BOClass s (BDan.withBoundary T F' hsnc')) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (W' : ℕ → TopologicalSpace.Opens M.carrier) (hWsub' : ∀ k < memberCount (BDan.withBoundary T F' hsnc') s hT' + 1, closure ↑(W' (k + 1)) ⊆ ↑(W' k)) (hW' : ∀ (k : ℕ), IsCompact (closure ↑(W' k))) (U : TopologicalSpace.Opens M.carrier) (hU₁ : U ≤ W (memberCount T s hT + 1)) (hU₂ : U ≤ W' (memberCount (BDan.withBoundary T F' hsnc') s hT' + 1)) : hfStep2SeqFamAlong T s hT W hWsub d hW hH hle U hU₁ = hfStep2SeqFamAlong (BDan.withBoundary T F' hsnc') s hT' W' hWsub' d hW' hH hle U hU₂

Step 2 along an admissible chain for (M, 𝓘, E) and Step 2 along an admissible chain for (M, 𝓘, F'), where F' is E with empty members deleted, agree on every common open ([Kol07, 32]; over data d): the chains of Step 2.1 agree on the intersection of the next-to-last opens (step21FamAux_indiff_rel), the links of Step 2.2 through the states over that intersection are the same (hfStep22Link_indiff_I: the triple of Step 2.2 does not see the boundary), and the two links transport to the intersection of the last opens (hfStep22Link_rel along the identity).

theorem Hironaka.Manifold.hfStep2SeqFamOn_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (F' : Manifold.HypersurfaceFamily M.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 = ∅) (hT' : Manifold.AnalyticTriple.BOClass s { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) : BO.hfStep2SeqFamOn T s d hT U hU hH hle = BO.hfStep2SeqFamOn { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } s d hT' U hU hH hle

Step 2 on an open does not see empty boundary members (over data d): Step 2 along the canonical chains for (M, 𝓘, E) and (M, 𝓘, F') agree on U (hfStep2SeqFamAlong_indiff_rel).

theorem Hironaka.Manifold.hfStep2SeqFamOn_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (d : HFData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (hnil : ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s T') (j : T'.F.ι), T'.F.hyp j = ∅ → d.bd₁.fam T' hT' j = CompatibleFamily.nil T') {N : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT' : Manifold.AnalyticTriple.BOClass s (T.pullback g hg)) (hH' : Manifold.IsClosedSubmanifold ψ₀ (⇑g ⁻¹' H) 1) (hle' : hH'.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv (T.pullback g hg).I (s - 1)) (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')) : BO.hfStep2SeqFamOn (T.pullback g hg) s d hT' U' hU' hH' hle' = ((BO.hfStep2SeqFamOn T s d hT (AnalyticMap.imageOpens g hg U') ⋯ hH hle).pullback (AnalyticMap.restrictMap g U' (AnalyticMap.imageOpens g hg U') ⋯) ⋯).eraseEmpty

Step 2 commutes with local analytic isomorphisms on the opens ([Kol07, 104, Step 2.3]; the second clause of [Kol07, 34.1]; over data d): along g : N → M, Step 2 of the pulled-back triple on U' is the pull-back of Step 2 on g(U') with its empty blow-ups deleted. The chain of Step 2.1 over N for the members that stay nonempty is the chain over the full list of members along opens carried into the canonical chain of g(U') (step21FamAux_filter_rel; a member emptied by g contributes nothing by hnil), which is the pull-back of that canonical chain link by link (step21FamAux_rel_along); the link of Step 2.2 is compared on N through the state over the intersection (hfStep22Link_rel along the identity) and transported along g (hfStep22Link_rel along g); restricting to U' and deleting the empty blow-ups gives the statement.