Theorem 97: the marked datum carried along the induction

[Kol07, Theorem 97]: for X a smooth variety over a field of characteristic zero, I an MC-invariant ideal sheaf and B, B' two blow-up sequences of order m = max-ord I which are étale equivalent, B = B'. Its proof is an induction on the stage i along the common pull-back B^U := ψ^*B = ψ'^*B' carrying three assertions: (1) (X_i, I_i) = (X'_i, I'_i), (2) the lifts ψ_i, ψ'_i : U_i ⇉ X_i satisfy im(ψ_i^* − ψ'^*_i) ⊂ (Π^U_i)^{-1}_*(MC(I^U_0), 1), (3) Z_{i−1} = Z'_{i−1}, with W_i = cosupp((Π^U_i)^{-1}_*(MC(I^U_0), 1)) and the remark that Z^U_i ⊂ W_i by Corollary 77.

The proof in this library (Hironaka/Resolution/Algebraic/MaximalContact/Theorem97Induction.lean) recasts the induction in a marked form that carries the marked ideal (M, 1), M := MC(ψ^*I), instead of I: the transforms I_i are in general neither D-balanced nor MC-invariant (the Warning in [Kol07, 104]), and the proof uses of I only that M_i := (Π^U_i)^{-1}_*(M, 1) is contained in the ideal of every centre Z^U_i ([Kol07, Corollary 77] with j = m − 1, together with the reducedness of the smooth centres). This file holds the definition of that datum:

• IsMarkedOneSeq C M: the sequence C on U is a blow-up sequence of order ≥ 1 for the marked ideal (M, 1) in the containment form, M_i ≤ 𝒪(Z^U_i) for every i, where M_i = C.markedTransformSeq M 1 i is the recursion M_0 = M, M_{i+1} = (π^U_i)^{-1}_*(M_i, 1) = (π^{U*}_i M_i : 𝒪(F^U_{i+1})) (the condition (1′) of [Kol07, Definition 66]). The containment is one of ideals, not of supports: for a non-reduced centre J = (x², y²) and M = (x, y) have equal zero sets but M ⊄ J, and it is the containment that makes M_{i+1} an ideal. isMarkedOneSeq_cons_iff is the recursive reading (nil ↦ True; cons Z rest, M ↦ M ≤ Z ∧ IsMarkedOneSeq rest (markedTransform Z M 1)).
• AgreeOn.mono: agreement on V(M) gives agreement on the smaller closed subscheme V(J) for M ≤ J (the closed immersion V(J) ⟶ V(M), Mathlib's IdealSheafData.inclusion); needed for the descent of the centres in the induction and in the one-step descent (Hironaka/Resolution/Algebraic/MaximalContact/AgreeOnBlowUp.lean).
• centersInRange_cons_iff, centersInRange_eqToHom_comp: the recursive reading of CentersInRange and its invariance under the transport of the source along an equality of schemes.

def AlgebraicGeometry.Scheme.BlowUpSequence.IsMarkedOneSeq {U : Scheme} (C : U.BlowUpSequence) (M : U.IdealSheafData) : Prop

The blow-up sequence C on U is of order ≥ 1 for the marked ideal (M, 1), in the containment form: the marked transform M_i = (Π^U_i)^{-1}_*(M, 1) (markedTransformSeq M 1) is contained in the ideal sheaf of the centre Z^U_i at every stage. This is Kollár's Z^U_i ⊂ W_i in the proof of [Kol07, Theorem 97], strengthened from supports to ideals.

Equations

• C.IsMarkedOneSeq M = ∀ (i : Fin C.length), C.markedTransformSeq M 1 i.castSucc ≤ C.center i

theorem AlgebraicGeometry.Scheme.BlowUpSequence.isMarkedOneSeq_nil {U : Scheme} (M : U.IdealSheafData) : (nil U).IsMarkedOneSeq M

The empty sequence is of order ≥ 1 for every (M, 1).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.isMarkedOneSeq_cons_iff {U : Scheme} (Z : U.IdealSheafData) (rest : Z.blowUp.BlowUpSequence) (M : U.IdealSheafData) : (cons U Z rest).IsMarkedOneSeq M ↔ M ≤ Z ∧ rest.IsMarkedOneSeq (M.markedTransform Z 1)

The recursive reading: on the cons shape the containment at stage 0 is M ≤ Z, and the tail is of order ≥ 1 for (π^{-1}_*(M, 1), 1).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.centersInRange_cons_iff {U X : Scheme} (Z : X.IdealSheafData) (rest : Z.blowUp.BlowUpSequence) (ψ : U ⟶ X) : (cons X Z rest).CentersInRange ψ ↔ ↑Z.support ⊆ Set.range ⇑ψ ∧ rest.CentersInRange (Hom.blowUpMap ψ Z)

CentersInRange read recursively: on the cons shape the condition at stage 0 is |Z| ⊆ im ψ, and the tail's condition is along the lift blowUpMap ψ Z (pullbackStageHom_cons_zero, pullbackStageHom_cons_succ, both definitional).

theorem AlgebraicGeometry.Scheme.BlowUpSequence.centersInRange_eqToHom_comp {U X : Scheme} (S : X.BlowUpSequence) {U' : Scheme} (e : U' = U) (ψ : U ⟶ X) : S.CentersInRange (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e) ψ) ↔ S.CentersInRange ψ

The covering condition on the centres is unchanged when the source of the map is transported along an equality of schemes.

theorem AlgebraicGeometry.Scheme.IdealSheafData.AgreeOn.mono {U X : Scheme} {f g : U ⟶ X} {M J : U.IdealSheafData} (h : M ≤ J) (hfg : AgreeOn f g M) : AgreeOn f g J

Kollár's use of the inductive assumption (2) on the centre Z^U_i ⊆ W_i (proof of [Kol07, Theorem 97]): two morphisms agreeing on V(M) agree on every closed subscheme V(J) with M ≤ J, since V(J) ⟶ V(M) is the closed immersion inclusion h and ι_J = inclusion h ≫ ι_M.