The rounds are indifferent to empty boundary members

Two triples with the same ideal sheaf whose boundary families differ by empty members only (an order embedding of the indices matching the members, the members off its range empty) have the same rounds, an exact equality of lists (resolveFrom_indiff). This is the empty blow-up convention [Kol07, 32] on the side of the boundary: empty members of the boundary family carry no information, and the order-reduction functors ignore them (the field indifferentToEmptyMembers of BOanFam). Each round's list agrees by that field, and the derived triples differ by empty members again: the exceptional members are added identically to both boundary families, and the index correspondence corrIdx of the total transforms (Hironaka/Resolution/Analytic/OrderReduction/Step21Indiff.lean) is the order embedding of the next round. The induction unfolds resolveFrom at the successor case only; its step is resolveFrom_indiff_step, with the two round lists abstracted so that their equality can be substituted, and the congruence resolveFrom_congr_triple along an equality of triples. Hironaka/Resolution/Analytic/Wlo09/Transport.lean and Hironaka/Resolution/Analytic/Wlo09/TopRound.lean use it to remove the empty members that the erasure of empty blow-ups creates in a boundary family.

theorem Hironaka.Manifold.resolveFrom_congr_triple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} {cur₁ cur₂ : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X} (e : cur₁ = cur₂) (hord₁ : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur₁.I x ≤ ↑d) (hfin₁ : Finite { j : cur₁.F.ι // cur₁.F.hyp j ≠ ∅ }) (hord₂ : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur₂.I x ≤ ↑d) (hfin₂ : Finite { j : cur₂.F.ι // cur₂.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) : resolveFrom bo d cur₁ hord₁ hfin₁ Ω hΩ hΩsub ι hι hrange = resolveFrom bo d cur₂ hord₂ hfin₂ Ω hΩ hΩsub ι hι hrange

The rounds depend on the triple only up to equality (its proofs are irrelevant): a congruence along an equality of triples.

theorem Hironaka.Manifold.resolveFrom_indiff_step {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (F' : Manifold.HypersurfaceFamily X.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o cur.F.ι) (hhyp : ∀ (i : F'.ι), cur.F.hyp (e i) = F'.hyp i) (hempty : ∀ b ∉ Set.range ⇑e, cur.F.hyp b = ∅) (ih : ∀ {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (F' : Manifold.HypersurfaceFamily X.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o cur.F.ι), (∀ (i : F'.ι), cur.F.hyp (e i) = F'.hyp i) → (∀ b ∉ Set.range ⇑e, cur.F.hyp b = ∅) → ∀ (hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑d) (hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) (hfin' : Finite { j : { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.F.ι // { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)), resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange = resolveFrom bo d { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hord hfin' Ω hΩ hΩsub ι hι hrange) (O : TopologicalSpace.Opens X.carrier) (Ω : ℕ → TopologicalSpace.Opens X.carrier) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hr : Set.range ⇑ι ⊆ ↑O) (L₁ L₂ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (X.restrict O)) (hL : L₁ = L₂) (hge₁ : L₁.toSuccession.IsOfOrderGe (cur.pullback (X.inclusion O) ⋯).I (d + 1) (cur.pullback (X.inclusion O) ⋯).F.idealSheaf) (hge₂ : L₂.toSuccession.IsOfOrderGe ({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).I (d + 1) ({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).F.idealSheaf) (h₁ h₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(AnalyticMap.corestrict ι O hr)) (hord₁ : ∀ (x : ↑↧(L₁.stage (Fin.last L₁.length)).carrier), Manifold.IdealSheaf.ord ((cur.pullback (X.inclusion O) ⋯).induced (d + 1) L₁ hge₁).I x ≤ ↑d) (hfin₁ : Finite { j : ((cur.pullback (X.inclusion O) ⋯).induced (d + 1) L₁ hge₁).F.ι // ((cur.pullback (X.inclusion O) ⋯).induced (d + 1) L₁ hge₁).F.hyp j ≠ ∅ }) (hΩ₁ : ∀ k < d, IsCompact (closure ↑(liftChain L₁ Ω k))) (hΩsub₁ : ∀ (k : ℕ), k + 1 < d → closure ↑(liftChain L₁ Ω k) ⊆ ↑(liftChain L₁ Ω (k + 1))) (hk₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(L₁.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₁)) (hr₁ : Set.range ⇑(L₁.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₁) ⊆ ↑(liftChain L₁ Ω 0)) (hord₂ : ∀ (x : ↑↧(L₂.stage (Fin.last L₂.length)).carrier), Manifold.IdealSheaf.ord (({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).induced (d + 1) L₂ hge₂).I x ≤ ↑d) (hfin₂ : Finite { j : (({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).induced (d + 1) L₂ hge₂).F.ι // (({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).induced (d + 1) L₂ hge₂).F.hyp j ≠ ∅ }) (hΩ₂ : ∀ k < d, IsCompact (closure ↑(liftChain L₂ Ω k))) (hΩsub₂ : ∀ (k : ℕ), k + 1 < d → closure ↑(liftChain L₂ Ω k) ⊆ ↑(liftChain L₂ Ω (k + 1))) (hk₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(L₂.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₂)) (hr₂ : Set.range ⇑(L₂.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₂) ⊆ ↑(liftChain L₂ Ω 0)) : (L₁.pullback (AnalyticMap.corestrict ι O hr) h₁).concat (resolveFrom bo d ((cur.pullback (X.inclusion O) ⋯).induced (d + 1) L₁ hge₁) hord₁ hfin₁ (liftChain L₁ Ω) hΩ₁ hΩsub₁ (L₁.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₁) hk₁ hr₁) = (L₂.pullback (AnalyticMap.corestrict ι O hr) h₂).concat (resolveFrom bo d (({ I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.pullback (X.inclusion O) ⋯).induced (d + 1) L₂ hge₂) hord₂ hfin₂ (liftChain L₂ Ω) hΩ₂ hΩsub₂ (L₂.pullbackLiftLast (AnalyticMap.corestrict ι O hr) h₂) hk₂ hr₂)

The successor step of resolveFrom_indiff with the two round lists abstracted, so that their equality (the field indifferentToEmptyMembers) can be substituted: the second factors agree by the induction hypothesis at the derived triples, whose boundary families correspond along the index correspondence corrIdx of the total transforms (the exceptional members added to both sides).

theorem Hironaka.Manifold.resolveFrom_indiff {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (F' : Manifold.HypersurfaceFamily X.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') (e : F'.ι ↪o cur.F.ι) (hhyp : ∀ (i : F'.ι), cur.F.hyp (e i) = F'.hyp i) (hempty : ∀ b ∉ Set.range ⇑e, cur.F.hyp b = ∅) (hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑d) (hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) (hfin' : Finite { j : { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.F.ι // { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) : resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange = resolveFrom bo d { I := cur.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hord hfin' Ω hΩ hΩsub ι hι hrange

Indifference to empty boundary members (the empty blow-up convention [Kol07, 32]). Two triples with the same ideal sheaf whose boundary families differ by empty members only (an order embedding e of the indices, the members off its range empty) have the same rounds: each round's value agrees by the field indifferentToEmptyMembers, and the derived triples differ by empty members again (the exceptional members are added to both).