Step 2 of Theorem 103 along an arbitrary chain of relatively compact opens

The value of Step 2 on a relatively compact open U (step2SeqFamOn, Step22Fam.lean) is computed along one fixed chain of relatively compact opens, taken from the compact exhaustion of the manifold (chainOpens, Step21Fam.lean). To show that the value does not depend on this choice, this module defines Step 2 along an arbitrary admissible chain W : ℕ → Opens M of r + 1 links (r the number of nonempty boundary members): relatively compact opens, each containing the closure of the next, the last containing U. The construction repeats that of step2SeqFamOn with W in place of the exhaustion chain (hfStep2FamChainAlong; hfStep22FamOnAlong, the value hfStep22ValueOf of Step 2.2 over a state of the chain read at the lifted range of the last restriction; hfStep2SeqFamAlong), and hfStep2SeqFamOn_eq_along identifies the canonical value as the value along the exhaustion chain, by definition.

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 independence of the chain, and with it the compatibility of Step 2 under restriction ([Wlo09, Theorem 2.0.3 (4)]), is proved in Step2Assembly.lean.

noncomputable def Hironaka.Manifold.BO.hfStep22ValueOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {M : AnalyticManifold 𝕜 E} (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} (st : ChainState T s W) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : AnalyticManifold.BlowUpSequence ψ₀ ((st.L.stage (Fin.last st.L.length)).restrict (st.L.liftRange (M.restrictLE ⋯) ⋯))

The value of Step 2.2 over a state of the chain (over data d): the family functor of Step 2.2 at the triple of Step 2.2 over the state's sequence, for the triple restricted to the state's open with the restricted hypersurface of maximal contact, read on the lifted range of the restriction to V.

Equations

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

theorem Hironaka.Manifold.BO.closure_chainLast_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) : closure ↑(W (memberCount T s hT + 1)) ⊆ ↑(W (memberCount T s hT))

The next-to-last open of an admissible chain of r + 1 links contains the closure of the last one.

theorem Hironaka.Manifold.BO.chainLast_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) : W (memberCount T s hT + 1) ≤ W (memberCount T s hT)

The last open of an admissible chain lies in the next-to-last one.

noncomputable def Hironaka.Manifold.BO.hfStep2FamChainAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) (d : HFData ψ₀ s) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) : ChainState T s (W (memberCount T s hT))

The chain of Step 2.1 along W, over data d: its state at the next-to-last open W r.

Equations

• Hironaka.Manifold.BO.hfStep2FamChainAlong T s hT W hWsub d hW = Hironaka.Manifold.step21FamAux T s d.bd₁ hT W (Hironaka.Manifold.memberCount T s hT + 1) hW hWsub (T.F.nonemptyList ⋯).reverse ⋯

noncomputable def Hironaka.Manifold.BO.hfStep22FamOnAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) [FiniteDimensional 𝕜 E] (d : HFData ψ₀ s) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) : AnalyticManifold.BlowUpSequence ψ₀ (((hfStep2FamChainAlong T s hT W hWsub d hW).L.stage (Fin.last (hfStep2FamChainAlong T s hT W hWsub d hW).L.length)).restrict ((hfStep2FamChainAlong T s hT W hWsub d hW).L.liftRange (M.restrictLE ⋯) ⋯))

The value of Step 2.2 along W (over data d): the value over the chain's state at W r, read at the lifted range of W (r + 1) ⊆ W r (hfStep22ValueOf).

Equations

• Hironaka.Manifold.BO.hfStep22FamOnAlong T s hT W hWsub d hW hH hle = Hironaka.Manifold.BO.hfStep22ValueOf d T hT hH hle (Hironaka.Manifold.BO.hfStep2FamChainAlong T s hT W hWsub d hW) ⋯ ⋯

noncomputable def Hironaka.Manifold.BO.hfStep2SeqFamAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (hWsub : ∀ k < memberCount T s hT + 1, closure ↑(W (k + 1)) ⊆ ↑(W k)) [FiniteDimensional 𝕜 E] (d : HFData ψ₀ s) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (U : TopologicalSpace.Opens M.carrier) (hUW : U ≤ W (memberCount T s hT + 1)) : AnalyticManifold.BlowUpSequence ψ₀ (M.restrict U)

The value of Step 2 on U along the admissible chain W, over data d: the chain of Step 2.1 along W with Step 2.2 appended at the last link, restricted to U ⊆ W (r + 1), with its empty blow-ups deleted.

Equations

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

theorem Hironaka.Manifold.BO.hfStep2SeqFamOn_eq_along {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (hT : Manifold.AnalyticTriple.BOClass s T) [FiniteDimensional 𝕜 E] (d : HFData ψ₀ s) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : hfStep2SeqFamOn T s d hT U hU hH hle = hfStep2SeqFamAlong T s hT (chainOpens (exhaustion M) (exhaustionIdx (exhaustion M) hU) (memberCount T s hT + 1)) ⋯ d ⋯ hH hle U ⋯

The value of Step 2 on U (hfStep2SeqFamOn) is Step 2 along the chain of exhaustion opens, by definition.