The chain of Step 2.1 does not depend on the chain of opens

The value of Step 2.1 of the proof of [Kol07, Theorem 103] in the compatible-family form (Step21Fam.lean) is computed along a fixed shrinking chain of relatively compact opens. By the second clause of [Kol07, 34.1] and the compatibility of [Wlo09, Theorem 2.0.3 (4)] it should not depend on the chain: two chains over two admissible chains of opens, processing the same members, agree on a common smaller open up to empty blow-ups (ChainState.step21FamAux_filter_rel). The proof goes link by link through a virtual chain over the intersections of the opens, the chain of the triple pulled back along the identity (ChainState.restrictEraseId), to which both chains are related by the transport of one link (link_rel of ChainTransport.lean, twice); the states are compared by "the sequence over the smaller open, with the empty blow-ups deleted, is the pull-back of the sequence over the larger one, with the empty blow-ups deleted". A member whose boundary hypersurface is empty contributes nothing (link_L_of_hyp_eq_empty: the induced member is the strict transform of ∅, and the family's value at an empty member is the trivial family, the hypothesis hnil, which the concrete data satisfy), which identifies the chain over a member list filtered of its empty members with the chain over the full list.

The consequences, the independence of the chain, the compatibility under restriction and the commutation with local analytic isomorphisms, are drawn in Step21FamIndep.lean; the same two-chain argument gives the indifference to empty boundary members in Step21FamIndiff.lean.

theorem Hironaka.Manifold.ChainState.link_L_of_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (hnil : ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s T') (j : T'.F.ι), T'.F.hyp j = ∅ → bd.fam T' hT' j = CompatibleFamily.nil T') {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) {j : T.F.ι} (hj : T.F.hyp j = ∅) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : (link T s bd hT st j hV hVW).L = st.L.pullback (M.restrictLE ⋯) ⋯

A link at a member whose hypersurface is empty is the restriction of the sequence to the smaller open (the counterpart for boundary members of [Kol07, 32]): the induced member is the strict transform of ∅ (hyp_originalIdx, strictTransformSeq_empty), the family's value there is the trivial family (hnil), and appending the empty sequence is the identity (concat_nil_right).

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_pullback_restrict_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {X Y I U : TopologicalSpace.Opens M.carrier} (A : BlowUpSequence ψ₀ (M.restrict X)) (B : BlowUpSequence ψ₀ (M.restrict Y)) (hIX : I ≤ X) (hIY : I ≤ Y) (hUI : U ≤ I) (h : (A.pullback (M.restrictLE hIX) ⋯).eraseEmpty = (B.pullback (M.restrictLE hIY) ⋯).eraseEmpty) : (A.pullback (M.restrictLE ⋯) ⋯).eraseEmpty = (B.pullback (M.restrictLE ⋯) ⋯).eraseEmpty

Two sequences over opens X, Y whose restrictions to a common open I agree up to empty blow-ups agree, up to empty blow-ups, on every U ≤ I (pullback_comp, eraseEmpty_pullback_eraseEmpty).

theorem Hironaka.Manifold.ChainState.image_id_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {I W : TopologicalSpace.Opens M.carrier} (hIW : I ≤ W) : ⇑ContMDiffMap.id '' ↑I ⊆ ↑W

The image of an open under the identity is the open (as sets).

theorem Hironaka.Manifold.ChainState.pullback_inclusion_pullback_restrictMap_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {I W : TopologicalSpace.Opens M.carrier} (hIW : I ≤ W) : (T.pullback (M.inclusion W) ⋯).pullback (AnalyticMap.restrictMap ContMDiffMap.id I W ⋯) ⋯ = (T.pullback ContMDiffMap.id ⋯).pullback (M.inclusion I) ⋯

The triple over a smaller open I ≤ W, as the pull-back along I → W of the triple over W, is the triple over I of the triple pulled back along the identity (pullback_pullback).

noncomputable def Hironaka.Manifold.ChainState.restrictEraseId {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) {I : TopologicalSpace.Opens M.carrier} (hIW : I ≤ W) : ChainState (T.pullback ContMDiffMap.id ⋯) s I

The virtual state over a smaller open: the state's sequence restricted to I ≤ W, with the empty blow-ups deleted, as a chain state of the triple pulled back along the identity (its order clause by isOfOrderGe_pullback and isOfOrderGe_eraseEmpty).

Equations

• Hironaka.Manifold.ChainState.restrictEraseId T s st hIW = { L := (st.L.pullback (Hironaka.Manifold.AnalyticMap.restrictMap ContMDiffMap.id I W ⋯) ⋯).eraseEmpty, hge := ⋯ }

theorem Hironaka.Manifold.ChainState.restrictEraseId_L {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) {I : TopologicalSpace.Opens M.carrier} (hIW : I ≤ W) : (restrictEraseId T s st hIW).L = (st.L.pullback (M.restrictLE hIW) ⋯).eraseEmpty

The virtual state's sequence is the restricted sequence with the empty blow-ups deleted (the restriction written as restrictLE).

theorem Hironaka.Manifold.ChainState.step21FamAux_filter_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (W : ℕ → TopologicalSpace.Opens M.carrier) (r : ℕ) (hW : ∀ (k : ℕ), IsCompact (closure ↑(W k))) (hWsub : ∀ k < r, closure ↑(W (k + 1)) ⊆ ↑(W k)) (W' : ℕ → TopologicalSpace.Opens M.carrier) (r' : ℕ) (hW' : ∀ (k : ℕ), IsCompact (closure ↑(W' k))) (hWsub' : ∀ k < r', closure ↑(W' (k + 1)) ⊆ ↑(W' k)) (l l' : List T.F.ι) : (∀ j ∈ l, T.F.hyp j = ∅ → ∀ {M' : AnalyticManifold 𝕜 E} (T' : Manifold.AnalyticTriple ψ₀ M') (hT' : Manifold.AnalyticTriple.BOClass s T') (j' : T'.F.ι), T'.F.hyp j' = ∅ → bd.fam T' hT' j' = CompatibleFamily.nil T') → List.filter (fun (j : T.F.ι) => decide (T.F.hyp j ≠ ∅)) l = l' → ∀ (hl : l.length ≤ r) (hl' : l'.length ≤ r') (U : TopologicalSpace.Opens M.carrier) (hU₁ : U ≤ W l.length) (hU₂ : U ≤ W' l'.length), ((step21FamAux T s bd hT W r hW hWsub l hl).L.pullback (M.restrictLE hU₁) ⋯).eraseEmpty = ((step21FamAux T s bd hT W' r' hW' hWsub' l' hl').L.pullback (M.restrictLE hU₂) ⋯).eraseEmpty

The second clause of [Kol07, 34.1] for the chain of Step 2.1: two chains over two admissible chains of opens, the second processing the members of the first with nonempty hypersurface, agree on every common smaller open up to empty blow-ups. By induction on the member list: a member with empty hypersurface is a restriction on the first chain and is dropped by the second (link_L_of_hyp_eq_empty); a kept member is linked on both chains and compared through the virtual chain over the intersections (link_rel twice, restrictEraseId), then restricted to the smaller open (eraseEmpty_pullback_restrict_congr).