The stage lifts of a pull-back, stage by stage

For a list of centres L on M and a local analytic isomorphism h : N → M, the stages of the pull-back h^* L come with the lifts h_i : N_i → M_i (pullbackLift), the squares π ∘ h_{i+1} = h_i ∘ π' of [Kol07, Definition 30, 30.1]. The lifts are local analytic isomorphisms, surjective when h is, and the centres of h^* L are the preimages of those of L under them (Hironaka.Resolution.Analytic.Functor.PullbackSequence); the last-stage lift lies over h and has range (σ^r)⁻¹(range h) (stageMap_last_pullbackLiftLast, range_pullbackLiftLast). This module states the same facts at every stage: over h (stageMap_pullbackLift), intertwining the blow-downs (map_pullbackLift), injective when h is (injective_pullbackLift), range (σ^i)⁻¹(range h) (range_pullbackLift); and, for an injective h, the lift corestricted onto its range is a diffeomorphism onto the open submanifold (σ^i)⁻¹(range h) of the stage (pullbackLiftDiffeomorph, by Mathlib's IsLocalDiffeomorph.toDiffeomorphOfBijective). Through these diffeomorphisms the restriction of a succession to an open U₁ ⊆ U₂ ([Wlo09, Theorem 2.0.3, (4)]) is identified with the pull-back along the open inclusion. The proofs are by recursion on the list, the pattern of stageMap_last_pullbackLiftLast and injective_pullbackLiftLast.

theorem AnalyticManifold.BlowUpSequence.pullbackLiftAux_zero {𝕜 : 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) (hi : 0 < L.length + 1) (hi' : 0 < (L.pullback h hh).length + 1) : L.pullbackLiftAux h hh 0 hi hi' = h

The stage lift at stage 0 is h itself (the ℕ-indexed form of pullbackLift_zero).

theorem AnalyticManifold.BlowUpSequence.stageMapAux_pullbackLiftAux {𝕜 : 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) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) (q : (N.finStages (L.pullback h hh).toSuccession.later ⟨i, hi'⟩).carrier) : (L.toSuccession.stageMapAux i hi) ((L.pullbackLiftAux h hh i hi hi') q) = h (((L.pullback h hh).toSuccession.stageMapAux i hi') q)

The stage lifts lie over h: σ^i ∘ h_i = h ∘ σ'^i, ℕ-indexed (the stage-wise form of stageMap_last_pullbackLiftLast).

theorem AnalyticManifold.BlowUpSequence.pullbackLiftAux_map {𝕜 : 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) (i : ℕ) (hi : i < L.length) (hi' : i < (L.pullback h hh).length) (q : ((L.pullback h hh).toSuccession.stage ⟨i + 1, ⋯⟩).carrier) : (L.pullbackLiftAux h hh i ⋯ ⋯) (((L.pullback h hh).toSuccession.map ⟨i, hi'⟩) q) = (L.toSuccession.map ⟨i, hi⟩) ((L.pullbackLiftAux h hh (i + 1) ⋯ ⋯) q)

The stage lifts intertwine the blow-downs, ℕ-indexed: h_i ∘ π'_{i+1} = π_{i+1} ∘ h_{i+1} (blowUpπ_liftStep along the list).

theorem AnalyticManifold.BlowUpSequence.injective_pullbackLiftAux {𝕜 : 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.Injective ⇑h → ∀ (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1), Function.Injective ⇑(L.pullbackLiftAux h hh i hi hi')

The stage lifts of an injective h are injective, ℕ-indexed (injective_liftStep along the list, the pattern of isLocalDiffeomorph_pullbackLiftAux).

theorem AnalyticManifold.BlowUpSequence.stageMap_pullbackLift {𝕜 : 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) (i : Fin (L.length + 1)) (q : ((L.pullback h hh).stage ⟨↑i, ⋯⟩).carrier) : (L.toSuccession.stageMap i) ((L.pullbackLift h hh i) q) = h (((L.pullback h hh).toSuccession.stageMap ⟨↑i, ⋯⟩) q)

[Kol07, Definition 30, 30.1]: the stage lifts lie over h, σ^i ∘ h_i = h ∘ σ'^i.

theorem AnalyticManifold.BlowUpSequence.map_pullbackLift {𝕜 : 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) (i : Fin L.length) (q : ((L.pullback h hh).stage ⟨↑i + 1, ⋯⟩).carrier) : (L.pullbackLift h hh i.castSucc) (((L.pullback h hh).toSuccession.map ⟨↑i, ⋯⟩) q) = (L.toSuccession.map i) ((L.pullbackLift h hh i.succ) q)

[Kol07, Definition 30, 30.1]: the stage lifts intertwine the blow-downs, h_i ∘ π'_{i+1} = π_{i+1} ∘ h_{i+1}.

theorem AnalyticManifold.BlowUpSequence.injective_pullbackLift {𝕜 : 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) (hi : Function.Injective ⇑h) (i : Fin (L.length + 1)) : Function.Injective ⇑(L.pullbackLift h hh i)

[Kol07, Definition 30, 30.1] (the printed sentence is the surjective case): the stage lifts of an injective local analytic isomorphism are injective.

theorem AnalyticManifold.BlowUpSequence.range_pullbackLift {𝕜 : 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) (i : Fin (L.length + 1)) : Set.range ⇑(L.pullbackLift h hh i) = ⇑(L.toSuccession.stageMap i) ⁻¹' Set.range ⇑h

[Kol07, Definition 30, 30.1]: the range of the stage lift h_i is the preimage of the range of h under the composite blow-down σ^i (the stage-wise form of range_pullbackLiftLast: ⊆ from stageMap_pullbackLift, ⊇ is mem_range_pullbackLift_of_stageMap_mem).

theorem AnalyticManifold.BlowUpSequence.range_pullbackLift_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) (i : Fin (L.length + 1)) {V : TopologicalSpace.Opens (L.stage i).carrier} (hV : ↑V = ⇑(L.toSuccession.stageMap i) ⁻¹' Set.range ⇑h) : Set.range ⇑(L.pullbackLift h hh i) ⊆ ↑V

The range of a stage lift lies in every open V of the stage carrying the preimage of the range of h.

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLiftDiffeomorph {𝕜 : 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) (hi : Function.Injective ⇑h) (i : Fin (L.length + 1)) (V : TopologicalSpace.Opens (L.stage i).carrier) (hV : ↑V = ⇑(L.toSuccession.stageMap i) ⁻¹' Set.range ⇑h) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback h hh).stage ⟨↑i, ⋯⟩).carrier ((L.stage i).restrict V).carrier ⊤

[Kol07, Definition 30, 30.1] (the lift of an open immersion): the stage lift of an injective local analytic isomorphism, corestricted onto its range — an open V of the stage with V = (σ^i)⁻¹(range h) — as a diffeomorphism onto that open submanifold: the corestriction is a bijective local analytic isomorphism (isLocalDiffeomorph_corestrict, injective_pullbackLift, range_pullbackLift), hence a diffeomorphism by Mathlib's IsLocalDiffeomorph.toDiffeomorphOfBijective.

Equations

• L.pullbackLiftDiffeomorph h hh hi i V hV = ⋯.toDiffeomorphOfBijective ⋯

theorem AnalyticManifold.BlowUpSequence.pullbackLiftDiffeomorph_apply {𝕜 : 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) (hi : Function.Injective ⇑h) (i : Fin (L.length + 1)) (V : TopologicalSpace.Opens (L.stage i).carrier) (hV : ↑V = ⇑(L.toSuccession.stageMap i) ⁻¹' Set.range ⇑h) (q : ((L.pullback h hh).stage ⟨↑i, ⋯⟩).carrier) : ↑((L.pullbackLiftDiffeomorph h hh hi i V hV) q) = (L.pullbackLift h hh i) q

The diffeomorphism onto the trace is the stage lift, read in the stage.