Descent of a blow-up sequence along a surjective local analytic isomorphism

The descent of [Kol07, Proposition 37], (37.1)–(37.2), iterated along the sequence. On manifolds, with the functors valued in centre lists: a list L' on N whose two pull-backs to a fibre product (P, p₁, p₂) of the surjective local analytic isomorphism g : N → M with itself agree is the pull-back of a unique list L on M, by recursion on L'. The first centre is saturated (saturated_of_isFibreProduct), so it is the preimage of a closed submanifold Z of M (IsClosedSubmanifold.image_of_saturated); the tail lives on the blowing-up of N along g⁻¹Z, which is the domain of the lift g₁ : Bl_{g⁻¹Z} N → Bl_Z M; the lifted projections form again a fibre product (isFibreProduct_lifted), and the tail descends by the recursive call. Uniqueness is pullback_injective_of_surjective.

theorem AnalyticManifold.BlowUpSequence.exists_pullback_eq_of_isFibreProduct {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {N : AnalyticManifold 𝕜 E} (L' : BlowUpSequence ψ₀ N) {M P : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : Function.Surjective ⇑g → ∀ (p₁ p₂ : AnalyticMap P N) (hp : Manifold.IsFibreProduct g g p₁ p₂), L'.pullback p₁ ⋯ = L'.pullback p₂ ⋯ → ∃ (L : BlowUpSequence ψ₀ M), L.pullback g hg = L'

[Kol07, Proposition 37], (37.1)–(37.2) iterated ("we can repeat the above argument"): a list on N whose two pull-backs to a fibre product of g with itself agree descends to M.

theorem AnalyticManifold.BlowUpSequence.exists_unique_pullback_eq_of_isFibreProduct {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (g : AnalyticMap N M) (hg : Manifold.IsCoprodOfOpenEmbeddings g) (hs : Function.Surjective ⇑g) (p₁ p₂ : AnalyticMap P N) (hp : Manifold.IsFibreProduct g g p₁ p₂) (L' : BlowUpSequence ψ₀ N) (hL' : L'.pullback p₁ ⋯ = L'.pullback p₂ ⋯) : ∃! L : BlowUpSequence ψ₀ M, L.pullback g ⋯ = L'

[Kol07, Proposition 37], the descent step with its uniqueness: a list on the cover whose two pull-backs to the fibre product agree is the pull-back of exactly one list on the base (uniqueness by pullback_injective_of_surjective).