Pull-back of a concatenation, and the transforms at the last stage along the lift

The pull-back of a blow-up sequence along a smooth morphism h is formed stage by stage ([Kol07, Definition 30], 30.1), the morphism lifting through each blow-up to the next stage. For sequences of centres this module gives the lift h_r of a local analytic isomorphism h : N → M to the last stages, shows that the pull-back of a concatenation L.concat L' is the concatenation of the pull-back of L and the pull-back of L' along h_r, and shows that along h_r the controlled transform of (𝓘, m) and the boundary family from a start F pull back.

• BlowUpSequence.pullbackLiftLast, isLocalDiffeomorph_pullbackLiftLast, surjective_pullbackLiftLast — the lift of h to the last stages, typed on the last stages directly (the stage-indexed lift pullbackLift carries the length identity in its index).
• BlowUpSequence.pullback_concat — the pull-back of a concatenation.
• HypersurfaceFamily.totalTransform_comap_liftStep, BlowUpSequence.totalTransformSeqFrom_last_pullbackLiftLast — the boundary family from F at the last stage of h^* L is the pull-back along h_r of the family at the last stage of L.
• BlowUpSequence.markedTransformSeq_last_pullbackLiftLast — the controlled transform at the last stage of h^* L is the pull-back along h_r, for L of order ≥ m.

These are the transport lemmas behind the functoriality of Steps 2.1 and 2.2 of the proof of [Kol07, Theorem 103] (Step21Functoriality.lean, Step22Pullback.lean), where each step of the construction is pulled back along the lift to the last stage of the previous one. Not in the sources; bookkeeping.

theorem Manifold.HypersurfaceFamily.totalTransform_comap_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) (F : HypersurfaceFamily M.carrier) : totalTransform (⇑(blowUpπ ψ₀ ⋯)) (⇑h ⁻¹' Y) (comap (⇑h) F) = comap (⇑(AnalyticManifold.BlowUpSequence.liftStep h hh hY)) (totalTransform (⇑(blowUpπ ψ₀ hY)) Y F)

The total transform of h⁻¹(F) under the blow-up of h⁻¹(Y) is the pull-back along the lift liftStep of the total transform of F under the blow-up of Y ([Kol07, Definition 25]): the strict transforms pull back (strictTransformSet_preimage_liftStep), and the exceptional divisor lies over the exceptional divisor.

def AnalyticManifold.BlowUpSequence.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) : AnalyticMap ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)) (L.stage (Fin.last L.length))

The lift h_r of a local analytic isomorphism h : N → M to the last stages of h^* L and L ([Kol07, Definition 30], 30.1), by recursion on the sequence of centres, typed on the last stages directly.

Equations

• (AnalyticManifold.BlowUpSequence.nil x).pullbackLiftLast x_2 x_3 = x_2
• (AnalyticManifold.BlowUpSequence.cons hY rest).pullbackLiftLast x_2 x_3 = rest.pullbackLiftLast (AnalyticManifold.BlowUpSequence.liftStep x_2 x_3 hY) ⋯

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

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_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) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(L.pullbackLiftLast h hh)

The lift to the last stages is a local analytic isomorphism.

theorem AnalyticManifold.BlowUpSequence.surjective_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) : Function.Surjective ⇑h → Function.Surjective ⇑(L.pullbackLiftLast h hh)

The lift to the last stages of a surjective local analytic isomorphism is surjective.

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

The pull-back of a concatenation is the concatenation of the pull-backs, the second along the lift of h to the last stage of L ([Kol07, Definition 30], 30.1, for a composite sequence).

theorem AnalyticManifold.BlowUpSequence.totalTransformSeqFrom_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) (F : Manifold.HypersurfaceFamily M.carrier) : (L.pullback h hh).toSuccession.totalTransformSeqFrom (Manifold.HypersurfaceFamily.comap (⇑h) F) (Fin.last (L.pullback h hh).toSuccession.length) = Manifold.HypersurfaceFamily.comap (⇑(L.pullbackLiftLast h hh)) (L.toSuccession.totalTransformSeqFrom F (Fin.last L.toSuccession.length))

The boundary family from h⁻¹(F) at the last stage of h^* L is the pull-back along the lift h_r of the boundary family from F at the last stage of L (totalTransform_comap_liftStep at each step).

theorem AnalyticManifold.BlowUpSequence.markedTransformSeq_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) (I E₀ : M.IdealSheaf) (m : ℕ) : L.toSuccession.IsOfOrderGe I m E₀ → (L.pullback h hh).toSuccession.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m (Fin.last (L.pullback h hh).toSuccession.length) = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftLast h hh) ⋯ (L.toSuccession.markedTransformSeq I m (Fin.last L.toSuccession.length))

The controlled transform of (h^* 𝓘, m) at the last stage of h^* L is the pull-back along the lift h_r of the controlled transform of (𝓘, m) at the last stage of L, for L of order ≥ m (birationalTransform_comap_liftStep at each step).