The principalization sequence commutes with closed embeddings when E = ∅

Clause (5) of [Kol07, Theorem 35], the functoriality for closed embeddings of [Kol07, 34.3]: for a closed embedding j : Y ↪ X of smooth k-schemes with 𝒪_X/I_X = j_*(𝒪_Y/I_Y) and E = ∅, BP(X, I_X, ∅) = j_* BP(Y, I_Y, ∅). With E empty the disjoining part of BP is empty (BP_of_isEmpty: BP T = BMO_1(X, I, 1, ∅)), so the clause is exactly [Kol07, Claim 71.2] for BMO_1, "the functoriality properties required in (35) follow … from (71.2)" [Kol07, 72]. Claim 71.2 is proved in Hironaka/Resolution/Algebraic/Stage/ClosedEmbeddingGeneral.lean for the functor at a fixed dimension (Hironaka.Stage.tower_bmo_one_eq_pushforward_closedEmbedding_aux); it is read here at the dimension of X through dimFreeBMO_seq_eq_tower (BMO_1 is the dimension-free functor, and the closed subscheme Y has dimension ≤ dim X, bmoClass_of_closedEmbedding). BP_eq_of_isEmpty says that BP does not see how an empty boundary is indexed, through the indifference of BMO_1 to unit members; with it the clause holds for any empty boundary on Y.

theorem Hironaka.Sequence.BP_pushforward_of_closedEmbedding {k : Type u} [Field k] [CharZero k] (TX TY : AlgebraicGeometry.Triple k) (j : TY.X.left ⟶ TX.X.left) [AlgebraicGeometry.IsClosedImmersion j] (hj : TX.ClosedEmbedding TY j) (hE : IsEmpty TX.E.ι) : BP TX = (BP TY).pushforward j

Clause (5) of [Kol07, Theorem 35]: for a closed embedding j : Y ↪ X carrying 𝒪_X/I_X = j_*(𝒪_Y/I_Y) and E = ∅, BP(X, I_X, ∅) = j_* BP(Y, I_Y, j^{-1} ∅). The disjoining part is empty (BP_of_isEmpty) and the BMO_1 part is [Kol07, Claim 71.2] at the dimension of X.

theorem Hironaka.Sequence.BP_eq_of_isEmpty {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (E' : T.X.left.DivisorFamily) (hE' : E'.IsSnc) (hE : IsEmpty T.E.ι) [IsEmpty E'.ι] : BP T = BP { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := E', isSnc := hE' }

BP does not see how an empty boundary is indexed: two triples on the same (X, I) whose boundaries both have empty index type have the same principalization sequence (the indifference of BMO_1 to unit members, at the dimension of X).