Step 2 on an open: independence of the chain and compatibility under restriction

The value of Step 2 on a relatively compact open U (step2SeqFamOn, Step22Fam.lean) is Step 2 along the chain of exhaustion opens (hfStep2SeqFamOn_eq_along, Step2Along.lean): the chain of Step 2.1 with the value of Step 2.2 appended at the last link, restricted to U, with its empty blow-ups deleted. This module proves that the value does not depend on the admissible chain of opens, and derives the compatibility of the values under restriction, the clause (4) of [Wlo09, Theorem 2.0.3] that makes them a compatible family:

• BO.hfStep2SeqFamAlong_rel — along two admissible chains the two values of Step 2 agree on every common open: the chains of Step 2.1 agree on the intersection of the next-to-last opens (step21FamAux_filter_rel, ChainIndep.lean); the link of Step 2.2 on each chain is compared, through the state over that intersection, with the link on the other (hfStep22Link_rel along the identity, Step2LinkTransport.lean), the two intermediate links being the same sequence; then both are restricted to the common open (eraseEmpty_pullback_restrict_congr).
• hfStep2SeqFamOn_compat — for U ≤ V, the value of Step 2 on U is the value on V restricted to U with its empty blow-ups deleted: independence of the chain, for the chain of V read on U. This is the second clause of [Kol07, 34.1] (pull-back along an open embedding, up to empty blow-ups) in the per-open form, the counterpart for Step 2 of step21FamOn_compat (Step21FamIndep.lean).

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. The compatibility is the field compat of the compatible family of the local functor (LocalFunctorFam.lean).

theorem Hironaka.Manifold.BO.hfStep2SeqFamAlong_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)) (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 T 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 T s hT + 1)) : hfStep2SeqFamAlong T s hT W hWsub d hW hH hle U hU₁ = hfStep2SeqFamAlong T s hT W' hWsub' d hW' hH hle U hU₂

Along two admissible chains of opens the values of Step 2 agree on every common open ([Kol07, 34.1] for the choice of the chain; over data d): the chains of Step 2.1 agree on the intersection of the next-to-last opens (step21FamAux_filter_rel, applied to the same list of members); the link of Step 2.2 on each chain is compared, through the state over that intersection (restrictEraseId), with the link on the other (hfStep22Link_rel along the identity; the two intermediate links are the same sequence); then both are restricted to the common open (eraseEmpty_pullback_restrict_congr).

theorem Hironaka.Manifold.hfStep2SeqFamOn_compat {𝕜 : 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)) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hUV : U ≤ V) : BO.hfStep2SeqFamOn T s d hT U hU hH hle = ((BO.hfStep2SeqFamOn T s d hT V hV hH hle).pullback (M.restrictLE hUV) ⋯).eraseEmpty

Compatibility of Step 2 under restriction ([Wlo09, Theorem 2.0.3 (4)]; the second clause of [Kol07, 34.1] per open; over data d): for U ≤ V the value on U is the value on V restricted to U with its empty blow-ups deleted, by the independence of the chain (hfStep2SeqFamAlong_rel) for the chain of V read on U.