The clauses from the end data of the loop

Clause (c) of [Wlo05, Theorem 1.0.2] and the fine form of clause (e) for BED, derived from the end data EmbeddedEnd ⟨TX, 1⟩ (componentIdeals TX) ∅ (BED TX) taken as a hypothesis h; the proof of the theorem obtains the end data from CP1–CP6 (embeddedEnd_BED_of_invCE, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge).

• BED_strictTransform_last_smooth_of_embeddedEnd, BED_hasSncWith_strictTransform_last_of_embeddedEnd — clause (c): the final strict transform of the reduced Y is smooth and has simple normal crossings with the final boundary. The end data give them for the members — the irreducible components of Y — whose final strict transforms are pairwise disjoint, and the final strict transform of Y is their product (strictTransformSeq_eq_prod_of_pairwise_disjoint: reduced, same support).
• BED_comap_composite_eq_strictTransform_mul_sncDivisor_of_embeddedEnd — clause (e) in the fine form of [Wlo05, Theorem 4.7.1], σ^*(I_Y) = M(σ^*(I_Y)) · I_Ỹ: σ^*(I_Y) = I_Ỹ · J with J the ideal of an snc divisor supported on the final boundary. [Kol07, 72] writes σ^*(I_Y) as the final marked transform times the product of the pulled-back exceptional divisors; the end data identify the final marked transform with I_Ỹ, and isIdealOfSncDivisor_prod_comap_exceptionalAt (Hironaka.Resolution.Algebraic.Kol07.ExceptionalMonomial) makes the product an snc divisor supported on the final boundary.

It also proves the elementary identity iInf_componentIdeals_eq: a reduced ideal is the intersection of the reduced ideals of the irreducible components of its support. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.

theorem Hironaka.Resolution.iInf_componentIdeals_eq {k : Type u} [Field k] (TX : AlgebraicGeometry.Triple k) [AlgebraicGeometry.IsReduced TX.I.subscheme] : ⨅ c ∈ componentIdeals TX, c = TX.I

A reduced ideal is the intersection of the reduced ideals of the irreducible components of its support (the decomposition of Y in [Wlo05, Theorem 4.7.1]): the Galois connection between supports and vanishing ideals (vanishingIdeal_iSup), the union coe_support_eq_biUnion_componentIdeals and vanishingIdeal_support_of_isReduced.

theorem Hironaka.Resolution.pairwise_disjoint_strictTransformSeq_BED_last_of_embeddedEnd {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (h : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)) : (↑(componentIdeals TX)).Pairwise fun (a b : TX.X.left.IdealSheafData) => Disjoint ((BED TX).strictTransformSeq a (Fin.last (BED TX).length)).support ((BED TX).strictTransformSeq b (Fin.last (BED TX).length)).support

The final strict transforms of the irreducible components of Y are pairwise disjoint ([Wlo05, Theorem 4.7.1]), from the end data.

theorem Hironaka.Resolution.strictTransformSeq_BED_last_eq_prod_of_embeddedEnd {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) [AlgebraicGeometry.IsReduced TX.I.subscheme] (h : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)) : (BED TX).strictTransformSeq TX.I (Fin.last (BED TX).length) = ∏ c ∈ componentIdeals TX, (BED TX).strictTransformSeq c (Fin.last (BED TX).length)

The final strict transform of Y is the product of the final strict transforms of its irreducible components, from the end data.

theorem Hironaka.Resolution.BED_hasSncWith_strictTransform_last_of_embeddedEnd {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) [AlgebraicGeometry.IsReduced TX.I.subscheme] (h : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)) : ((BED TX).totalTransformSeq TX.E (Fin.last (BED TX).length)).HasSncWith ((BED TX).strictTransformSeq TX.I (Fin.last (BED TX).length))

Clause (c) of [Wlo05, Theorem 1.0.2], second part, from the end data: the final total transform of the boundary has simple normal crossings with the final strict transform of Y.

theorem Hironaka.Resolution.BED_strictTransform_last_smooth_of_embeddedEnd {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) [AlgebraicGeometry.IsReduced TX.I.subscheme] (h : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp ((BED TX).strictTransformSeq TX.I (Fin.last (BED TX).length)).subschemeι (CategoryTheory.CategoryStruct.comp (BED TX).composite (TX.X.left ↘ AlgebraicGeometry.Spec ↧k)))

Clause (c) of [Wlo05, Theorem 1.0.2], first part, from the end data: the final strict transform of Y is smooth over k.

theorem Hironaka.Resolution.BED_comap_composite_eq_strictTransform_mul_sncDivisor_of_embeddedEnd {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) [AlgebraicGeometry.IsReduced TX.I.subscheme] (h : EmbeddedEnd { toTriple := TX, m := 1 } (componentIdeals TX) ∅ (BED TX)) : ∃ (J : ((BED TX).stage (Fin.last (BED TX).length)).IdealSheafData), J.IsIdealOfSncDivisor ∧ J.support ≤ ((BED TX).totalTransformSeq TX.E (Fin.last (BED TX).length)).support ∧ TX.I.comap (BED TX).composite = (BED TX).strictTransformSeq TX.I (Fin.last (BED TX).length) * J

Clause (e) of [Wlo05, Theorem 1.0.2] in the fine form of [Wlo05, Theorem 4.7.1], from the end data: the pull-back of I_Y to the end result is the final strict transform of Y times the ideal of a simple normal crossing divisor supported on the final boundary.