The strict transform of a reduced subscheme is the product of those of its components

Clause (c) of [Wlo05, Theorem 1.0.2] speaks of the strict transform Ỹ of the reduced subscheme Y, while [Wlo05, Theorem 4.7.1] and its proof work with the strict transforms of the irreducible components Y_i. The bridge is bookkeeping about strict transforms of reduced ideals, assembled here from Hironaka/Resolution/Algebraic/Wlo05/EmbeddedPullbackTools.lean (the strict transform of a reduced closed subscheme stays reduced along a sequence, isReduced_strictTransformSeq_subscheme; the support of the strict transform of a finite union is the union of the strict transforms' supports, coe_support_strictTransformSeq_biUnion; a reduced ideal is the vanishing ideal of its support, vanishingIdeal_support_of_isReduced): when the strict transforms of the components at a stage are pairwise disjoint, the strict transform of Y at that stage is their product (vanishingIdeal_iSup_support_eq_prod), and simple normal crossings with the boundary pass from the factors to the product pointwise.

theorem Hironaka.Sequence.strictTransformSeq_eq_prod_of_pairwise_disjoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) [AlgebraicGeometry.IsReduced J.subscheme] {ι : Type v} (C : Finset ι) (c : ι → X.IdealSheafData) (hc : ∀ a ∈ C, AlgebraicGeometry.IsReduced (c a).subscheme) (hJ : ↑J.support = ⋃ a ∈ C, ↑(c a).support) (i : Fin (S.length + 1)) (hdisj : (↑C).Pairwise fun (a b : ι) => Disjoint (S.strictTransformSeq (c a) i).support (S.strictTransformSeq (c b) i).support) : S.strictTransformSeq J i = ∏ a ∈ C, S.strictTransformSeq (c a) i

The strict transform of a reduced ideal whose support is the union of the supports of finitely many reduced ideals is, at a stage where the strict transforms of those are pairwise disjoint, the product of their strict transforms: both sides are reduced with the same support. This passes from the disjoint strict transforms of the components in [Wlo05, Theorem 4.7.1] to the strict transform of the subvariety in [Wlo05, Theorem 1.0.2 (c)].

theorem Hironaka.Sequence.hasSncWith_prod_of_pairwise_disjoint {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) {ι : Type v} (A : Finset ι) (I : ι → X.IdealSheafData) (hdisj : (↑A).Pairwise fun (a b : ι) => Disjoint (I a).support (I b).support) (h : ∀ a ∈ A, E.HasSncWith (I a)) : E.HasSncWith (∏ a ∈ A, I a)

Simple normal crossings with a family pass from finitely many pairwise disjoint closed subschemes to their product: at a point of the product's support exactly one factor passes, and the product's stalk is that factor's stalk.