The reduced union of a simple normal crossing family is a Cartier divisor

Hironaka's definition of a reduced subscheme E with only normal crossings [Hir64, Definition 2] presupposes that the ideal sheaf of E is invertible; Kollár's principalization theorem produces the pull-back of an ideal as a monomial ideal ∏ F_j^{a_j} on a simple normal crossing family F [Kol07, Theorem 35 (2)]. Clause (iii) of [Hir64, Corollary 3] needs the reduced inverse image, that is the radical of that monomial ideal, to be invertible with only normal crossings. This module supplies the two facts, beside unionIdeal_eq_radical_prod and IsSnc.isSncBoundary_unionIdeal:

• isInvertible_unionIdeal_of_isSnc: the reduced union unionIdeal F of a simple normal crossing family on a locally Noetherian scheme smooth over k is defined by an invertible sheaf of ideals, checked at the stalks (isInvertible_of_forall_stalkIdeal_eq_span). At a point x its stalk is the radical of span {∏ z_{c(i)}}, the product of the pairwise distinct transversal coordinates of the members through x, which is its own radical since the coordinates are prime and pairwise non-dividing (IsLocalRing.isRadical_span_prod), and a product of nonzero elements of the regular local ring is a non-zero-divisor.
• radical_prod_pow_eq_unionIdeal_subfamily: the radical of ∏ F_j^{a_j} is the reduced union of the sub-family of members with positive multiplicity (both are the vanishing ideal of the same closed set).

theorem Hironaka.Sequence.isInvertible_unionIdeal_of_isSnc {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) : F.unionIdeal.IsInvertible

The reduced union of a simple normal crossing family [Kol07, Definition 24] on a locally Noetherian scheme smooth over k is defined by an invertible sheaf of ideals, as [Hir64, Definition 2] presupposes (checked at the stalks, isInvertible_of_forall_stalkIdeal_eq_span): at a point x its stalk is the radical of the product of the stalks of the members, span {∏ z_{c(i)}} over the members through x (prod_stalkIdeal_eq_span), which is its own radical since the z_{c(i)} are pairwise distinct members of a regular system of parameters, prime and pairwise non-divisible (isRadical_span_prod), and a product of nonzero elements of the regular local ring is a non-zero-divisor.

theorem Hironaka.Sequence.radical_prod_pow_eq_unionIdeal_subfamily {X : AlgebraicGeometry.Scheme} (F : X.DivisorFamily) (a : F.ι → ℕ) : (∏ j : F.ι, F.component j ^ a j).radical = (F.subfamily fun (j : F.ι) => a j ≠ 0).unionIdeal

The radical of the monomial ideal ∏ F_j^{a_j} of a family (the shape of the pull-back in [Kol07, Theorem 35 (2)]) is the reduced union of the sub-family of members with positive multiplicity: both are the vanishing ideal of the same closed set (vanishingIdeal_support, support_finset_prod, support_pow).