One-step descent of agreement through a blow-up

The inductive step of Kollár's proof of the uniqueness of blow-up sequences Kol07, Theorem 97, proof; Włodarczyk's equivariance of test blow-ups under the glueing automorphism is the same computation [Wlo09, Lemma 5.5.3, proof, (5)]. Let f, g : U → M agree on the closed analytic subspace V(J), let Y ⊆ M be a closed submanifold whose pulled-back ideal sheaves f^*I_Y, g^*I_Y are both the ideal sheaf of one closed submanifold Z ⊆ U contained in V(J), and let f', g' : Bl_Z U → Bl_Y M be lifts of f, g over the blow-downs. Then f' and g' agree on V((π')^{-1}_*(J, 1)) (agreeOnSubspace_blowUpLift).

The proof

Write M_1 := (π')^{-1}_*(J, 1); its stalks are the colons (π'^*J)_q : I_{F,q} (isDivExceptional_birationalTransform, with 1 ≤ ν_Z(J) from Z ⊆ V(J): stalkIdeal_le_vanishingStalk_of_subset_cosupport). Fix q with M_{1,q} ≠ 𝒪_q (elsewhere there is nothing to prove: agreeOnSubspace_of_forall_sub_mem). Then u := π' q ∈ V(J), so f u = g u.

• Off the exceptional divisor (u ∉ Z): I_{F,q} is the unit ideal and M_{1,q} = (π'^*J)_q; the blow-down is a local isomorphism at f' q, whose fibre over f u ∉ Y is one point, so f' q = g' q; every germ at f' q is π^* t (germMapInv), and f'^*π^*t − g'^*π^*t = π'^*(f^*t − g^*t) ∈ π'^*J (functoriality, germMap_germMap_germ).
• On the exceptional divisor (u ∈ Z, y := f u ∈ Y): take an adapted chart φ of Y at y with coordinates z_j, a blow-up chart Φ of index i at f' q (IsBlowUp.cover), and a blow-up chart Φ' of Bl_Z U at q with scaling coordinate e, so that I_{F,q} = (e) (stalkIdeal_exceptionalIdealSheaf_eq_span_coord) and x ∈ M_{1,q} ⟺ x e ∈ (π'^*J)_q. Set A_j := π'^* f^* z_j, B_j := π'^* g^* z_j. For the centre indices, A_{σk}, B_{σk} ∈ (e) (f^*I_Y = I_Z, IsBlowUp.stalkIdeal_pullback_eq_span_coord): A_{σk} = At_k e, B_{σk} = Bt_k e, and (At_k − Bt_k) e = π'^*(f^*z_{σk} − g^*z_{σk}) ∈ π'^*J, so At_k − Bt_k ∈ M_{1,q} ⊆ 𝔪_q: At_k(q) = Bt_k(q). The chart formulae z_{σi} ∘ π = w_{σi}, z_{σk} ∘ π = w_{σi} w_{σk}, z_j ∘ π = w_j (germMap_coord_self, germMap_coord_of_ne, germMap_coord_off) pulled back by f' give A_{σi} = a_i, A_{σk} = a_i a_k for the coordinates a_j := f'^* w_j. Since e ∈ (A_{σk})_k (the same identification of π'^*I_Z), At_i is a unit (else e (1 − At_i t) = 0 with a unit factor, contradicting coord_ne_zero), hence so is Bt_i. Reading g' q in its own chart Φ'' of index i'', Bt_i e = Bt_{i''} e · g'^*w''_{σi}, so g'^*w''_{σi}(q) ≠ 0 and g' q lies in the chart Φ (IsBlowUpChart.mem_source_of_mem_transitionDomain). With b_j := g'^* w_j in the same chart, At_i Bt_i (a_k − b_k) e = e [Bt_i(At_k − Bt_k) + Bt_k(Bt_i − At_i)], so a_j − b_j ∈ M_{1,q} for every coordinate; their values agree, so Φ(f' q) = Φ(g' q) and f' q = g' q; and the coordinate criterion sub_mem_of_forall_coord_sub_mem (Hadamard's lemma and Krull's intersection theorem) extends the agreement modulo M_{1,q} to every germ.

No smoothness or local-isomorphism hypothesis on f, g beyond the centre clause is used. The Hironaka library proves the same step for schemes (Hironaka/Resolution/Algebraic/MaximalContact/AgreeOnBlowUpKernel.lean).

theorem Hironaka.Manifold.agreeOnSubspace_blowUpLift {𝕜 : Type} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M U : AnalyticManifold 𝕜 E} (f g : AnalyticMap U M) {Y : Set M.carrier} {Z : Set U.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (hZ : Manifold.IsClosedSubmanifold ψ Z c) (hZf : Manifold.IdealSheaf.pullback ⇑f ⋯ hY.idealSheaf = hZ.idealSheaf) (hZg : Manifold.IdealSheaf.pullback ⇑g ⋯ hY.idealSheaf = hZ.idealSheaf) (J : U.IdealSheaf) (hJZ : Z ⊆ Manifold.IdealSheaf.support J) (hfg : AgreeOnSubspace f g J) (f' g' : AnalyticMap (Manifold.blowUp ψ hZ) (Manifold.blowUp ψ hY)) (hf' : ∀ (q : (Manifold.blowUp ψ hZ).carrier), (Manifold.blowUpπ ψ hY) (f' q) = f ((Manifold.blowUpπ ψ hZ) q)) (hg' : ∀ (q : (Manifold.blowUp ψ hZ).carrier), (Manifold.blowUpπ ψ hY) (g' q) = g ((Manifold.blowUpπ ψ hZ) q)) : AgreeOnSubspace f' g' (Manifold.MarkedIdealSheaf.birationalTransform hZ ⋯ { I := J, m := 1 }).I

One-step descent of agreement through a blow-up ([Kol07, Theorem 97, proof]; [Wlo09, Lemma 5.5.3, proof, (5)]): if f, g : U → M agree on V(J), pull the ideal sheaf of the closed submanifold Y back to the ideal sheaf of one closed submanifold Z ⊆ V(J), and f', g' are lifts of f, g to the blow-ups along Z and Y, then f' and g' agree on V((π')^{-1}_*(J, 1)).