The principalization sequence: unfolding, the empty blow-up convention, the empty boundary

The first facts about Hironaka.Sequence.BP (Hironaka/Resolution/Algebraic/Kol07/Thm35/Principalization.lean): its unfolding (BP_eq); the empty blow-up convention of [Kol07, 32], "the final outputs of the named blow-up sequence functors … do not contain empty blow-ups", as a theorem (BP_noEmptyCenters, the definition deletes them); and the case of an empty boundary (BP_of_isEmpty): for E = ∅ the disjoining sequence is the empty sequence (disjoinSeq_of_isEmpty), so BP T is BMO_1(X, I, 1, ∅) itself, up to two transports. First, disjoinSeq T.E = nil holds only propositionally (Fintype.card of an empty index type is not 0 by rfl), so the disjoined triple (X', π^* I, ∑ E^i) lives on a scheme X' merely equal to X: concat_pullback_eqToHom moves the BMO_1 part across the eqToHom isomorphism, and the commutation of BMO_1 with smooth surjections [Kol07, 34.1] at that isomorphism (dimFreeBMO_commutesWithSmooth) identifies the value. Second, the collapsed family ∑ E^i of an empty E is not empty: it has the single member E^0 = ∏_{i ∈ ∅} … = 𝒪_X, the empty divisor (disjoinedFamily_component_bot, card_disjoinedFamily), so the two boundaries differ by one unit member, which the indifference of BMO_1 to unit members (dimFreeBMO_indifferentToEmptyMembers) removes along the unique order embedding out of the empty index type. Finally the output of BMO_1 has no empty center (OrderGeSeqAssignment.noEmptyCenters), so the eraseEmpty of the definition is the identity there (eraseEmpty_eq_self_iff).

The empty-boundary case is what the closed embedding clause of [Kol07, Theorem 35 (5)] reduces to, since that clause is stated for E = ∅.

theorem Hironaka.Sequence.BP_eq {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : BP T = ((disjoinSeq T.E).concat ((Stage.BMO_m 1 k).seq { toTriple := disjoinedTriple T, m := 1 } ⋯)).eraseEmpty

The unfolding of the principalization sequence, by definition.

theorem Hironaka.Sequence.BP_noEmptyCenters {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : (BP T).NoEmptyCenters

BP T has no empty center: the definition deletes them, as the empty blow-up convention of [Kol07, 32] requires.

theorem Hironaka.Sequence.eqToHom_comp_composite_of_eq_nil {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} (hS : S = AlgebraicGeometry.Scheme.BlowUpSequence.nil X) (p : X = S.last) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) S.composite = CategoryTheory.CategoryStruct.id X

A blow-up sequence that is (propositionally) the empty sequence has composite 𝟙 up to the identification of its last stage with the base.

theorem Hironaka.Sequence.BP_of_isEmpty {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (hE : IsEmpty T.E.ι) : BP T = (Stage.BMO_m 1 k).seq { toTriple := T, m := 1 } ⋯

For E = ∅ the principalization sequence is BMO_1(X, I, 1, ∅) itself: with k = 0 components there are no disjoining steps [Kol07, 72]. The proof moves the BMO_1 part across the eqToHom isomorphism X ≅ X' (concat_pullback_eqToHom, then the commutation of BMO_1 with smooth surjections [Kol07, 34.1] at the isomorphism) after removing the one unit member of the collapsed family by the indifference of BMO_1 to unit members; the final eraseEmpty is the identity since the output of BMO_1 has no empty center.