The shrinking chain of Step 2.1 in the compatible-family form: general tools

In the compatible-family form of the order-reduction functors ([Wlo09, Theorem 2.0.3 (1), (4)]; the remark after [BM97, Theorem 1.6] on locally finite sequences), the value of Step 2.1 of the proof of [Kol07, Theorem 103] on a relatively compact open U is computed along a finite shrinking chain U ⊆ W_r ⋐ ⋯ ⋐ W_0 ⊆ M of relatively compact opens, each with closure in the previous one. Each factor (Lemma 102's family at one boundary member, later Step 2.2) is a compatible family on the induced triple at the last stage of the sequence built so far, and can only be read on a relatively compact open of that last stage; the preimage of the next, smaller open of the chain is such an open, by the properness of the composite blow-down. The sequence built so far is then restricted to the smaller open (pulled back along the open inclusion), the factor's value is carried to the restricted sequence's last stage along the lift of the inclusion, and the two are concatenated. This module holds the general pieces of that step:

• AnalyticMap.corestrict f V h — the corestriction of an analytic map onto an open V containing its range, a local analytic isomorphism when f is (isLocalDiffeomorph_corestrict) and surjective when the range is V (surjective_corestrict);
• FiniteSuccession.isProperMap_stageMap — the composite blow-down of a finite succession of blow-ups is proper, so the preimage of a relatively compact open is relatively compact;
• BlowUpSequence.stageMap_last_pullbackLiftLast, range_pullbackLiftLast_subset — the last-stage lift of a local analytic isomorphism h along a sequence of centres lies over h (σ^r ∘ h_r = h ∘ σ'^r, the pull-back of blow-up sequences of [Kol07, Definition 30 (30.1)] composed along the sequence), so its range lies in the preimage of the range of h;
• BlowUpSequence.liftRange, isCompact_closure_liftRange, liftCorestrict — the reading open, the range of the last-stage lift of h on the last stage of L, relatively compact when the range of h is, and the lift corestricted onto it (a surjective local analytic isomorphism);
• BlowUpSequence.shrinkAppend L h hh L' — the shrink-and-append step: the pull-back of L along h, followed by a sequence L' on the reading open carried along the corestricted lift;
• AnalyticTriple.boClass_pullback_of_isLocalDiffeomorph, BlowUpSequence.stage_last_concat — the class BOClass m is stable under pull-back of the triple along a local analytic isomorphism, and the last stage of a concatenation is that of the second sequence.

The order clause of the step is proved in FamilyOrder.lean; the chain itself is built in Step21Fam.lean, and the same step drives the construction of Theorem 107 in the compatible-family form (ChainState.linkWith, Step21Fam.lean).

Corestriction onto an open containing the range

def Hironaka.Manifold.AnalyticMap.corestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (V : TopologicalSpace.Opens M.carrier) (h : Set.range ⇑f ⊆ ↑V) : AnalyticMap N (M.restrict V)

The corestriction of an analytic map f : N → M onto an open V ⊇ range f, as an analytic map N → M.restrict V.

Equations

• Hironaka.Manifold.AnalyticMap.corestrict f V h = ⟨fun (p : N.carrier) => ⟨f p, ⋯⟩, ⋯⟩

@[simp]

theorem Hironaka.Manifold.AnalyticMap.corestrict_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (V : TopologicalSpace.Opens M.carrier) (h : Set.range ⇑f ⊆ ↑V) (p : N.carrier) : (M.inclusion V) ((corestrict f V h) p) = f p

theorem Hironaka.Manifold.isLocalDiffeomorph_corestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (V : TopologicalSpace.Opens M.carrier) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (h : Set.range ⇑f ⊆ ↑V) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(AnalyticMap.corestrict f V h)

The corestriction of a local analytic isomorphism is a local analytic isomorphism (it factors as (M.inclusion V)⁻¹ ∘ f, inclusionInv being the local inverse of the open inclusion).

theorem Hironaka.Manifold.surjective_corestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (V : TopologicalSpace.Opens M.carrier) (h' : Set.range ⇑f = ↑V) : Function.Surjective ⇑(AnalyticMap.corestrict f V ⋯)

The corestriction onto the range is surjective.

The composite blow-downs are proper

theorem AnalyticManifold.FiniteSuccession.isProperMap_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : IsProperMap ⇑(S.map i)

Every monoidal transformation of a succession is a blow-up, hence proper (IsBlowUp.isProperMap).

theorem AnalyticManifold.FiniteSuccession.isProperMap_stageMapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : ℕ) (h : i < S.length + 1) : IsProperMap ⇑(S.stageMapAux i h)

The composite blow-down σ^i : U_i → M is proper, by composition.

theorem AnalyticManifold.FiniteSuccession.isProperMap_stageMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin (S.length + 1)) : IsProperMap ⇑(S.stageMap i)

The composite blow-down of a finite succession is proper: the preimage of a relatively compact open is relatively compact. This is what makes the compatible-family form work over a neighbourhood of every compact set ([Wlo09, Theorem 2.0.3 (1)]).

The last-stage lift lies over the local isomorphism

theorem AnalyticManifold.BlowUpSequence.stageMap_last_pullbackLiftLast {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (q : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier) : (L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ((L.pullbackLiftLast h hh) q) = h (((L.pullback h hh).toSuccession.stageMap (Fin.last (L.pullback h hh).toSuccession.length)) q)

The last-stage lift of a local analytic isomorphism h lies over h: σ^r ∘ h_r = h ∘ σ'^r. One blow-up at a time, the lift of h to the blow-ups satisfies π ∘ h₁ = h ∘ π' (blowUpπ_liftStep, the pull-back of a blow-up along h in the sense of [Kol07, Definition 30 (30.1)]); the equation composes along the sequence.

theorem AnalyticManifold.BlowUpSequence.range_pullbackLiftLast_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Set.range ⇑(L.pullbackLiftLast h hh) ⊆ ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Set.range ⇑h

The range of the last-stage lift lies in the preimage of the range of h.

The reading open and the shrink-and-append step

noncomputable def AnalyticManifold.BlowUpSequence.liftRange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : TopologicalSpace.Opens (L.stage (Fin.last L.length)).carrier

The reading open of the chain: the range of the last-stage lift of h, an open of the last stage of L (a local analytic isomorphism has open range). The next factor of the chain is read on it.

Equations

• L.liftRange h hh = { carrier := Set.range ⇑(L.pullbackLiftLast h hh), is_open' := ⋯ }

theorem AnalyticManifold.BlowUpSequence.isCompact_closure_liftRange {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hc : IsCompact (closure (Set.range ⇑h))) : IsCompact (closure ↑(L.liftRange h hh))

The reading open is relatively compact when the range of h is: it lies in the preimage of range h under the proper composite blow-down.

noncomputable def AnalyticManifold.BlowUpSequence.liftCorestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : AnalyticMap ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)) ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh))

The last-stage lift corestricted onto the reading open: a surjective local analytic isomorphism from the last stage of h^* L onto the reading open of the last stage of L.

Equations

• L.liftCorestrict h hh = Hironaka.Manifold.AnalyticMap.corestrict (L.pullbackLiftLast h hh) (L.liftRange h hh) ⋯

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_liftCorestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(L.liftCorestrict h hh)

theorem AnalyticManifold.BlowUpSequence.surjective_liftCorestrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Function.Surjective ⇑(L.liftCorestrict h hh)

noncomputable def AnalyticManifold.BlowUpSequence.shrinkAppend {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (L' : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh))) : BlowUpSequence ψ₀ N

The shrink-and-append step of the chain: the sequence L restricted along h (its pull-back), followed by a sequence L' on the reading open carried to the restricted sequence's last stage along the corestricted lift.

Equations

• L.shrinkAppend h hh L' = (L.pullback h hh).concat (L'.pullback (L.liftCorestrict h hh) ⋯)

The class of BO_{n,m} is closed under pull-back along local analytic isomorphisms

theorem Manifold.AnalyticTriple.boClass_pullback_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : AnalyticTriple ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {m : ℕ} (hT : BOClass m T) : BOClass m (T.pullback h hh)

The class BOClass m is stable under pull-back of the triple along an arbitrary local analytic isomorphism h (the form of AnalyticTriple.boClass_of_isPullbackOf of ClassPullback.lean for the pull-back triple T.pullback h hh itself): the order bound pulls back pointwise and a member of the pulled-back family is nonempty only if the member is. The triples carried along the chain are pull-backs of induced triples along the lifts, whose class membership this supplies.

The last stage of a concatenation

theorem AnalyticManifold.BlowUpSequence.stage_last_concat {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (L' : BlowUpSequence ψ₀ (L.stage (Fin.last L.length))) : (L.concat L').stage (Fin.last (L.concat L').length) = L'.stage (Fin.last L'.length)

The last stage of a concatenation is the last stage of the second list (definitionally at each constructor; the lemma is the induction).