Clause (2) of marked order reduction: smooth morphisms, and indifference to empty members

Clause (2) of [Kol07, Theorem 107] with both clauses of [Kol07, 34.1]: BMO_{n,m} commutes with smooth morphisms. The first clause, for smooth surjections, is commutesWithSmoothSurjections (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Functoriality.lean); the second, for an arbitrary smooth h, says that BMO(Y, h^* I, m, h^{-1} E) is obtained from the pull-back h^* BMO(X, I, m, E) by deleting every blow-up whose centre is empty. The second clause is assembled here from the loops (step1_eraseEmpty_pullback, step2_eraseEmpty_pullback, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothLoop.lean) and Step 3 (step3Seq_eraseEmpty_pullback, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SmoothStep3.lean) through the tails of Functoriality.lean, for the invariant "pull-back up to unit members" (IsPullbackOfUpToUnits), under the indifference hboind of the input functors to unit boundary members: bmoSeq_eraseEmpty_pullback. Its two uses:

• commutesWithSmooth (hboind): the exact pull-back is a pull-back up to unit members (IsPullbackOf.upToUnits);
• indifferentToEmptyMembers (hboind) ([Kol07, 32] and the reindexing of [Kol07, 34.1] as a property of the functor): deleting unit members of the boundary is a pull-back up to unit members along the identity (isPullbackOfUpToUnits_id), and the pull-back along the identity with its empty blow-ups deleted is the sequence itself (pullback_id, eraseEmpty_bmoSeq).

The hypothesis hboind is discharged for the order-reduction data of dimension n in Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentGlobal.lean; the fields are assembled into BMOData in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Theorem107.lean.

theorem Hironaka.BMO.tailAfterStep2_eraseEmpty_pullback {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) (hT' : MarkedTriple.BMOClass n m T') (τ : { R : T.X.left.BlowUpSequence // R.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ R.NoEmptyCenters }) (τ' : { R : T'.X.left.BlowUpSequence // R.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E ∧ R.NoEmptyCenters }) (e : ↑τ' = ((↑τ).pullback h).eraseEmpty) : tailAfterStep2 T' hT' τ' = ((tailAfterStep2 T hT τ).pullback h).eraseEmpty

The tail after Step 2 under an arbitrary smooth morphism: if the Step-2 value on the pull-back data up to unit members is the erased pull-back of the Step-2 value, so is the tail (Step 3), along the last-stage isomorphism followed by the last-stage lift (step3Seq_eraseEmpty_pullback, IsPullbackOfUpToUnits.induced_eraseEmpty).

theorem Hironaka.BMO.tailAfterStep1_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (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') (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ S.NoEmptyCenters) (hS' : (S.pullback h).eraseEmpty.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E ∧ (S.pullback h).eraseEmpty.NoEmptyCenters) : tailAfterStep1 bo T' hT' ⟨(S.pullback h).eraseEmpty, hS'⟩ = ((tailAfterStep1 bo T hT ⟨S, hS⟩).pullback (S.pullbackLastHom h)).eraseEmpty.pullback (S.pullback h).eraseEmptyLastHom

The tail after Step 1 under an arbitrary smooth morphism: the tail (Steps 2 and 3) on the erased pull-back of a Step-1 value is the erased pull-back of the tail along the last-stage lift, carried along the last-stage isomorphism (step2_eraseEmpty_pullback on the induced marked triples, then tailAfterStep2_eraseEmpty_pullback).

theorem Hironaka.BMO.concat_tailAfterStep1_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (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') (σ : { S : T.X.left.BlowUpSequence // S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E ∧ S.NoEmptyCenters }) (σ' : { S : T'.X.left.BlowUpSequence // S.IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E ∧ S.NoEmptyCenters }) (e : ↑σ' = ((↑σ).pullback h).eraseEmpty) : (↑σ').concat (tailAfterStep1 bo T' hT' σ') = (((↑σ).concat (tailAfterStep1 bo T hT σ)).pullback h).eraseEmpty

The whole assembly under an arbitrary smooth morphism: if the Step-1 value on the pull-back data up to unit members is the erased pull-back of the Step-1 value, the concatenation with the tail is the erased pull-back of the concatenation (pullback_concat, eraseEmpty_concat, tailAfterStep1_eraseEmpty_pullback).

theorem Hironaka.BMO.bmoSeq_eraseEmpty_pullback {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (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') : bmoSeq bo T' hT' = ((bmoSeq bo T hT).pullback h).eraseEmpty

For a marked triple that is the pull-back of T up to unit boundary members along a smooth h, BMO_{n,m} is the pull-back of BMO_{n,m}(T) with its empty blow-ups deleted (the second clause of [Kol07, 34.1]), under the indifference of the input functors: the skipped rounds and the matched rounds of Steps 1–2, then Step 3, assembled through the tails.

theorem Hironaka.BMO.commutesWithSmooth {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) : (functor bo m).CommutesWithSmooth

BMO_{n,m} commutes with smooth morphisms (clause (2) of [Kol07, Theorem 107] with both clauses of [Kol07, 34.1]), given the indifference of every input functor bo d to empty boundary members (hboind): the surjective clause is commutesWithSmoothSurjections; for a general smooth h the rounds of Steps 1–2 at parameters above Y's pull back to empty blow-ups (pullback_eraseEmpty_eq_nil_of_maxOrd_lt, the skipped-round argument), leaving unit boundary members that only hboind lets the two runs ignore, and Step 3 is realize_pullback_eraseEmpty.

theorem Hironaka.BMO.indifferentToEmptyMembers {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) : (functor bo m).IndifferentToEmptyMembers

BMO_{n,m} is indifferent to empty boundary members ([Kol07, 32] and the reindexing of [Kol07, 34.1] as a property of the functor), given the indifference of every input functor bo d (hboind): deleting unit members of the boundary is a pull-back up to unit members along the identity, so the run on the smaller boundary is the run on the larger one pulled back along the identity and erased, that is, the run itself (eraseEmpty_bmoSeq).