Appending an empty member to a simple normal crossing family

The total transform of a divisor family appends the exceptional divisor as a last member [Kol07, Definition 25], which under a trivial blow-up is EMPTY (the unit ideal); the restricted marked triple of the boundary-clearing step carries such a member, and clause (3) of [Kol07, Lemma 102] compares it with Kollár's (E − E^j)|_{E^j}, which has none. This module holds the one fact that comparison needs: appending the unit ideal as a member keeps a family snc (isSnc_append_top) — the new member passes through no point, so the coordinates of [Kol07, Definition 24] at every point are unchanged, and the empty subscheme is regular vacuously.

theorem AlgebraicGeometry.Scheme.DivisorFamily.support_top_eq_bot {X : Scheme} : ⊤.support = ⊥

The unit ideal has empty support.

theorem AlgebraicGeometry.Scheme.DivisorFamily.isSnc_append_top {X : Scheme} (E : X.DivisorFamily) (hE : E.IsSnc) : (E.append ⊤).IsSnc

Appending the unit ideal — an empty member — to an snc family keeps it snc [Kol07, Definition 24]: the empty subscheme is regular vacuously, and the new member passes through no point, so the coordinates and the injection of Definition 24 at each point are those of the old family.