The value of Step 2.2 under deletion of empty blow-ups and under pull-back

The value of Step 2.2 on an open is the family functor of Step 2.2 (Step22Fam.lean) at the triple of Step 2.2 over the sequence of Step 2.1, read on the lifted range of the last restriction. To transport this value along the restrictions of the chain and along local analytic isomorphisms (Step2LinkTransport.lean), exactly as ChainTransport.lean transports Lemma 102's family at the induced triple, three facts about the value are needed:

• BO.hfStep22Fam_seqOn_eraseEmpty — the value over a sequence L is its value over the sequence with the empty blow-ups deleted, transported along the identification of the last stages (eraseEmptyLast). The tuned triple of Step 2.2 over L is the pull-back of the tuned triple of Step 2.2 over the cleaned sequence along eraseEmptyLast, up to the empty exceptional members (the appended member H_r is kept), so the indifference of the data to empty boundary members ([Kol07, 32]) and their commutation with local analytic isomorphisms ([Kol07, 34.1]) at the re-tuned mark give the value.
• BO.hfStep22Fam_seqOn_pullback, BO.hfStep22Fam_seqOn_pullback_liftRange — the value over the pull-back of L along a local analytic isomorphism is the pull-back of the value over L along the lift, with empty blow-ups deleted: the triple of Step 2.2 over the pulled-back sequence is the pull-back of the triple of Step 2.2 along the lift (step22TripleOf_isPullbackOf, Step22Pullback.lean), and the family functor of Step 2.2 commutes with local analytic isomorphisms (Step22FamFunctoriality.lean); with the compatibility of the family under inclusion, this gives the value on the lifted reading opens ([Kol07, 104, Step 2.3]).
• BO.hfStep22Fam_seqOn_congr — the value depends only on the sequence: a substitution along an equality of sequences.

The hf… declarations are the general forms over data d : HFData ψ₀ s of Step 2 (HFamData.lean); the plain forms are their instances at Lemma 102's data.

theorem Hironaka.Manifold.BO.hfStep22Fam_seqOn_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (hcls : stepHClass s (step22TripleOf T L hL hsnc)) (hLe : L.eraseEmpty.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnce : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L.eraseEmpty).append (transformHOf L.eraseEmpty H))) (hclse : stepHClass s (step22TripleOf T L.eraseEmpty hLe hsnce)) (V : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier) (hV : IsCompact (closure ↑V)) : ((hfStep22Functor d.hf).fam (step22TripleOf T L hL hsnc) hcls).seqOn V hV = ((((hfStep22Functor d.hf).fam (step22TripleOf T L.eraseEmpty hLe hsnce) hclse).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 functor of Step 2.2 over a sequence L is its value over the sequence with the empty blow-ups deleted, transported along the identification eraseEmptyLast of the last stages, with empty blow-ups deleted ([Kol07, 32] and [Kol07, 34.1]; over data d). The tuned triple of Step 2.2 over L is the pull-back of the tuned triple of Step 2.2 over the cleaned sequence along eraseEmptyLast, up to the empty exceptional members of the deleted steps (markedTransformSeq_last_eraseEmpty, eraseEmptyIdx; the appended member H_r is kept, both greatest members being the appended one), so the indifference of the data to empty members at the re-tuned mark and then their commutation with local analytic isomorphisms give the value.

theorem Hironaka.Manifold.BO.hfStep22Fam_seqOn_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} (hW : AnalyticMap N M) (hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (hcls : stepHClass s (step22TripleOf T L hL hsnc)) (hL' : (L.pullback hW hhW).toSuccession.IsOfOrderGe (T.pullback hW hhW).I s (T.pullback hW hhW).F.idealSheaf) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf (L.pullback hW hhW)).append (transformHOf (L.pullback hW hhW) (⇑hW ⁻¹' H)))) (hcls' : stepHClass s (step22TripleOf (T.pullback hW hhW) (L.pullback hW hhW) hL' hsnc')) (U' : TopologicalSpace.Opens ((L.pullback hW hhW).stage (Fin.last (L.pullback hW hhW).length)).carrier) (hU' : IsCompact (closure ↑U')) : ((hfStep22Functor d.hf).fam (step22TripleOf (T.pullback hW hhW) (L.pullback hW hhW) hL' hsnc') hcls').seqOn U' hU' = ((((hfStep22Functor d.hf).fam (step22TripleOf T L hL hsnc) hcls).seqOn (AnalyticMap.imageOpens (L.pullbackLiftLast hW hhW) ⋯ U') ⋯).pullback (AnalyticMap.restrictMap (L.pullbackLiftLast hW hhW) U' (AnalyticMap.imageOpens (L.pullbackLiftLast hW hhW) ⋯ U') ⋯) ⋯).eraseEmpty

The value of the family functor of Step 2.2 over the pull-back of a sequence along a local analytic isomorphism is the pull-back of its value over the sequence, read at the image of the open under the lift, with empty blow-ups deleted ([Kol07, 34.1]; over data d): the triple of Step 2.2 over the pulled-back sequence is the pull-back of the triple of Step 2.2 along the lift (step22TripleOf_isPullbackOf), and the family functor of Step 2.2 commutes with local analytic isomorphisms (hfStep22Functor_commutesWithLocalIsos).

theorem Hironaka.Manifold.BO.hfStep22Fam_seqOn_pullback_liftRange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {M N P Q : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} (hW : AnalyticMap N M) (hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW) (L : AnalyticManifold.BlowUpSequence ψ₀ M) (hL : L.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnc : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) (hcls : stepHClass s (step22TripleOf T L hL hsnc)) (hL' : (L.pullback hW hhW).toSuccession.IsOfOrderGe (T.pullback hW hhW).I s (T.pullback hW hhW).F.idealSheaf) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf (L.pullback hW hhW)).append (transformHOf (L.pullback hW hhW) (⇑hW ⁻¹' H)))) (hcls' : stepHClass s (step22TripleOf (T.pullback hW hhW) (L.pullback hW hhW) hL' hsnc')) (ρ : AnalyticMap P M) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) (ρ' : AnalyticMap Q N) (hρ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ') (hV : AnalyticMap Q P) (hsq : ContMDiffMap.comp ρ hV = ContMDiffMap.comp hW ρ') (hO₁ : IsCompact (closure ↑(L.liftRange ρ hρ))) (hOP : IsCompact (closure ↑((L.pullback hW hhW).liftRange ρ' hρ'))) : ((((hfStep22Functor d.hf).fam (step22TripleOf T L hL hsnc) hcls).seqOn (L.liftRange ρ hρ) hO₁).pullback (AnalyticMap.restrictMap (L.pullbackLiftLast hW hhW) ((L.pullback hW hhW).liftRange ρ' hρ') (L.liftRange ρ hρ) ⋯) ⋯).eraseEmpty = ((hfStep22Functor d.hf).fam (step22TripleOf (T.pullback hW hhW) (L.pullback hW hhW) hL' hsnc') hcls').seqOn ((L.pullback hW hhW).liftRange ρ' hρ') hOP

The value over the sequence L on the lifted range of ρ, pulled back along the lift restricted to the lifted range of ρ', is the value over the pulled-back sequence on the lifted range of ρ' (over data d): hfStep22Fam_seqOn_pullback, the compatibility of the family under inclusion, and the fact that the lift carries the lifted range of ρ' into that of ρ by the commuting square hsq. The analogue for Lemma 102's family at the induced triple is fam_seqOn_induced_pullback_liftRange (ChainTransport.lean).

theorem Hironaka.Manifold.BO.hfStep22Fam_seqOn_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {H : Set M.carrier} {L₁ L₂ : AnalyticManifold.BlowUpSequence ψ₀ M} (e : L₁ = L₂) (hL₁ : L₁.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hL₂ : L₂.toSuccession.IsOfOrderGe T.I s T.F.idealSheaf) (hsnc₁ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L₁).append (transformHOf L₁ H))) (hsnc₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L₂).append (transformHOf L₂ H))) (hcls₁ : stepHClass s (step22TripleOf T L₁ hL₁ hsnc₁)) (hcls₂ : stepHClass s (step22TripleOf T L₂ hL₂ hsnc₂)) (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₂) {Z : AnalyticManifold 𝕜 E} (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)) : (((hfStep22Functor d.hf).fam (step22TripleOf T L₁ hL₁ hsnc₁) hcls₁).seqOn U₁ hU₁).pullback f₁ hf₁ = (((hfStep22Functor d.hf).fam (step22TripleOf T L₂ hL₂ hsnc₂) hcls₂).seqOn U₂ hU₂).pullback f₂ hf₂

The value of the family functor of Step 2.2 depends only on the sequence: for equal sequences the values at the triples of Step 2.2, read on corresponding opens along stageOfEq, correspond (a substitution; over data d).