The principalization sequence commutes with smooth morphisms and with change of fields

Clause (4) of [Kol07, Theorem 35]: the principalization commutes with smooth morphisms ([Kol07, 34.1], both clauses: with smooth surjections outright, and with a general smooth morphism up to the deletion of empty blow-ups) and with change of fields [Kol07, 34.2]. "The functoriality properties required in (35) follow from the corresponding functoriality properties in (69)" [Kol07, 72]: the definition BP T = (disjoinSeq T.E ⧺ BMO_1(disjoinedTriple T)).eraseEmpty is built from two functorial pieces, so the proofs are assemblies.

• The disjoining sequence pulls back (IsPullbackOf.disjoinSeq_eq, IsBaseChangeOf.disjoinSeq_eq, from disjoin_functorial in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Functorial.lean), and the disjoined triple of the pulled-back data is the pullback (resp. base change) of the disjoined triple along the lift Triple.disjoinedMap (disjoinedTriple_isPullbackOf, disjoinedTriple_isBaseChangeOf).
• The lift is smooth (smooth_disjoinedMap) and, over a surjection, surjective (surjective_disjoinedMap): it is a stage lift of the pullback through an eqToHom.
• So the functoriality of BMO_1 ([Kol07, Theorem 69 (2)]; dimFreeBMO_commutesWithSmooth, both clauses, and dimFreeBMO_commutesWithBaseChange) identifies the BMO_1 part of BP T' with the pullback of the BMO_1 part of BP T along the lift.
• The concatenation pulls back piecewise (pullback_concat, the second piece along pullbackLastHom), the eqToHom of disjoin_functorial is absorbed (concat_pullback_eqToHom, pullback_comp), and the deletion of the empty blow-ups commutes with a flat surjective pullback (eraseEmpty_pullback_of_flat_surjective); for a general smooth g the second clause of 34.1 deletes them once more on both sides (eraseEmpty_pullback_eraseEmpty', eraseEmpty_concat_eraseEmpty).

theorem AlgebraicGeometry.Triple.smooth_disjoinedMap {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {T : Triple k} {T' : Triple L} (g : T'.X.left ⟶ T.X.left) [Smooth g] (e : Hironaka.Sequence.disjoinSeq T'.E = (Hironaka.Sequence.disjoinSeq T.E).pullback g) : Smooth (disjoinedMap g e)

The lift disjoinedMap of a smooth g is smooth (an eqToHom followed by the last-stage lift of the pullback, smooth_pullbackLastHom).

theorem AlgebraicGeometry.Triple.surjective_disjoinedMap {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] {T : Triple k} {T' : Triple L} (g : T'.X.left ⟶ T.X.left) [Flat g] (hs : Function.Surjective ⇑g) (e : Hironaka.Sequence.disjoinSeq T'.E = (Hironaka.Sequence.disjoinSeq T.E).pullback g) : Function.Surjective ⇑(disjoinedMap g e)

The lift disjoinedMap of a flat surjection is surjective (surjective_pullbackLastHom).

theorem Hironaka.Sequence.BP_pullback_of_surjective {k : Type u} [Field k] [CharZero k] (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hs : Function.Surjective ⇑g) (h : T'.IsPullbackOf T g) : BP T' = (BP T).pullback g

Clause (4) of [Kol07, Theorem 35], the first clause of [Kol07, 34.1]: BP commutes with smooth surjections carrying the pullback data.

theorem Hironaka.Sequence.BP_pullback_eraseEmpty {k : Type u} [Field k] [CharZero k] (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (h : T'.IsPullbackOf T g) : BP T' = ((BP T).pullback g).eraseEmpty

Clause (4) of [Kol07, Theorem 35], the second clause of [Kol07, 34.1]: for every smooth g carrying the pullback data, BP T' is the pullback g^* BP T with its empty blow-ups deleted.

theorem Hironaka.Sequence.BP_baseChange {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (σ : k →+* L) (T : AlgebraicGeometry.Triple k) (T' : AlgebraicGeometry.Triple L) (p : T'.X.left ⟶ T.X.left) (h : T'.IsBaseChangeOf T σ p) : BP T' = (BP T).pullback p

Clause (4) of [Kol07, Theorem 35], the change of fields of [Kol07, 34.2]: for σ : k →+* L and a triple T' over L carrying the base-change data of T, BP T' is the pullback of BP T along the projection.