The rounds read through a composite: restriction of the reading map

The rounds of the resolution family (resolveFrom, Hironaka/Resolution/Analytic/Wlo09/Rounds.lean) read through a composite ι ∘ j of local analytic isomorphisms are the rounds read through ι, pulled back along j: an equality of lists before any erasing (resolveFrom_comp). This is the pull-back of a blow-up sequence along a smooth morphism [Kol07, 30.1] for the concatenation of the rounds, and it gives the compat field of the resolution family resolveFam at ι := restrictLE (V ≤ W), j := restrictLE (U ≤ V), once canonicity (Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean) has identified the values along the two chains.

The proof is the induction on the number of rounds that defines resolveFrom, unfolded at the successor case only: the round's list pulled back along ι' ∘ j is its pull-back along ι' pulled back along j (pullback_comp), the last-stage lift of the composite is the composite of the last-stage lifts up to the identification stageOfEq of the two pulled-back lists (pullbackLiftLast_comp_apply, uniqueness of lifts), and the concatenation absorbs that identification (concat_pullback_stageOfEq). Two congruences do the bookkeeping: the rounds depend on the reading map alone (resolveFrom_congr_ι), and pulling the second piece of a concatenation back along stageOfEq of an equality of first pieces is the identity (concat_pullback_stageOfEq, the pull-back form of concat_map_stageOfEq). List algebra, not in the sources.

theorem Hironaka.Manifold.concat_pullback_stageOfEq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {L₁ L₂ : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (e : L₂ = L₁) (R : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (L₁.stage (Fin.last L₁.length))) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑(AnalyticManifold.BlowUpSequence.stageOfEq e).toAnalyticMap) : L₂.concat (R.pullback (AnalyticManifold.BlowUpSequence.stageOfEq e).toAnalyticMap he) = L₁.concat R

Transport of the second piece of a concatenation along an equality of first pieces, the pull-back form of concat_map_stageOfEq: pulling the second piece back along the cast stageOfEq e absorbs the cast.

theorem Hironaka.Manifold.resolveFrom_congr_ι {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (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ι : ι₁ = ι₂) (h₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι₁) (r₁ : Set.range ⇑ι₁ ⊆ ↑(Ω 0)) (h₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι₂) (r₂ : Set.range ⇑ι₂ ⊆ ↑(Ω 0)) : resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι₁ h₁ r₁ = resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι₂ h₂ r₂

The rounds depend on the reading map only (its proofs are irrelevant): a congruence along an equality of reading maps.

theorem Hironaka.Manifold.resolveFrom_comp {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (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 N' : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) (j : AnalyticMap N' N) (hj : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑j) (hrange' : Set.range ⇑(ContMDiffMap.comp ι j) ⊆ ↑(Ω 0)) : resolveFrom bo d cur hord hfin Ω hΩ hΩsub (ContMDiffMap.comp ι j) ⋯ hrange' = (resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange).pullback j hj

Restriction of the reading map. The rounds read through ι ∘ j are the rounds read through ι, pulled back along the local analytic isomorphism j: an equality of lists before any erasing ([Kol07, 30.1] for the concatenation: pullback_concat, pullback_comp, the last-stage lifts compose). The compat field of resolveFam is this at ι := restrictLE (V ≤ W), j := restrictLE (U ≤ V), after canonicity.