The value of a compatible-family functor at the induced triple

Two transport identities for the value of the data BDanFamData of [Kol07, Lemma 102] in the compatible-family form (FamilyData.lean), read at the triple induced by a sequence of centres at its last stage (the triples (X_j, I_j, E_j) of [Kol07, 104, Step 2.1.j]).

• Deleting empty blow-ups ([Kol07, 32]; [Kol07, 34.1]): the triple induced by the sequence with its empty blow-ups deleted is the pull-back of the triple induced by the sequence along the isomorphism eraseEmptyLast⁻¹ of the last stages (its controlled transform by markedTransformSeq_last_eraseEmpty), up to the empty members of the boundary (the order embedding eraseEmptyIdx of the kept indices), so the indifference of the data to empty members and its commutation with local analytic isomorphisms identify the two values (fam_seqOn_induced_eraseEmpty).
• Pulling back along a local analytic isomorphism (the functoriality argument in the proof of [Kol07, Lemma 102]): the triple induced by the pulled-back sequence is the pull-back of the induced triple along the lift to the last stage (induced_pullback), and the commutation of the data with local analytic isomorphisms applies (fam_seqOn_induced_pullback).

Not in the sources; bookkeeping for the assembly of Step 2.1 in the compatible-family form.

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_congr {𝕜 : 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} (h : T₁ = T₂) (hT₁ : Manifold.AnalyticTriple.BOClass s T₁) (hT₂ : Manifold.AnalyticTriple.BOClass s T₂) (j₁ : T₁.F.ι) (j₂ : T₂.F.ι) (hj : j₁ ≍ j₂) (U : TopologicalSpace.Opens X.carrier) (hU : IsCompact (closure ↑U)) : (bd.fam T₁ hT₁ j₁).seqOn U hU = (bd.fam T₂ hT₂ j₂).seqOn U hU

The value of the family depends only on the triple and the member.

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_induced_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) {M N : AnalyticManifold 𝕜 E} (TW : Manifold.AnalyticTriple ψ₀ M) (hTW : Manifold.AnalyticTriple.BOClass s TW) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe TW.I s TW.F.idealSheaf) (j : TW.F.ι) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hTW' : Manifold.AnalyticTriple.BOClass s (TW.pullback h hh)) (hL' : (L.pullback h hh).toSuccession.IsOfOrderGe (TW.pullback h hh).I s (TW.pullback h hh).F.idealSheaf) (U' : TopologicalSpace.Opens ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier) (hU' : IsCompact (closure ↑U')) : (bd.fam ((TW.pullback h hh).induced s (L.pullback h hh) hL') ⋯ ((L.pullback h hh).toSuccession.originalIdx (TW.pullback h hh).F (Fin.last (L.pullback h hh).toSuccession.length) j)).seqOn U' hU' = (((bd.fam (TW.induced s L hL) ⋯ (L.toSuccession.originalIdx TW.F (Fin.last L.toSuccession.length) j)).seqOn (AnalyticMap.imageOpens (L.pullbackLiftLast h hh) ⋯ U') ⋯).pullback (AnalyticMap.restrictMap (L.pullbackLiftLast h hh) U' (AnalyticMap.imageOpens (L.pullbackLiftLast h hh) ⋯ U') ⋯) ⋯).eraseEmpty

The value of the family at the triple induced by a pulled-back sequence is the value at the triple induced by the sequence on the image, pulled back along the lift to the last stage (the functoriality argument in the proof of [Kol07, Lemma 102]): induced_pullback, originalIdx_last_pullback_heq and the commutation of the data with local analytic isomorphisms.

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_induced_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (bd : BDanFamData ψ₀ s) {M : AnalyticManifold 𝕜 E} (TW : Manifold.AnalyticTriple ψ₀ M) (hTW : Manifold.AnalyticTriple.BOClass s TW) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe TW.I s TW.F.idealSheaf) (j : TW.F.ι) (V : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (hV : IsCompact (closure ↑V)) : (bd.fam (TW.induced s L hL) ⋯ (L.toSuccession.originalIdx TW.F (Fin.last L.toSuccession.length) j)).seqOn V hV = (((bd.fam (TW.induced s L.eraseEmpty ⋯) ⋯ (L.eraseEmpty.toSuccession.originalIdx TW.F (Fin.last L.eraseEmpty.toSuccession.length) j)).seqOn (AnalyticMap.imageOpens L.eraseEmptyLast.toAnalyticMap ⋯ V) ⋯).pullback (AnalyticMap.restrictMap L.eraseEmptyLast.toAnalyticMap V (AnalyticMap.imageOpens L.eraseEmptyLast.toAnalyticMap ⋯ V) ⋯) ⋯).eraseEmpty

The value of the family at the triple induced by a sequence is the value at the triple induced by the sequence with its empty blow-ups deleted, transported along the isomorphism eraseEmptyLast of the last stages ([Kol07, 32]; [Kol07, 34.1]): the former triple is the pull-back of the latter along eraseEmptyLast⁻¹ up to empty boundary members (markedTransformSeq_last_eraseEmpty, eraseEmptyIdx), so the indifference of the data to empty members and its commutation with local analytic isomorphisms apply.