Transport of one link of the chain of Step 2.1

The second clause of [Kol07, 34.1] (the value on a pull-back is the pull-back of the value with the empty blow-ups deleted) and the compatibility of [Wlo09, Theorem 2.0.3 (4)], for the chain of Step 2.1 of the proof of [Kol07, Theorem 103] in the compatible-family form (Step21Fam.lean): along a local analytic isomorphism h : N → M carrying an open W' ⊆ N into W ⊆ M, a chain state over W' for the pulled-back triple and a chain state over W whose sequences agree up to empty blow-ups after pulling back keep that relation through one link (the same member j, smaller opens V' ⊆ W', V ⊆ W with h(V') ⊆ V).

This is an instance of the general transport of a link along a value functor (ValueTransport.lean), for the value functor "the family of one boundary member bd read at the induced triple of the sequence, at the member's index" (ChainState.linkValue):

• BDanFamData.fam_seqOn_induced_pullback_liftRange — the value functor commutes with local analytic isomorphisms, on the reading opens (fam_seqOn_induced_pullback on the image open, then the family's compat);
• BDanFamData.linkValue_rel — the comparison of the two appended values, BlowUpSequence.valueTransport_rel with the naturality of the value functor supplied by fam_seqOn_induced_eraseEmpty (it ignores empty blow-ups), fam_seqOn_induced_pullback_liftRange and fam_seqOn_induced_pullback_congr (a substitution);
• ChainState.link_rel — the relation is kept by one link (ChainState.link), ChainState.shrinkAppend_rel_of_value_rel with the two values compared by linkValue_rel after reading the value over W' at the pulled-back triple (fam_seqOn_congr).

The transport is applied to two chains of opens over the same manifold in ChainIndep.lean and along a local analytic isomorphism in Step21FamIndep.lean.

theorem Hironaka.Manifold.BDanFamData.fam_seqOn_induced_pullback_liftRange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {s : ℕ} (bd : BDanFamData ψ₀ s) {M N P Q : AnalyticManifold 𝕜 E} (T₁ : Manifold.AnalyticTriple ψ₀ M) (hT₁ : Manifold.AnalyticTriple.BOClass s T₁) (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) (j : T₁.F.ι) (ρ : 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ρ'))) : (((bd.fam (T₁.induced s L₁ hL₁) ⋯ (L₁.toSuccession.originalIdx T₁.F (Fin.last L₁.toSuccession.length) j)).seqOn (L₁.liftRange ρ hρ) hO₁).pullback (AnalyticMap.restrictMap (L₁.pullbackLiftLast hW hhW) ((L₁.pullback hW hhW).liftRange ρ' hρ') (L₁.liftRange ρ hρ) ⋯) ⋯).eraseEmpty = (bd.fam ((T₁.pullback hW hhW).induced s (L₁.pullback hW hhW) ⋯) ⋯ ((L₁.pullback hW hhW).toSuccession.originalIdx (T₁.pullback hW hhW).F (Fin.last (L₁.pullback hW hhW).toSuccession.length) j)).seqOn ((L₁.pullback hW hhW).liftRange ρ' hρ') hOP

The value at the pulled-back sequence is the value at the sequence pulled back along the lift, on the reading opens: the family's value at the induced triple of hW^* L₁ on the reading open of ρ' is the value at the induced triple of L₁ on the reading open of ρ, pulled back along the restricted last-stage lift, with the empty blow-ups deleted (fam_seqOn_induced_pullback on the image open, then the family's compat to the reading open of ρ).

theorem Hironaka.Manifold.BDanFamData.linkValue_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {s : ℕ} (bd : BDanFamData ψ₀ s) {M N P Q : AnalyticManifold 𝕜 E} (T₁ : Manifold.AnalyticTriple ψ₀ M) (hT₁ : Manifold.AnalyticTriple.BOClass s T₁) (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) (j : T₁.F.ι) (ρ : 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)) : (((bd.fam ((T₁.pullback hW hhW).induced s L₂ hL₂) ⋯ (L₂.toSuccession.originalIdx (T₁.pullback hW hhW).F (Fin.last L₂.toSuccession.length) j)).seqOn (L₂.liftRange ρ' hρ') hO₂).pullback (ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap) hκ₂).eraseEmpty = (((bd.fam (T₁.induced s L₁ hL₁) ⋯ (L₁.toSuccession.originalIdx T₁.F (Fin.last L₁.toSuccession.length) j)).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, the heart of the transport of the chain: for sequences L₂ on N and L₁ on M which agree, with the empty blow-ups deleted, after pulling L₁ back along hW, the family's value at the induced triple of L₂ on the reading open of ρ' and its value at the induced triple of L₁ on the reading open of ρ, both pulled back to the common last stage of the restricted sequences and with the empty blow-ups deleted, agree. The general valueTransport_rel with the naturality of the value functor: fam_seqOn_induced_eraseEmpty (both are the value at the induced triple of the common cleaned sequence), fam_seqOn_induced_pullback_liftRange (on the L₁ side) and fam_seqOn_induced_pullback_congr (the substitution along hrel).

noncomputable def Hironaka.Manifold.ChainState.linkValue {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) (j : T.F.ι) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : AnalyticManifold.BlowUpSequence ψ₀ ((st.L.stage (Fin.last st.L.length)).restrict (st.L.liftRange (M.restrictLE ⋯) ⋯))

The value appended by one link of the chain of Step 2.1: the family read at the induced triple of the state's sequence, at the member's index, on the reading open (the local definitions of ChainState.link).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.ChainState.link_L {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) {W : TopologicalSpace.Opens M.carrier} (st : ChainState T s W) (j : T.F.ι) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) : (link T s bd hT st j hV hVW).L = st.L.shrinkAppend (M.restrictLE ⋯) ⋯ (linkValue T s bd hT st j hV hVW)

One link is the shrink-and-append step with the link's value.

theorem Hironaka.Manifold.ChainState.link_rel {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (bd : BDanFamData ψ₀ s) (hT : Manifold.AnalyticTriple.BOClass s T) (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) (j : T.F.ι) {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) : (link (T.pullback h hh) s bd hT' st' j hV' hV'W').L.eraseEmpty = ((link T s bd hT st j hV hVW).L.pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty

The second clause of [Kol07, 34.1] for one link of the chain of Step 2.1: the relation "the sequence over W' with the empty blow-ups deleted is the pull-back of the sequence over W with the empty blow-ups deleted" along a local analytic isomorphism h with h(W') ⊆ W is kept by one link at a member j, for smaller opens V ⊆ W, V' ⊆ W' with h(V') ⊆ V. The general shrinkAppend_rel_of_value_rel, the two appended values compared by linkValue_rel (the family's commutesWithLocalIsos and compat at the induced triples, the common sequence, the uniqueness of maps over the blow-down) after reading the value over W' at the pulled-back triple (triple_pullback_restrictMap_eq, fam_seqOn_congr).