Transport of a link along a value functor #
The argument, stated once, behind 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) for one link of a chain of Step 2 of
the proof of [Kol07, Theorem 103]: 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 (smaller opens V' ⊆ W', V ⊆ W with h(V') ⊆ V), whatever the value appended by the
link, as long as that value is read from a "value functor" with the two naturality properties: it
commutes with local analytic isomorphisms, and it does not see empty blow-ups. Here the value
functor is not fixed: the argument is stated for arbitrary appended values, the two naturality
properties entering as hypotheses on those values, and the three value functors of the
development are instances:
- the family of one boundary member at the induced triple (
ChainTransport.lean, the chain of Step 2.1); - the family functor of Step 2.2 at the triple of Step 2.2 (
Step2LinkTransport.lean, the link of Step 2.2); - an arbitrary family functor with the two naturality properties at the induced triple
(
Modified/InducedValueFunctor.lean, the rounds of the modified algorithm).
The argument, in two halves:
- The algebra of sequences (
BlowUpSequence.shrinkAppend_eraseEmpty_pullback): the shrink-and-append step ofL₂onNwith a valueF₂, with the empty blow-ups deleted and pulled back alongh|_{V'}, is the restricted sequence with the empty blow-ups deleted followed by the appended value transported to the common last stage (pullback_concat,eraseEmpty_concat,concat_map_stageOfEq,map_eq_pullback_symm), so the relation reduces to a comparison of the two appended values pulled back to that stage. - The comparison of the two appended values (
BlowUpSequence.valueTransport_rel): for valuesG₂on the reading open ofL₂,G₁on that ofL₁, given (i)G₂and the valueGPath^* L₁are the valuesGe₂,GePat the cleaned sequences transported alongeraseEmptyLast(the value functor ignores empty blow-ups;hA2,hA1), (ii)G₁pulled back along the restricted last-stage lift isGP(the value functor commutes with local isomorphisms;hFP), and (iii)Ge₂andGePagree under the identification of the cleaned sequences (a substitution alonghrel;hcongr, whose side conditionsmem_imageOpens_eraseEmptyLast_liftRange_iffandstageOfEq_eraseEmptyLast_liftCorestrict_applyare supplied), the two values pulled back to the common cleaned last stage agree. The maps are identified by the uniqueness of maps over the blow-down (eq_of_stageMap_last_comp_eq,LiftUnique.lean:liftCorestrict_pullbackLiftLast_comp_eq) and the opens bymem_liftRange_iff.
Over states of a chain (ChainState), the set-up of one link — the square of restrictions, the
identification of the two pull-backs of the sequence over W, the relation of the restricted
sequences, the triple over W' as a pull-back of the triple over W — is
ChainState.shrinkAppend_rel_of_value_rel and the lemmas before it: the relation is kept by the
shrink-and-append step as soon as the two appended values compare (hF).
The algebra of sequences #
theorem
AnalyticManifold.BlowUpSequence.shrinkAppend_eraseEmpty_pullback
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N P Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ : 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)
(F₁ : BlowUpSequence ψ₀ ((L₁.stage (Fin.last L₁.length)).restrict (L₁.liftRange ρ hρ)))
(F₂ : BlowUpSequence ψ₀ ((L₂.stage (Fin.last L₂.length)).restrict (L₂.liftRange ρ' hρ')))
(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
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap))
(hF :
(F₂.pullback (ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap)
hκ₂).eraseEmpty = (F₁.pullback
((ContMDiffMap.comp (L₁.liftCorestrict ρ hρ) ((L₁.pullback ρ hρ).pullbackLiftLast hV hhV)).comp
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap)
hκ₁).eraseEmpty)
:
The algebra of sequences of one link's transport: for sequences L₁ on M and L₂ on N
which agree, with the empty blow-ups deleted, after pulling L₁ back along hW : N → M, and for
the restrictions ρ : P → M, ρ' : Q → N, hV : Q → P forming a commuting square, the
shrink-and-append step of L₂ (with a value F₂ on its reading open), with the empty blow-ups
deleted, is the shrink-and-append step of L₁ (with F₁) pulled back along hV with the empty
blow-ups deleted, provided the two values agree after pulling back to the common last stage of the
restricted sequences with the empty blow-ups deleted (hF). e₀ identifies the two pull-backs of
L₁ to Q; hA the two restricted sequences.
theorem
AnalyticManifold.BlowUpSequence.stageMap_last_stageOfEq_symm
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
{L₁ L₂ : BlowUpSequence ψ₀ M}
(e : L₁ = L₂)
(q : (L₂.stage (Fin.last L₂.length)).carrier)
:
(L₁.toSuccession.stageMap (Fin.last L₁.toSuccession.length)) ((stageOfEq e).symm q) = (L₂.toSuccession.stageMap (Fin.last L₂.toSuccession.length)) q
stageMap_last_stageOfEq for the inverse isomorphism.
theorem
AnalyticManifold.BlowUpSequence.stageMap_last_eraseEmptyLast_symm
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M : AnalyticManifold 𝕜 E}
(L : BlowUpSequence ψ₀ M)
(q : (L.eraseEmpty.stage (Fin.last L.eraseEmpty.length)).carrier)
:
(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) (L.eraseEmptyLast.symm q) = (L.eraseEmpty.toSuccession.stageMap (Fin.last L.eraseEmpty.toSuccession.length)) q
stageMap_last_eraseEmptyLast for the inverse isomorphism.
theorem
AnalyticManifold.BlowUpSequence.image_liftRange_pullbackLiftLast_subset
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N P Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ : 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 ρ')
:
⇑(L₁.pullbackLiftLast hW hhW) '' ↑((L₁.pullback hW hhW).liftRange ρ' hρ') ⊆ ↑(L₁.liftRange ρ hρ)
The last-stage lift of hW carries the reading open of ρ' on the pulled-back sequence into
the reading open of ρ on the sequence, when ρ ∘ hV = hW ∘ ρ'.
theorem
Hironaka.Manifold.mem_imageOpens_toAnalyticMap_iff
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{X Y : AnalyticManifold 𝕜 E}
(e : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) X.carrier Y.carrier ⊤)
(O : TopologicalSpace.Opens X.carrier)
(p : Y.carrier)
:
Membership in the image of an open under an analytic isomorphism.
The comparison of the two appended values #
theorem
AnalyticManifold.BlowUpSequence.mem_imageOpens_eraseEmptyLast_liftRange_iff
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ' : AnalyticMap Q N)
(hρ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ')
(hrel : L₂.eraseEmpty = (L₁.pullback hW hhW).eraseEmpty)
(p : (L₂.eraseEmpty.stage (Fin.last L₂.eraseEmpty.length)).carrier)
:
p ∈ Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ') ↔ (stageOfEq hrel) p ∈ Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ')
The two image opens of the reading opens on the cleaned sequences correspond under the
identification stageOfEq hrel of the cleaned sequences (mem_liftRange_iff).
theorem
AnalyticManifold.BlowUpSequence.stageMap_last_stageOfEq_trans_eraseEmptyLast_symm
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ' : AnalyticMap Q N)
(hρ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ')
(hA : (L₂.pullback ρ' hρ').eraseEmpty = ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmpty)
(z : ((L₂.pullback ρ' hρ').eraseEmpty.stage (Fin.last (L₂.pullback ρ' hρ').eraseEmpty.length)).carrier)
:
(((L₁.pullback hW hhW).pullback ρ' hρ').toSuccession.stageMap
(Fin.last ((L₁.pullback hW hhW).pullback ρ' hρ').toSuccession.length))
(((stageOfEq hA).trans ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.symm) z) = ((L₂.pullback ρ' hρ').eraseEmpty.toSuccession.stageMap (Fin.last (L₂.pullback ρ' hρ').eraseEmpty.toSuccession.length))
z
The blow-down of the common cleaned last stage through the pull-back of L₁ to Q (hA
followed by eraseEmptyLast).
theorem
AnalyticManifold.BlowUpSequence.stageOfEq_eraseEmptyLast_liftCorestrict_apply
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ' : AnalyticMap Q N)
(hρ' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ρ')
(hrel : L₂.eraseEmpty = (L₁.pullback hW hhW).eraseEmpty)
(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))
(z : ((L₂.pullback ρ' hρ').eraseEmpty.stage (Fin.last (L₂.pullback ρ' hρ').eraseEmpty.length)).carrier)
:
(stageOfEq hrel)
↑((ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap L₂.eraseEmptyLast.toAnalyticMap (L₂.liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ')) ⋯)
(ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap))
z) = ↑((ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap
((L₁.pullback hW hhW).liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ'))
⋯)
(ContMDiffMap.comp ((L₁.pullback hW hhW).liftCorestrict ρ' hρ')
((stageOfEq hA).trans ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.symm).toAnalyticMap))
z)
The two transported maps into the cleaned reading opens agree under stageOfEq hrel: the
uniqueness of maps over the blow-down of the cleaned sequence (eq_of_stageMap_last_comp_eq).
theorem
AnalyticManifold.BlowUpSequence.liftCorestrict_pullbackLiftLast_comp_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N P Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ : 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 ρ')
(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ρ).pullbackLiftLast hV hhV)).comp
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap))
:
(ContMDiffMap.comp (L₁.liftCorestrict ρ hρ) ((L₁.pullback ρ hρ).pullbackLiftLast hV hhV)).comp
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap = ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullbackLiftLast hW hhW) ((L₁.pullback hW hhW).liftRange ρ' hρ')
(L₁.liftRange ρ hρ) ⋯)
(ContMDiffMap.comp ((L₁.pullback hW hhW).liftCorestrict ρ' hρ')
((stageOfEq hA).trans ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.symm).toAnalyticMap)
The restricted map into the reading open of ρ factors through the last-stage lift of
hW: the uniqueness of maps over the blow-down of L₁ (eq_of_stageMap_last_comp_eq).
theorem
AnalyticManifold.BlowUpSequence.valueTransport_rel
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N P Q : AnalyticManifold 𝕜 E}
(L₁ : BlowUpSequence ψ₀ M)
(L₂ : BlowUpSequence ψ₀ N)
(hW : AnalyticMap N M)
(hhW : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑hW)
(ρ : 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 ρ')
(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
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap))
{G₂ : BlowUpSequence ψ₀ ((L₂.stage (Fin.last L₂.length)).restrict (L₂.liftRange ρ' hρ'))}
{G₁ : BlowUpSequence ψ₀ ((L₁.stage (Fin.last L₁.length)).restrict (L₁.liftRange ρ hρ))}
{GP :
BlowUpSequence ψ₀
(((L₁.pullback hW hhW).stage (Fin.last (L₁.pullback hW hhW).length)).restrict
((L₁.pullback hW hhW).liftRange ρ' hρ'))}
{Ge₂ :
BlowUpSequence ψ₀
((L₂.eraseEmpty.stage (Fin.last L₂.eraseEmpty.length)).restrict
(Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ')))}
{GeP :
BlowUpSequence ψ₀
(((L₁.pullback hW hhW).eraseEmpty.stage (Fin.last (L₁.pullback hW hhW).eraseEmpty.length)).restrict
(Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ')))}
(hA2 :
G₂ = (Ge₂.pullback
(Hironaka.Manifold.AnalyticMap.restrictMap L₂.eraseEmptyLast.toAnalyticMap (L₂.liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ')) ⋯)
⋯).eraseEmpty)
(hA1 :
GP = (GeP.pullback
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap
((L₁.pullback hW hhW).liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ'))
⋯)
⋯).eraseEmpty)
(hFP :
(G₁.pullback
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullbackLiftLast hW hhW) ((L₁.pullback hW hhW).liftRange ρ' hρ')
(L₁.liftRange ρ hρ) ⋯)
⋯).eraseEmpty = GP)
(hcongr :
∀
(hf₁ :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤
⇑(ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap L₂.eraseEmptyLast.toAnalyticMap (L₂.liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ')) ⋯)
(ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap)))
(hf₂ :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤
⇑(ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap
((L₁.pullback hW hhW).liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ'))
⋯)
(ContMDiffMap.comp ((L₁.pullback hW hhW).liftCorestrict ρ' hρ')
((stageOfEq hA).trans ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.symm).toAnalyticMap))),
Ge₂.pullback
(ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap L₂.eraseEmptyLast.toAnalyticMap (L₂.liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens L₂.eraseEmptyLast.toAnalyticMap ⋯ (L₂.liftRange ρ' hρ')) ⋯)
(ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap))
hf₁ = GeP.pullback
(ContMDiffMap.comp
(Hironaka.Manifold.AnalyticMap.restrictMap (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap
((L₁.pullback hW hhW).liftRange ρ' hρ')
(Hironaka.Manifold.AnalyticMap.imageOpens (L₁.pullback hW hhW).eraseEmptyLast.toAnalyticMap ⋯
((L₁.pullback hW hhW).liftRange ρ' hρ'))
⋯)
(ContMDiffMap.comp ((L₁.pullback hW hhW).liftCorestrict ρ' hρ')
((stageOfEq hA).trans ((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.symm).toAnalyticMap))
hf₂)
:
(G₂.pullback (ContMDiffMap.comp (L₂.liftCorestrict ρ' hρ') (L₂.pullback ρ' hρ').eraseEmptyLast.symm.toAnalyticMap)
hκ₂).eraseEmpty = (G₁.pullback
((ContMDiffMap.comp (L₁.liftCorestrict ρ hρ) ((L₁.pullback ρ hρ).pullbackLiftLast hV hhV)).comp
((stageOfEq e₀).trans
(((L₁.pullback hW hhW).pullback ρ' hρ').eraseEmptyLast.trans (stageOfEq ⋯))).symm.toAnalyticMap)
hκ₁).eraseEmpty
The transport of a link's value, the heart of the transport of a chain, for arbitrary
appended values: for sequences L₂ on N and L₁ on M whose restrictions agree, with the
empty blow-ups deleted, after pulling L₁ back along hW (hA), a value G₂ on the reading
open of ρ' on L₂ and a value G₁ on the reading open of ρ on L₁, both pulled back to the
common cleaned last stage of the restricted sequences and with the empty blow-ups deleted, agree,
provided
G₂and the valueGPon the reading open ofρ'onhW^* L₁are the valuesGe₂,GePon the cleaned sequences transported alongeraseEmptyLastand cleaned (the value functor ignores empty blow-ups;hA2,hA1);G₁pulled back along the restricted last-stage lift ofhWand cleaned isGP(the value functor commutes with local analytic isomorphisms;hFP);Ge₂andGeP, pulled back to the common cleaned stage, agree (hcongr; in the instances a substitution along the relationhrelof the cleaned sequences, the opens corresponding bymem_imageOpens_eraseEmptyLast_liftRange_iffand the maps bystageOfEq_eraseEmptyLast_liftCorestrict_apply).
The maps are identified by the uniqueness of maps over the blow-down
(liftCorestrict_pullbackLiftLast_comp_eq).
The set-up of one link over states of a chain #
theorem
Hironaka.Manifold.ChainState.triple_pullback_restrictMap_eq
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
:
The triple over W' is the pull-back of the triple over W along h|_{W'}.
theorem
Hironaka.Manifold.ChainState.boClass_triple_pullback_restrictMap
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(s : ℕ)
(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)
:
Manifold.AnalyticTriple.BOClass s ((T.pullback (M.inclusion W) ⋯).pullback (AnalyticMap.restrictMap h W' W hWW') ⋯)
The class of the triple over W, pulled back along h|_{W'}, from the class of the pulled-back
triple.
theorem
Hironaka.Manifold.ChainState.isOfOrderGe_triple_pullback_restrictMap
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
(T : Manifold.AnalyticTriple ψ₀ M)
(s : ℕ)
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
(st' : ChainState (T.pullback h hh) s W')
:
st'.L.toSuccession.IsOfOrderGe ((T.pullback (M.inclusion W) ⋯).pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).I s
((T.pullback (M.inclusion W) ⋯).pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).F.idealSheaf
The order clause of a state over W' for the pulled-back triple, read at the triple over W
pulled back along h|_{W'}.
theorem
Hironaka.Manifold.ChainState.restrictLE_comp_restrictMap
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{M N : AnalyticManifold 𝕜 E}
(h : AnalyticMap N M)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
{V : TopologicalSpace.Opens M.carrier}
(hVW : closure ↑V ⊆ ↑W)
{V' : TopologicalSpace.Opens N.carrier}
(hV'W' : closure ↑V' ⊆ ↑W')
(hVV' : ⇑h '' ↑V' ⊆ ↑V)
:
ContMDiffMap.comp (M.restrictLE ⋯) (AnalyticMap.restrictMap h V' V hVV') = ContMDiffMap.comp (AnalyticMap.restrictMap h W' W hWW') (N.restrictLE ⋯)
The square of restrictions: V ⊆ W after h|_{V'} is h|_{W'} after V' ⊆ W'.
theorem
Hironaka.Manifold.ChainState.pullback_restrictLE_pullback_restrictMap
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
{T : Manifold.AnalyticTriple ψ₀ M}
{s : ℕ}
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
{V : TopologicalSpace.Opens M.carrier}
(hVW : closure ↑V ⊆ ↑W)
{V' : TopologicalSpace.Opens N.carrier}
(hV'W' : closure ↑V' ⊆ ↑W')
(hVV' : ⇑h '' ↑V' ⊆ ↑V)
(st : ChainState T s W)
:
(st.L.pullback (M.restrictLE ⋯) ⋯).pullback (AnalyticMap.restrictMap h V' V hVV') ⋯ = (st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).pullback (N.restrictLE ⋯) ⋯
The two pull-backs of the sequence over W to V' agree (e₀ of the transport).
theorem
Hironaka.Manifold.ChainState.eraseEmpty_pullback_restrictLE
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
{T : Manifold.AnalyticTriple ψ₀ M}
{s : ℕ}
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
{V' : TopologicalSpace.Opens N.carrier}
(hV'W' : closure ↑V' ⊆ ↑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)
:
(st'.L.pullback (N.restrictLE ⋯) ⋯).eraseEmpty = ((st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).pullback (N.restrictLE ⋯) ⋯).eraseEmpty
The relation of the sequences over W' and W restricts to V' (hA of the transport).
theorem
Hironaka.Manifold.ChainState.shrinkAppend_rel_of_value_rel
{𝕜 : Type}
[RCLike 𝕜]
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ}
{ψ₀ : E ≃L[𝕜] Fin n → 𝕜}
{M N : AnalyticManifold 𝕜 E}
{T : Manifold.AnalyticTriple ψ₀ M}
{s : ℕ}
(h : AnalyticMap N M)
(hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h)
{W : TopologicalSpace.Opens M.carrier}
{W' : TopologicalSpace.Opens N.carrier}
(hWW' : ⇑h '' ↑W' ⊆ ↑W)
{V : TopologicalSpace.Opens M.carrier}
(hVW : closure ↑V ⊆ ↑W)
{V' : TopologicalSpace.Opens N.carrier}
(hV'W' : closure ↑V' ⊆ ↑W')
(hVV' : ⇑h '' ↑V' ⊆ ↑V)
(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)
(F :
AnalyticManifold.BlowUpSequence ψ₀ ((st.L.stage (Fin.last st.L.length)).restrict (st.L.liftRange (M.restrictLE ⋯) ⋯)))
(F' :
AnalyticManifold.BlowUpSequence ψ₀
((st'.L.stage (Fin.last st'.L.length)).restrict (st'.L.liftRange (N.restrictLE ⋯) ⋯)))
(hF :
∀
(hκ₂ :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤
⇑(ContMDiffMap.comp (st'.L.liftCorestrict (N.restrictLE ⋯) ⋯)
(st'.L.pullback (N.restrictLE ⋯) ⋯).eraseEmptyLast.symm.toAnalyticMap))
(hκ₁ :
IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤
⇑((ContMDiffMap.comp (st.L.liftCorestrict (M.restrictLE ⋯) ⋯)
((st.L.pullback (M.restrictLE ⋯) ⋯).pullbackLiftLast (AnalyticMap.restrictMap h V' V hVV') ⋯)).comp
((AnalyticManifold.BlowUpSequence.stageOfEq ⋯).trans
(((st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).pullback (N.restrictLE ⋯)
⋯).eraseEmptyLast.trans
(AnalyticManifold.BlowUpSequence.stageOfEq ⋯))).symm.toAnalyticMap)),
(F'.pullback
(ContMDiffMap.comp (st'.L.liftCorestrict (N.restrictLE ⋯) ⋯)
(st'.L.pullback (N.restrictLE ⋯) ⋯).eraseEmptyLast.symm.toAnalyticMap)
hκ₂).eraseEmpty = (F.pullback
((ContMDiffMap.comp (st.L.liftCorestrict (M.restrictLE ⋯) ⋯)
((st.L.pullback (M.restrictLE ⋯) ⋯).pullbackLiftLast (AnalyticMap.restrictMap h V' V hVV') ⋯)).comp
((AnalyticManifold.BlowUpSequence.stageOfEq ⋯).trans
(((st.L.pullback (AnalyticMap.restrictMap h W' W hWW') ⋯).pullback (N.restrictLE ⋯)
⋯).eraseEmptyLast.trans
(AnalyticManifold.BlowUpSequence.stageOfEq ⋯))).symm.toAnalyticMap)
hκ₁).eraseEmpty)
:
(st'.L.shrinkAppend (N.restrictLE ⋯) ⋯ F').eraseEmpty = ((st.L.shrinkAppend (M.restrictLE ⋯) ⋯ F).pullback (AnalyticMap.restrictMap h V' V hVV') ⋯).eraseEmpty
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" is kept by the shrink-and-append step with
values F' over W' and F over W, for smaller opens V ⊆ W, V' ⊆ W' with h(V') ⊆ V, as
soon as the two values agree after pulling back to the common cleaned last stage of the
restricted sequences (hF, for the identifications pullback_restrictLE_pullback_restrictMap
and eraseEmpty_pullback_restrictLE). The algebra of sequences is
shrinkAppend_eraseEmpty_pullback.