The empty boundary family on a smooth scheme

A small module in the closed-embedding chapter of the tower (Claim 71.2, [Kol07, 108]): it collects, through its imports, the descent of the identity along a smooth surjection (Hironaka.Sequence.seq_eq_pushforward_of_cover, the first bullet of [Kol07, 34.1] with the injectivity of pull-back along a flat surjection) and the transport Hironaka.Sequence.isNonzeroEverywhere_map_of_isClosedImmersion (the push-forward along a closed immersion of an ideal sheaf with nonzero stalks has nonzero stalks, which makes the intermediate triple (Y_i, (Y ↪ Y_i)_* J, 1, ∅) of Kollár's chain a triple in the sense of [Kol07, Notation 64]), and it holds one corollary: isSnc_of_isEmpty, a boundary family with no member is a simple normal crossing divisor on a smooth k-scheme.

theorem Hironaka.Stage.isSnc_of_isEmpty {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) [IsEmpty E.ι] : E.IsSnc

On a smooth k-scheme a boundary family without members is a simple normal crossing divisor [Kol07, Definition 24]: the instance-argument form of AlgebraicGeometry.isSnc_of_isEmpty.