The pull-back of a list of centres, stage by stage

For a list of centres L on M and a local analytic isomorphism h : N → M, BlowUpSequence.pullback is the list of the preimage centres under the successive lifts h_i : N_i → M_i (pullbackLiftAux), the pull-back of a blow-up sequence along a smooth morphism [Kol07, Definition 30, 30.1]. This file records, by induction on the list, what the succession of h^* L carries at each stage in terms of L's data pulled back along the lifts:

• the lifts are local analytic isomorphisms, surjective when h is (isLocalDiffeomorph_pullbackLiftAux, surjective_pullbackLiftAux);
• the centres (center_pullbackAux), the weak transforms (weakTransformSeqAux_pullback), the boundaries (boundarySeqAux_pullback, along a surjective h: Hironaka's reduced transform is natural along surjective local isomorphisms, reducedTransform_comap_liftStep) and, along a sequence of order ≥ m for (I, m), the marked transforms (markedTransformSeqAux_pullback, the marking being legitimate at every stage), each the comap along the lift of the datum on L;
• the descent of [Kol07, Definition 66] (isOfOrderGe_of_pullback): if h^* L is a smooth blow-up sequence of order ≥ m for (h^* I, m, h^* E) [Kol07, Definition 66] and h is surjective, then L is one for (I, m, E): stage by stage, the normal-crossings clause and the order clause come back along the bijective germ maps (Hironaka.Resolution.Analytic.Functor.PullbackTransport), the marking of the first transform being legitimate once the order clause at stage 0 is known.

This is how the clauses of the descended functor are read on the pull-back to the cover in the global case of the proof of [Kol07, Theorem 103] (the functoriality package is local, as the proof remarks at the end of its local case).

The lifts

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

The lifts of a local analytic isomorphism to the stages are local analytic isomorphisms.

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

The lifts of a surjective local analytic isomorphism to the stages are surjective (surjective_liftStep at each step).

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

The lift h_i : N_i → M_i of a local analytic isomorphism to the stage i is a local analytic isomorphism.

theorem AnalyticManifold.BlowUpSequence.surjective_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) (hs : Function.Surjective ⇑h) (i : Fin (L.length + 1)) : Function.Surjective ⇑(L.pullbackLift h hh i)

The lifts of a surjective local analytic isomorphism are surjective.

The stages of the pull-back

theorem AnalyticManifold.BlowUpSequence.center_pullbackAux {𝕜 : 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) : (L.pullback h hh).toSuccession.center ⟨i, hi'⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i ⋯ ⋯) ⋯ (L.toSuccession.center ⟨i, hi⟩)

The centres of h^* L are the pull-backs of the centres of L along the lifts.

theorem AnalyticManifold.BlowUpSequence.weakTransformSeqAux_pullback {𝕜 : 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) (J : M.IdealSheaf) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1) : (L.pullback h hh).toSuccession.weakTransformSeqAux (Manifold.IdealSheaf.pullback ⇑h ⋯ J) i hi' = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i hi hi') ⋯ (L.toSuccession.weakTransformSeqAux J i hi)

The weak transforms along h^* L are the pull-backs of the weak transforms along L (weakTransform_comap_liftStep at each step).

theorem AnalyticManifold.BlowUpSequence.boundarySeqAux_pullback {𝕜 : 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 → ∀ (E₀ : M.IdealSheaf) (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1), (L.pullback h hh).toSuccession.boundarySeqAux (Manifold.IdealSheaf.pullback ⇑h ⋯ E₀) i hi' = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i hi hi') ⋯ (L.toSuccession.boundarySeqAux E₀ i hi)

The boundaries along h^* L, for a SURJECTIVE h, are the pull-backs of the boundaries along L (reducedTransform_comap_liftStep at each step).

theorem AnalyticManifold.BlowUpSequence.markedTransformSeqAux_pullback {𝕜 : 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₀ → ∀ (i : ℕ) (hi : i < L.length + 1) (hi' : i < (L.pullback h hh).length + 1), (L.pullback h hh).toSuccession.markedTransformSeqAux (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m i hi' = Manifold.IdealSheaf.pullback ⇑(L.pullbackLiftAux h hh i hi hi') ⋯ (L.toSuccession.markedTransformSeqAux I m i hi)

Along a sequence of order ≥ m for (I, m, E₀), the marked transforms along h^* L are the pull-backs of the marked transforms along L (birationalTransform_comap_liftStep at each step; the marking is legitimate by the order clause of [Kol07, Definition 66] at that step).

The stages of the pull-back, indexed by Fin, along the lifts pullbackLift

theorem AnalyticManifold.BlowUpSequence.center_pullback {𝕜 : 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) : (L.pullback h hh).toSuccession.center ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i.castSucc) ⋯ (L.toSuccession.center i)

The centres of h^* L along the lifts (Fin-indexed form of center_pullbackAux).

theorem AnalyticManifold.BlowUpSequence.weakTransformSeq_pullback {𝕜 : 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) (J : M.IdealSheaf) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.weakTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ J) ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i) ⋯ (L.toSuccession.weakTransformSeq J i)

The weak transforms along h^* L along the lifts (Fin-indexed form of weakTransformSeqAux_pullback).

theorem AnalyticManifold.BlowUpSequence.boundarySeq_pullback {𝕜 : 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) (hs : Function.Surjective ⇑h) (E₀ : M.IdealSheaf) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.boundarySeq (Manifold.IdealSheaf.pullback ⇑h ⋯ E₀) ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i) ⋯ (L.toSuccession.boundarySeq E₀ i)

The boundaries along h^* L, for a surjective h, along the lifts (Fin-indexed form of boundarySeqAux_pullback).

theorem AnalyticManifold.BlowUpSequence.markedTransformSeq_pullback {𝕜 : 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 : ℕ) (hge : L.toSuccession.IsOfOrderGe I m E₀) (i : Fin (L.length + 1)) : (L.pullback h hh).toSuccession.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m ⟨↑i, ⋯⟩ = Manifold.IdealSheaf.pullback ⇑(L.pullbackLift h hh i) ⋯ (L.toSuccession.markedTransformSeq I m i)

The marked transforms along h^* L, for L of order ≥ m for (I, m, E₀), along the lifts (Fin-indexed form of markedTransformSeqAux_pullback).

The descent of [Kol07, Definition 66]

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_of_pullback {𝕜 : 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 → ∀ (I E₀ : M.IdealSheaf) (m : ℕ), (L.pullback h hh).toSuccession.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑h ⋯ I) m (Manifold.IdealSheaf.pullback ⇑h ⋯ E₀) → L.toSuccession.IsOfOrderGe I m E₀

[Kol07, Definition 66] descends along a surjective local analytic isomorphism: if h^* L is a smooth blow-up sequence of order ≥ m for (h^* I, m, h^* E₀) and h is surjective, then L is one for (I, m, E₀). Stage by stage: the normal-crossings clause and the order clause at the first centre come back along the bijective germ maps (HasOnlyNormalCrossingsWith.of_comap_of_surjective, ordAlongIdeal_comap_of_isLocalDiffeomorphAt, every point of the centre having a preimage), and the tail of h^* L is the pull-back of the tail of L along the surjective lift, for the first marked transform and the first boundary (birationalTransform_comap_liftStep — the marking being legitimate by the order clause just obtained — and reducedTransform_comap_liftStep).

Transfer of the clauses along an equality of lists

theorem AnalyticManifold.BlowUpSequence.forall_last_ord_lt_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {L₁ L₂ : BlowUpSequence ψ₀ N} (e : L₁ = L₂) (I : N.IdealSheaf) (m : ℕ) (H : ∀ (x : (L₁.toSuccession.stage (Fin.last L₁.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L₁.toSuccession.weakTransformSeq I (Fin.last L₁.toSuccession.length)) x < ↑m) (x : (L₂.toSuccession.stage (Fin.last L₂.toSuccession.length)).carrier) : Manifold.IdealSheaf.ord (L₂.toSuccession.weakTransformSeq I (Fin.last L₂.toSuccession.length)) x < ↑m

The output clause of [Kol07, Theorem 103, (1)] transfers along an equality of lists (the points of the last stage are transported by subst).

theorem AnalyticManifold.BlowUpSequence.ord_lt_of_forall_last {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} {L : BlowUpSequence ψ₀ N} (I : N.IdealSheaf) (m : ℕ) (H : ∀ (x : (L.toSuccession.stage (Fin.last L.toSuccession.length)).carrier), Manifold.IdealSheaf.ord (L.toSuccession.weakTransformSeq I (Fin.last L.toSuccession.length)) x < ↑m) (k : ℕ) (hk : k < L.length + 1) (e : k = L.length) (y : (N.finStages L.toSuccession.later ⟨k, hk⟩).carrier) : Manifold.IdealSheaf.ord (L.toSuccession.weakTransformSeqAux I k hk) y < ↑m

The output clause at the last stage, read at any index k provably equal to the length.