Tools for the transport of the chain of Step 2.1

Two facts used in the transport of a link along a value functor (ValueTransport.lean, ChainTransport.lean):

• BlowUpSequence.range_pullbackLiftLast, mem_liftRange_iff — the range of the last-stage lift of a local analytic isomorphism h along a sequence of centres is the preimage of the range of h under the composite blow-down (one step is exists_liftStep_eq: every point over a point of the range of h lifts), so the reading open of the chain (FamilyChain.lean) is the preimage of the smaller open under the blow-down.
• BDanFamData.fam_seqOn_induced_pullback_congr — for two equal sequences of centres, opens of their last stages corresponding under stageOfEq, and maps into them agreeing under stageOfEq, the pull-backs of the family's values at the induced triples agree (a substitution).

theorem AnalyticManifold.BlowUpSequence.range_pullbackLiftLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Set.range ⇑(L.pullbackLiftLast h hh) = ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Set.range ⇑h

The range of the last-stage lift of h is the preimage of the range of h under the composite blow-down: ⊆ is range_pullbackLiftLast_subset; for ⊇, a point over h b is in the range of the lift of the first step (exists_liftStep_eq), then the induction.

theorem AnalyticManifold.BlowUpSequence.mem_liftRange_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (p : (L.stage (Fin.last L.length)).carrier) : p ∈ L.liftRange h hh ↔ (L.toSuccession.stageMap (Fin.last L.toSuccession.length)) p ∈ Set.range ⇑h

The reading open of the chain is the preimage of the range of h under the composite blow-down.

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_induced_pullback_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) {X Z : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ X} (hT : Manifold.AnalyticTriple.BOClass s T) {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ X} (e : L₁ = L₂) (hL₁ : L₁.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hL₂ : L₂.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (j : T.F.ι) {U₁ : TopologicalSpace.Opens (L₁.stage (Fin.last L₁.length)).carrier} {U₂ : TopologicalSpace.Opens (L₂.stage (Fin.last L₂.length)).carrier} (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (hU : ∀ (p : (L₁.stage (Fin.last L₁.length)).carrier), p ∈ U₁ ↔ (AnalyticManifold.BlowUpSequence.stageOfEq e) p ∈ U₂) (f₁ : AnalyticMap Z ((L₁.stage (Fin.last L₁.length)).restrict U₁)) (f₂ : AnalyticMap Z ((L₂.stage (Fin.last L₂.length)).restrict U₂)) (hf₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₁) (hf₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₂) (hf : ∀ (z : Z.carrier), (AnalyticManifold.BlowUpSequence.stageOfEq e) ↑(f₁ z) = ↑(f₂ z)) : ((bd.fam (T.induced s L₁ hL₁) ⋯ (L₁.toSuccession.originalIdx T.F (Fin.last L₁.toSuccession.length) j)).seqOn U₁ hU₁).pullback f₁ hf₁ = ((bd.fam (T.induced s L₂ hL₂) ⋯ (L₂.toSuccession.originalIdx T.F (Fin.last L₂.toSuccession.length) j)).seqOn U₂ hU₂).pullback f₂ hf₂

Congruence of pulled-back induced values along equal sequences: for equal sequences L₁ = L₂, opens of their last stages corresponding under stageOfEq, and maps into those opens agreeing under stageOfEq, the pull-backs of the family's values at the induced triples agree (a substitution).