Theorem 97: étale equivalent blow-up sequences are equal

[Kol07, Theorem 97]: two étale equivalent blow-up sequences of order m for an MC-invariant ideal sheaf on a smooth variety over a field of characteristic zero are equal. The proof in this library has two parts. The marked form (eq_of_pullback_eq_of_agreeOn_of_step in Hironaka/Resolution/Algebraic/MaximalContact/Theorem97Induction.lean, a structural induction on the common pull-back) and the reduction of Theorem 97 to it (eq_of_etaleEquivSeq_of_step) both take the one inductive step the induction needs, the descent of agreement of two morphisms through one blow-up, as an explicit hypothesis hstep; that step is agreeOn_blowUpMap (Hironaka/Resolution/Algebraic/MaximalContact/AgreeOnBlowUpKernel.lean), in exactly the shape of hstep. The two theorems below are the unconditional forms: hstep := agreeOn_blowUpMap.

Conventions. Theorem 97 needs no hypothesis on I beyond m ≥ 1: MC-invariance enters the uniqueness of maximal contact only through Theorem 92, so Kollár's "MC-invariant" and "m = max-ord I" are not hypotheses here (Theorem97Induction.lean explains why the marked form uses no property of I). Kollár's "étale surjections" are read in the form of [Kol07, Definition 96] where the images of ψ, ψ' contain the cosupport (EtaleEquivSeq, Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivSeq.lean). The theorem is used for the independence of the order-reduction functor from the hypersurface of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/FunctorIndependence.lean).

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_pullback_eq_of_agreeOn {X U : Scheme} (ψ ψ' : U ⟶ X) [Flat ψ] [Flat ψ'] (M : U.IdealSheafData) (h1 : AgreeOn ψ ψ' M) (B B' : X.BlowUpSequence) (C : U.BlowUpSequence) (hB : B.pullback ψ = C) (hB' : B'.pullback ψ' = C) (h2 : C.IsMarkedOneSeq M) (h3 : B.CentersInRange ψ) (h3' : B'.CentersInRange ψ') : B = B'

The marked form of [Kol07, Theorem 97]: for flat ψ, ψ' : U ⟶ X agreeing on V(M), blow-up sequences B, B' on X with the common pull-back C of order ≥ 1 for (M, 1), and the centres of B, B' in the images of the lifts, B = B'. This is eq_of_pullback_eq_of_agreeOn_of_step with the one-step descent agreeOn_blowUpMap.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_etaleEquivSeq {k : Type u} [Field k] {X : Scheme} [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {m : ℕ} (hm : 1 ≤ m) {E E' : X.DivisorFamily} {B B' : X.BlowUpSequence} (hB : B.IsOrderSeq f I E m) (hB' : B'.IsOrderSeq f I E' m) (e : EtaleEquivSeq f I m B B') : B = B'

[Kol07, Theorem 97]: for X smooth of relative dimension n over k of characteristic zero, m ≥ 1, smooth blow-up sequences B of order m for (X, I, E) and B' of order m for (X, I, E') that are étale equivalent ([Kol07, Definition 96], with the images of ψ, ψ' containing the cosupport), B = B'.