The loops of Steps 1 and 2 under an arbitrary smooth morphism

The second clause of [Kol07, 34.1] for the loops of the proof of [Kol07, Theorem 107]: along a smooth h : Y → X, not necessarily surjective, Step 1 on the data of Y is the pull-back of Step 1 on X with its empty blow-ups deleted, under the indifference of the input functors bo d to unit boundary members (hboind). The induction runs over the recursion of step1 on X with the invariant "T' is the pull-back of T up to unit members" (IsPullbackOfUpToUnits, Hironaka/Resolution/Algebraic/MarkedOrderReduction/UpToUnits.lean). At a round of X at order d:

• if the round order of Y is also d, the round on Y is the erased pull-back of the round on X: hboind moves the round from (Y, N(I'), E') to the round triple of the full pull-back (unit members appended, nonmonomialTriple_fullPullback), on which the second clause of [Kol07, 34.1] for [Kol07, Theorem 103] applies (step1Round_eraseEmpty_pullback_of_eq);
• if the round order of Y is smaller, the round is skipped: its pull-back consists of empty blow-ups (pullback_eraseEmpty_eq_nil_of_maxOrd_lt, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SkippedRound.lean), and Y's data are unchanged up to the isomorphism of the erased sequence with the empty sequence, along which step1 is transported by the surjective clause (step1_pullback_of_surjective at the identity, step1_induced_eq_seq).

In both cases the marked triple induced on Y after the erased pulled-back round is the pull-back up to unit members of the triple induced on X after the round (IsPullbackOfUpToUnits.induced_eraseEmpty), and the induction closes with pullback_concat, eraseEmpty_concat and the erasure along the last-stage isomorphism (eraseEmpty_pullback_of_flat_surjective). Step 2 is the same argument on the separation order, the skipped round bounded by maxOrd_comap_sepIdeal_lt (Kollár's observation in [Kol07, 111, Step 2] that ord (N^m + I^s) ≥ ms iff ord N ≥ s and ord I ≥ m). The whole functor is treated in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Smooth.lean.

theorem Hironaka.BMO.step1_induced_eq_seq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T' : MarkedTriple k) {S₁ S₂ : T'.X.left.BlowUpSequence} (e : S₁ = S₂) (h₁ : S₁.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E) (h₂ : S₂.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E) (c₁ : MarkedTriple.BMOClass n m (T'.induced S₁ h₁ (Fin.last S₁.length))) (c₂ : MarkedTriple.BMOClass n m (T'.induced S₂ h₂ (Fin.last S₂.length))) : ↑(step1 bo (T'.induced S₁ h₁ (Fin.last S₁.length)) c₁) = (↑(step1 bo (T'.induced S₂ h₂ (Fin.last S₂.length)) c₂)).pullback (CategoryTheory.eqToHom ⋯)

The value of step1 on the marked triple induced at the end of a sequence, transported along an equality of sequences (the eqToHom of the last-stage identification).

theorem Hironaka.BMO.step2_induced_eq_seq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T' : MarkedTriple k) {S₁ S₂ : T'.X.left.BlowUpSequence} (e : S₁ = S₂) (h₁ : S₁.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E) (h₂ : S₂.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E) (c₁ : MarkedTriple.BMOClass n m (T'.induced S₁ h₁ (Fin.last S₁.length))) (c₂ : MarkedTriple.BMOClass n m (T'.induced S₂ h₂ (Fin.last S₂.length))) : ↑(step2 bo (T'.induced S₁ h₁ (Fin.last S₁.length)) c₁) = (↑(step2 bo (T'.induced S₂ h₂ (Fin.last S₂.length)) c₂)).pullback (CategoryTheory.eqToHom ⋯)

The value of step2 on the marked triple induced at the end of a sequence, transported along an equality of sequences.

theorem Hironaka.BMO.isPullbackOf_induced_nil {k : Type u} [Field k] [CharZero k] (T' : MarkedTriple k) : T'.IsPullbackOf (T'.induced (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left) ⋯ (Fin.last (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left).length)) (CategoryTheory.CategoryStruct.id T'.X.left)

A marked triple is the exact pull-back, along the identity, of the marked triple induced by the empty sequence.

theorem Hironaka.BMO.step1_eq_step1_induced_nil {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T' : MarkedTriple k) (hT' : MarkedTriple.BMOClass n m T') : ↑(step1 bo T' hT') = ↑(step1 bo (T'.induced (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left) ⋯ (Fin.last (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left).length)) ⋯)

step1 on a marked triple is step1 on the marked triple induced by the empty sequence (the surjective clause at the identity).

theorem Hironaka.BMO.step2_eq_step2_induced_nil {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T' : MarkedTriple k) (hT' : MarkedTriple.BMOClass n m T') : ↑(step2 bo T' hT') = ↑(step2 bo (T'.induced (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left) ⋯ (Fin.last (AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left).length)) ⋯)

step2 on a marked triple is step2 on the marked triple induced by the empty sequence.

theorem Hironaka.BMO.step1Round_eraseEmpty_pullback_of_eq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (hd : m ≤ roundOrder T) (hd' : m ≤ roundOrder T') (hr : roundOrder T' = roundOrder T) : step1Round bo T' hT' hd' = ((step1Round bo T hT hd).pullback h).eraseEmpty

A round of Step 1 with matching round orders commutes with an arbitrary smooth morphism up to empty blow-ups (clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1], per round): the round of Step 1 on the pull-back data is the erased pull-back of the round; hboind moves the round to the round triple of the full pull-back (unit members appended), on which the second clause applies.

theorem Hironaka.BMO.step1Round_pullback_eraseEmpty_eq_nil {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hd : m ≤ roundOrder T) (hlt : roundOrder T' < roundOrder T) : ((step1Round bo T hT hd).pullback h).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left

The skipped round of Step 1: when the round order of the pull-back data is smaller than the round order of X, the round pulls back to empty blow-ups only (pullback_eraseEmpty_eq_nil_of_maxOrd_lt at the round triples).

theorem Hironaka.BMO.step1_eraseEmpty_pullback_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (l : ℕ) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] : T'.IsPullbackOfUpToUnits T h → ∀ (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T'), roundOrder T ≤ l → ↑(step1 bo T' hT') = ((↑(step1 bo T hT)).pullback h).eraseEmpty

The induction behind step1_eraseEmpty_pullback: on a bound l for the round order of X, following the recursion of step1 on X, with the invariant "up to unit members".

theorem Hironaka.BMO.step1_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : ↑(step1 bo T' hT') = ((↑(step1 bo T hT)).pullback h).eraseEmpty

Step 1 on the pull-back data up to unit members is the pull-back of Step 1 with its empty blow-ups deleted (the second clause of [Kol07, 34.1] for Step 1), under the indifference of the input functors.

theorem Hironaka.BMO.sepIdeal_fullPullback {k : Type u} [Field k] [CharZero k] (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : sepIdeal (T'.fullPullback T h) = sepIdeal T'

The separating ideal of the full pull-back is the separating ideal of T': unit members are ignored by the split and by the separation order.

theorem Hironaka.BMO.sepTriple_fullPullback {k : Type u} [Field k] [CharZero k] (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) : sepTriple T' = let __src := T'.toTriple; { X := __src.X, smoothOfRelativeDimension := ⋯, I := sepIdeal (T'.fullPullback T h), isNonzeroEverywhere := ⋯, E := __src.E, isSnc := ⋯ }

The separating triple of T' is the separating triple of its full pull-back with the unit members deleted.

theorem Hironaka.BMO.sepTriple_isPullbackOf_of_eq {k : Type u} [Field k] [CharZero k] (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOf T h) (hsep : sepOrder T' = sepOrder T) : (sepTriple T').IsPullbackOf (sepTriple T) h

The separating triple of an exact pull-back with the same separation order is the pull-back of the separating triple (sepTriple_isPullbackOf without surjectivity).

theorem Hironaka.BMO.step2Round_eraseEmpty_pullback_of_eq {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') (hpos : 0 < sepOrder T) (hpos' : 0 < sepOrder T') (hs : sepOrder T' = sepOrder T) : step2Round bo T' hT' hpos' = ((step2Round bo T hT hpos).pullback h).eraseEmpty

A round of Step 2 with matching separation orders commutes with an arbitrary smooth morphism up to empty blow-ups (clause (2) of [Kol07, Theorem 103] with the second clause of [Kol07, 34.1], per round): the round of Step 2 on the pull-back data is the erased pull-back of the round.

theorem Hironaka.BMO.maxOrd_comap_sepIdeal_lt {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hpos : 0 < sepOrder T) (hlt : sepOrder T' < sepOrder T) : ((sepIdeal T).comap h).maxOrd < ↑(T.m * sepOrder T)

When the separation order of the pull-back data is smaller than that of X, the pulled-back separating ideal N(I')^m + I'^s (with X's s) has maximal order < ms: at a point of order ≥ m for I' the order of N(I') is at most the smaller separation order, and elsewhere ord I'^s < sm (Kollár's observation in [Kol07, 111, Step 2]).

theorem Hironaka.BMO.step2Round_pullback_eraseEmpty_eq_nil {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hpos : 0 < sepOrder T) (hlt : sepOrder T' < sepOrder T) : ((step2Round bo T hT hpos).pullback h).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil T'.X.left

The skipped round of Step 2: when the separation order of the pull-back data is smaller than that of X, the round pulls back to empty blow-ups only.

theorem Hironaka.BMO.step2_eraseEmpty_pullback_aux {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (l : ℕ) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] : T'.IsPullbackOfUpToUnits T h → ∀ (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T'), sepOrder T ≤ l → ↑(step2 bo T' hT') = ((↑(step2 bo T hT)).pullback h).eraseEmpty

The induction behind step2_eraseEmpty_pullback: on a bound l for the separation order of X, following the recursion of step2 on X, with the invariant "up to unit members".

theorem Hironaka.BMO.step2_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n m : ℕ} (bo : (d : ℕ) → BOData n d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hp : T'.IsPullbackOfUpToUnits T h) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m T') : ↑(step2 bo T' hT') = ((↑(step2 bo T hT)).pullback h).eraseEmpty

Step 2 on the pull-back data up to unit members is the pull-back of Step 2 with its empty blow-ups deleted (the second clause of [Kol07, 34.1] for Step 2), under the indifference of the input functors.