Step 2.1 on an open is indifferent to empty boundary members

The empty blow-up convention of [Kol07, 32] in the compatible-family form of Step 2.1 (Step21Fam.lean): when the nonempty members of E are the members of F' along an order embedding e : F'.ι ↪o E.ι (matched members, the others empty), Step 2.1 on U for (M, 𝓘, E) is Step 2.1 on U for (M, 𝓘, F') (step21FamOn_indifferentToEmptyMembers):

• BDanFamData.fam_seqOn_induced_indiff — Lemma 102's family at the member i of the induced boundary from F' is the family at the member e i of the induced boundary from E, read on any open: the family's indifferentToEmptyMembers along the index correspondence corrIdx of the induced boundaries;
• ChainState.link_L_indiff — two chain states with the same sequence, for the two triples, link to the same sequence at corresponding members (the pulled-back triples over the open are again a boundary change along e);
• ChainState.step21FamAux_indiff_rel — the chains over corresponding member lists, along any two admissible chains of opens, agree on every common open up to empty blow-ups: the two-chain argument of ChainIndep.lean through the virtual chain over the intersections (link_rel twice, restrictEraseId), the two virtual links identified by link_L_indiff;
• step21FamOn_indifferentToEmptyMembers — the list of nonempty members of E is the image along e of that of F' (nonemptyList_eq_map), so the two chains agree on U.

Its chain argument (step21FamAux_indiff_rel) enters the indifference of Step 2 on an open (Step2AssemblyComm.lean).

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_induced_indiff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) {X : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ X) (hT : Manifold.AnalyticTriple.BOClass s T) (F' : Manifold.HypersurfaceFamily X.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')) (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hL' : L.toSuccession.IsOfOrderGe (BDan.withBoundary T F' hsnc').I s (BDan.withBoundary T F' hsnc').F.idealSheaf) (i : F'.ι) (O : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (hO : IsCompact (closure ↑O)) : (bd.fam (T.induced s L hL) ⋯ (L.toSuccession.originalIdx T.F (Fin.last L.toSuccession.length) (e i))).seqOn O hO = (bd.fam ((BDan.withBoundary T F' hsnc').induced s L hL') ⋯ (L.toSuccession.originalIdx F' (Fin.last L.toSuccession.length) i)).seqOn O hO

The value of one link is indifferent to empty members: Lemma 102's family at the member i of the induced boundary from F' equals the family at the member e i of the induced boundary from E, read on any relatively compact open of the last stage. This is the family's indifferentToEmptyMembers along the index correspondence corrIdx e of the induced boundaries, whose members are matched (hyp_corrIdxAux_of_forall) and empty outside the range (hyp_eq_empty_of_notMem_range_corrIdx), the member index corresponding (corrIdxAux_originalIdxAux).

theorem Hironaka.Manifold.ChainState.link_L_indiff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) {X : AnalyticManifold 𝕜 E} (T T' : Manifold.AnalyticTriple ψ₀ X) (hI : T'.I = T.I) (e : T'.F.ι ↪o T.F.ι) (he : ∀ (i : T'.F.ι), T.F.hyp (e i) = T'.F.hyp i) (he' : ∀ b ∉ Set.range ⇑e, T.F.hyp b = ∅) (hT : Manifold.AnalyticTriple.BOClass s T) (hT' : Manifold.AnalyticTriple.BOClass s T') {W : TopologicalSpace.Opens X.carrier} (st : ChainState T s W) (st' : ChainState T' s W) (hL : st.L = st'.L) (i : T'.F.ι) {V : TopologicalSpace.Opens X.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : (link T s bd hT st (e i) hV hVW).L = (link T' s bd hT' st' i hV hVW).L

One link of the chain is indifferent to empty members: two chain states with the same sequence, for a triple T and for a triple T' with the same ideal sheaf whose boundary members are members of T.F along e (the others empty), link to the same sequence at the members e i and i. The triples pulled back to the open are again such a pair (AnalyticTriple.ext'), and the link's value is fam_seqOn_induced_indiff at the induced triples.

theorem Hironaka.Manifold.ChainState.step21FamAux_indiff_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (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) (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' : List F'.ι) (l : List T.F.ι) : List.map (⇑e) 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 (BDan.withBoundary T F' hsnc') s bd hT' W' r' hW' hWsub' l' hl').L.pullback (M.restrictLE hU₂) ⋯).eraseEmpty

The two chains over corresponding member lists agree on every common open: the chain for (M, 𝓘, E) over a list l'.map e along one admissible chain of opens and the chain for (M, 𝓘, F') over l' along another, restricted to a common open and with the empty blow-ups deleted, are equal. By induction on l': the states so far agree on the intersection of the two opens (the induction hypothesis), the two links are compared through the virtual chain over the intersections (link_rel twice, restrictEraseId), where they are the same link at corresponding members (link_L_indiff), then restricted to the smaller open (eraseEmpty_pullback_restrict_congr).

theorem Hironaka.Manifold.step21FamOn_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {s : ℕ} (bd : BDanFamData ψ₀ s) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass s T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (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' }) : step21FamOn T s bd hT U hU = step21FamOn { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } s bd hT' U hU

Step 2.1 on U is indifferent to empty boundary members (Step 2.1 of the proof of [Kol07, Theorem 103] applies Lemma 102 to the nonempty members): the list of nonempty members of E is the image along e of that of F' (nonemptyList_eq_map, reversed), and the two chains agree on U (step21FamAux_indiff_rel).