Functoriality of the geometric Step 3 on a marked triple under smooth surjections

The first clause of [Kol07, 34.1] for Step 3 of the proof of [Kol07, Theorem 107]: the geometric Step 3 of the pull-back data (Y, h^* I, m, h^{-1} E) is the pull-back of the geometric Step 3 of (X, I, m, E). Hironaka/Resolution/Algebraic/Monomial/Geometric/PullbackRun.lean proves it for a piece family refining the input family along h (realize_pullback_of_surjective), and Hironaka/Resolution/Algebraic/Monomial/Geometric/Refinement.lean produces the concrete refining family: the components of h^{-1} E with the exponents Φ.exponentAt ∘ h (refinesAlong_ofDivisorFamily). Step 3's input family on Y (step3Family) has the same components and labels but the exponents ord_η (h^* I) at the generic points η of the components of h^{-1} E: they agree with Φ.exponentAt (h η) because a flat morphism sends η to a generic point of the member (mem_genericPoints_support_of_flat), where the marked monomial ideal M(I) has the order of I (ord_monomialPart_of_mem_genericPoints) and the order of the monomial ideal is the sum over the single piece through the point (ord_monomial_eq_total, faceAt_eq_singleton_of_mem_genericPoints); this is exponentAt_step3Family_of_mem_genericPoints. The refining family is taken with Step 3's own enumeration of the components of h^{-1} E (componentsEquiv), so the two families on Y coincide outright (ofDivisorFamily_congr_of_forall); the pull-back data are canonical (T'.I = h^* I, T'.E = h^{-1} E, T'.m = m, the structure morphism h ≫ f), which the proof of step3Seq_pullback_of_surjective makes literal by destructuring T'.

theorem Hironaka.Monomial.PieceFamily.realize_congr_family {X : AlgebraicGeometry.Scheme} {Φ₁ Φ₂ : PieceFamily X} (e : Φ₁ = Φ₂) {n m : ℕ} (hV₁ : Φ₁.IsValid n m) (hV₂ : Φ₂.IsValid n m) : Φ₁.realize n m hV₁ = Φ₂.realize n m hV₂

The realized runs of two equal families, with any two validity proofs, coincide.

theorem Hironaka.BMO.exponentAt_step3Family_of_mem_genericPoints {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {j : T.E.ι} {x : ↥T.X.left} (hx : x ∈ (T.E.component j).support.genericPoints) : (step3Family T).exponentAt x = (T.I.ord x).toNat

At a generic point of a component of a member, the exponent of Step 3's input family is the order of I: the point lies on exactly one piece, whose exponent is the order of the marked monomial ideal M(I) there (ord_monomial_eq_total through monomial_exponentAt_step3Family), which is the order of I at a generic point.

theorem Hironaka.BMO.step3Seq_pullback_of_surjective {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') : step3Seq T' hT' = (step3Seq T hT).pullback h

The geometric Step 3 of a marked triple commutes with smooth surjections (the first clause of [Kol07, 34.1] for Step 3; [Kol07, 111]: "the functoriality conditions are just as obvious as before"): the input family of the pull-back data is the concrete refining family of refinesAlong_ofDivisorFamily, taken with Step 3's own enumeration of the components (componentsEquiv), up to the exponents, which agree at the generic points (exponentAt_step3Family_of_mem_genericPoints); the two families are then equal (ofDivisorFamily_congr_of_forall), and realize_pullback_of_surjective applies.