Clause (2) of marked order reduction: smooth surjections

Clause (2) of [Kol07, Theorem 107] with the first clause of [Kol07, 34.1] ("B commutes with every smooth surjection h"; [Kol07, 111]: "the functoriality conditions are just as obvious as before"): BMO_{n,m}(Y, h^* I, m, h^{-1} E) = h^* BMO_{n,m}(X, I, m, E) for a smooth surjection h. The functor is the concatenation Step 1 ++ Step 2 ++ Step 3 on the marked triples induced after each step (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean); the pull-back of a concatenation is the concatenation of the pull-backs, the later ones along the last-stage lifts (pullback_concat), and each step commutes with the smooth surjective lift on the induced marked triple, which carries the pull-back data of the triple induced on X (MarkedTriple.isPullbackOf_induced_last): Step 1 by step1_pullback_of_surjective, Step 2 by step2_pullback_of_surjective (Hironaka/Resolution/Algebraic/MarkedOrderReduction/LoopFunctorial.lean) and Step 3 by step3Seq_pullback_of_surjective (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Functorial.lean). The step values are carried as subtype values (the sequence with its order and no-empty-centres proofs) through the tails tailAfterStep2 (after Step 2) and tailAfterStep1 (after Step 1), so that the equality of a step on Y with the pull-back of the step on X is substituted into the induced marked triple of the next step without motive problems (tailAfterStep2_pullback, tailAfterStep1_pullback, concat_tailAfterStep1_pullback). The second clause of [Kol07, 34.1], for an arbitrary smooth morphism, is Hironaka/Resolution/Algebraic/MarkedOrderReduction/Smooth.lean.

noncomputable def Hironaka.BMO.tailAfterStep2 {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : MarkedTriple k) (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 }) : T.X.left.BlowUpSequence

Step 3 of BMO_{n,m} after a Step-2 value τ (the sequence with its proofs) on the marked triple T induced after Step 1, run on the marked triple induced at the end of τ: the tail of the concatenation after Step 2.

Equations

• Hironaka.BMO.tailAfterStep2 T hT τ = (↑τ).concat (Hironaka.BMO.step3Seq (T.induced ↑τ ⋯ (Fin.last (↑τ).length)) ⋯)

noncomputable def Hironaka.BMO.tailAfterStep1 {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T : MarkedTriple k) (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 }) : (↑σ).last.BlowUpSequence

Steps 2 and 3 of BMO_{n,m} after a Step-1 value σ (the sequence with its proofs), on the marked triple induced at its end: the tail of the concatenation bmoSeq.

Equations

• Hironaka.BMO.tailAfterStep1 bo T hT σ = Hironaka.BMO.tailAfterStep2 (T.induced ↑σ ⋯ (Fin.last (↑σ).length)) ⋯ (Hironaka.BMO.step2 bo (T.induced ↑σ ⋯ (Fin.last (↑σ).length)) ⋯)

theorem Hironaka.BMO.bmoSeq_eq_concat_tailAfterStep1 {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) : bmoSeq bo T hT = (↑(step1 bo T hT)).concat (tailAfterStep1 bo T hT (step1 bo T hT))

bmoSeq is Step 1 followed by its tail (definitional; the class proofs are irrelevant).

theorem Hironaka.BMO.tailAfterStep2_pullback {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hp : T'.IsPullbackOf 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) : tailAfterStep2 T' hT' τ' = (tailAfterStep2 T hT τ).pullback h

The tail after Step 2 under a smooth surjection: if the Step-2 value on the pull-back data is the pull-back of the Step-2 value, the tail (Step 3) on the pull-back data is the pull-back of the tail, by step3Seq_pullback_of_surjective on the marked triples induced after Step 2, along the last-stage lift, which is smooth and surjective.

theorem Hironaka.BMO.tailAfterStep1_pullback {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hp : T'.IsPullbackOf 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).IsOrderGeSeq (T'.X.left ↘ AlgebraicGeometry.Spec ↧k) T'.I T'.m T'.E ∧ (S.pullback h).NoEmptyCenters) : tailAfterStep1 bo T' hT' ⟨S.pullback h, hS'⟩ = (tailAfterStep1 bo T hT ⟨S, hS⟩).pullback (S.pullbackLastHom h)

The tail after Step 1 under a smooth surjection: the tail (Steps 2 and 3) on the pull-back of a Step-1 value is the pull-back of the tail along the last-stage lift, by step2_pullback_of_surjective on the induced marked triples (the lift is smooth and surjective, and the induced triple carries the pull-back data), then tailAfterStep2_pullback.

theorem Hironaka.BMO.concat_tailAfterStep1_pullback {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T T' : MarkedTriple k) (h : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth h] (hs : Function.Surjective ⇑h) (hp : T'.IsPullbackOf 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) : (↑σ').concat (tailAfterStep1 bo T' hT' σ') = ((↑σ).concat (tailAfterStep1 bo T hT σ)).pullback h

The whole assembly under a smooth surjection: if the Step-1 value on the pull-back data is the pull-back of the Step-1 value, the concatenation with the tail on the pull-back data is the pull-back of the concatenation (pullback_concat, tailAfterStep1_pullback).

theorem Hironaka.BMO.commutesWithSmoothSurjections {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} : (functor bo m).CommutesWithSmoothSurjections

BMO_{n,m} commutes with smooth surjections (clause (2) of [Kol07, Theorem 107] with the first clause of [Kol07, 34.1]): the round parameters are preserved (roundOrder_of_isPullbackOf, sepOrder_of_isPullbackOf), each round commutes by the field commutesWithSmooth of the order-reduction data, and Step 3 by realize_pullback_of_surjective on the refining family refinesAlong_ofDivisorFamily taken with Step 3's own enumeration of the components (the two families coincide by ofDivisorFamily_congr_of_forall); no round is skipped and no blow-up is deleted.