The link of Step 2.2 along a local analytic isomorphism

ChainTransport.lean transports one link of the chain of Step 2.1 along a local analytic isomorphism h with h(W') ⊆ W: the relation "the sequence over W' with its empty blow-ups deleted is the pull-back of the sequence over W with its empty blow-ups deleted" is preserved by a link. Step 2 appends one more link, the value of the family functor of Step 2.2 at the triple of Step 2.2 over the chain's sequence, read on the lifted range of the last restriction (step22FamOn; over a state of the chain, hfStep22ValueOf of Step2Along.lean). This module is the same transport for that link, an instance of the general transport of a link along a value functor (ValueTransport.lean) for the value functor "the family functor of Step 2.2 at the triple of Step 2.2"; it is what makes the value of Step 2 independent of the chain of opens (Step2Assembly.lean) and commute with local analytic isomorphisms (Step2AssemblyComm.lean), the analytic form of the functoriality clause of Step 2.3 of the proof of Theorem 103 ([Kol07, 104, Step 2.3]; [Kol07, 34.1]).

• BO.hfStep22Value_rel — the comparison of the two appended values: BlowUpSequence.valueTransport_rel with the naturality of the value functor supplied by hfStep22Fam_seqOn_eraseEmpty, hfStep22Fam_seqOn_pullback_liftRange and hfStep22Fam_seqOn_congr of Step2LinkPrep.lean (in place of fam_seqOn_induced_eraseEmpty, fam_seqOn_induced_pullback_liftRange, fam_seqOn_induced_pullback_congr of linkValue_rel);
• BO.hfStep22Link_rel — the relation is preserved by the link of Step 2.2 (ChainState.shrinkAppend_rel_of_value_rel, the value over W' read at the pulled-back triple by hfStep22Fam_seqOn_congr_triple).

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_congr_triple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} (d : HFData ψ₀ s) {X : AnalyticManifold 𝕜 E} {X₁ X₂ : Manifold.AnalyticTriple ψ₀ X} (e : X₁ = X₂) (h₁ : stepHClass s X₁) (h₂ : stepHClass s X₂) (U : TopologicalSpace.Opens X.carrier) (hU : IsCompact (closure ↑U)) : ((hfStep22Functor d.hf).fam X₁ h₁).seqOn U hU = ((hfStep22Functor d.hf).fam X₂ h₂).seqOn U hU

The value of the family functor of Step 2.2 depends only on the triple (a substitution; over data d).

theorem Hironaka.Manifold.BO.step22TripleOf_congr_triple {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {X : AnalyticManifold 𝕜 E} {T₁ T₂ : Manifold.AnalyticTriple ψ₀ X} (e : T₁ = T₂) {H : Set X.carrier} (L : AnalyticManifold.BlowUpSequence ψ₀ X) (hL₁ : L.toSuccession.IsOfOrderGe T₁.I s T₁.F.idealSheaf) (hL₂ : L.toSuccession.IsOfOrderGe T₂.I s T₂.F.idealSheaf) (hsnc₁ hsnc₂ : Manifold.HypersurfaceFamily.IsSnc ψ₀ ((exceptionalOf L).append (transformHOf L H))) : step22TripleOf T₁ L hL₁ hsnc₁ = step22TripleOf T₂ L hL₂ hsnc₂

The triple of Step 2.2 depends only on the triple and the sequence (a substitution).

theorem Hironaka.Manifold.BO.hfStep22Value_rel {𝕜 : 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) (hT₁ : Manifold.AnalyticTriple.BOClass s T₁) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T₁.I (s - 1)) (hW : AnalyticMap N M) (hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW) (hT₂ : Manifold.AnalyticTriple.BOClass s (T₁.pullback hW hhW)) (L₁ : AnalyticManifold.BlowUpSequence ψ₀ M) (hL₁ : L₁.toSuccession.IsOfOrderGe T₁.I s T₁.F.idealSheaf) (ρ : AnalyticMap P M) (hρ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ) (ρ' : AnalyticMap Q N) (hρ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ') (hV : AnalyticMap Q P) (hhV : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hV) (hsq : ContMDiffMap.comp ρ hV = ContMDiffMap.comp hW ρ') (L₂ : AnalyticManifold.BlowUpSequence ψ₀ N) (hL₂ : L₂.toSuccession.IsOfOrderGe (T₁.pullback hW hhW).I s (T₁.pullback hW hhW).F.idealSheaf) (hrel : L₂.eraseEmpty = (L₁.pullback hW hhW).eraseEmpty) (hO₁ : IsCompact (closure ↑(L₁.liftRange ρ hρ))) (hO₂ : IsCompact (closure ↑(L₂.liftRange ρ' hρ'))) (hρ'c : IsCompact (closure (Set.range ⇑ρ'))) (e₀ : (L₁.pullback ρ hρ).pullback hV hhV = (L₁.pullback hW hhW).pullback ρ' hρ') (hA : (L₂.pullback ρ' hρ').eraseEmpty = ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmpty) (hκ₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap)) (hκ₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑((ContMDiffMap.comp (L₁.liftCorestrict ρ hρ) ((L₁.pullback ρ hρ).pullbackLiftLast hV hhV)).comp ((AnalyticManifold.BlowUpSequence.stageOfEq e₀).trans (((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (AnalyticManifold.BlowUpSequence.stageOfEq ⋯))).symm.toAnalyticMap)) : ((((hfStep22Functor d.hf).fam (step22TripleOf (T₁.pullback hW hhW) L₂ hL₂ ⋯) ⋯).seqOn (L₂.liftRange ρ' hρ') hO₂).pullback (ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap) hκ₂).eraseEmpty = ((((hfStep22Functor d.hf).fam (step22TripleOf T₁ L₁ hL₁ ⋯) ⋯).seqOn (L₁.liftRange ρ hρ) hO₁).pullback ((ContMDiffMap.comp (L₁.liftCorestrict ρ hρ) ((L₁.pullback ρ hρ).pullbackLiftLast hV hhV)).comp ((AnalyticManifold.BlowUpSequence.stageOfEq e₀).trans (((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (AnalyticManifold.BlowUpSequence.stageOfEq ⋯))).symm.toAnalyticMap) hκ₁).eraseEmpty

The comparison of the two appended values of Step 2.2 (linkValue_rel for the link of Step 2.2; over data d): for sequences L₂ on N and L₁ on M whose cleaned forms agree after pulling L₁ back along hW, the value of the family functor of Step 2.2 at the triple of Step 2.2 over L₂ on the reading open of ρ', and its value at the triple of Step 2.2 over L₁ on the reading open of ρ, both pulled back to the common cleaned last stage of the restricted sequences and with their empty blow-ups deleted, agree. The general valueTransport_rel with the naturality of the value functor: hfStep22Fam_seqOn_eraseEmpty (both are the value at the triple of Step 2.2 over the common cleaned sequence), hfStep22Fam_seqOn_pullback_liftRange (on the L₁ side) and hfStep22Fam_seqOn_congr (the substitution along hrel).

theorem Hironaka.Manifold.BO.hfStep22Link_rel {𝕜 : 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) (hT : Manifold.AnalyticTriple.BOClass s T) {H : Set M.carrier} (hH : Manifold.IsClosedSubmanifold ψ₀ H 1) (hle : hH.idealSheaf ≤ Manifold.IdealSheaf.iteratedDeriv T.I (s - 1)) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hT' : Manifold.AnalyticTriple.BOClass s (T.pullback h hh)) {W : TopologicalSpace.Opens M.carrier} {W' : TopologicalSpace.Opens N.carrier} (hWW' : ⇑h '' ↑W' ⊆ ↑W) (st : ChainState T s W) (st' : ChainState (T.pullback h hh) s W') (hrel : st'.L.eraseEmpty = (st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).eraseEmpty) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) {V' : TopologicalSpace.Opens N.carrier} (hV' : IsCompact (closure ↑V')) (hV'W' : closure ↑V' ⊆ ↑W') (hVV' : ⇑h '' ↑V' ⊆ ↑V) : (st'.L.shrinkAppend (N.restrictLE ⋯) ⋯ (hfStep22ValueOf d (T.pullback h hh) hT' ⋯ ⋯ st' hV' hV'W')).eraseEmpty = ((st.L.shrinkAppend (M.restrictLE ⋯) ⋯ (hfStep22ValueOf d T hT hH hle st hV hVW)).pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

The relation "the sequence over W' with its empty blow-ups deleted is the pull-back of the sequence over W with its empty blow-ups deleted", along a local analytic isomorphism h with h(W') ⊆ W, is preserved by the link of Step 2.2, for smaller opens V ⊆ W, V' ⊆ W' with h(V') ⊆ V ([Kol07, 34.1]; link_rel for this link; over data d). The general ChainState.shrinkAppend_rel_of_value_rel; the two appended values are compared by hfStep22Value_rel after reading the value over W' at the pulled-back triple (hfStep22Fam_seqOn_congr_triple).