The dictionary between Hironaka's boundaries and Kollár's divisor families: the definitions

Hironaka's Main Theorem II [Hir64, Main Theorem II] speaks of one reduced closed subscheme E (an ideal sheaf) "with only normal crossings" [Hir64, Definition 2]; Kollár's simple normal crossing divisors [Kol07, Definition 24] are ordered finite families E = ∑ E^i of divisors (AlgebraicGeometry.Scheme.DivisorFamily). Both directions of the passage are needed to state Hironaka's theorem in terms of Kollár's sequences and vice versa:

• IdealSheafData.componentFamily E: the family of the irreducible components of V(E), each with its reduced structure (the vanishing ideal sheaf of the component), indexed by the generic points of V(E) (Closeds.genericPoints: the points of V(E) maximal for specialization, one per irreducible component) and ordered by a well-ordering of that index set. This reads Hironaka's "irreducible component (i.e., a maximal reduced irreducible subscheme) of E" [Hir64, Definition 2] as Kollár's "E = ∑ E^i with ordered index set" [Kol07, Definition 31]; the ordering plays no role in the dictionary.
• DivisorFamily.unionIdeal F: the reduced ideal sheaf of the union of the members of a family, the vanishing ideal sheaf of ⋃ᵢ V(E^i), Hironaka's red(⋃ E^i), the shape of his boundary E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)) in clause (iii) of Main Theorem II (reducedTransform).

The index set of componentFamily is finite on a Noetherian space (Closeds.genericPoints_finite: a closed set is a finite union of irreducible closed sets, Mathlib's NoetherianSpace.exists_finite_set_isClosed_irreducible, and each of these has at most one generic point), which is the Fintype instance Kollár's families carry. This module holds the definitions only; the dictionary itself is proved in Hironaka/Scheme/Snc/DictionaryOrder.lean, DictionaryBoundary.lean and DictionaryComponents.lean.

theorem TopologicalSpace.Closeds.genericPoints_finite {Y : Type u_1} [TopologicalSpace Y] [T0Space Y] [QuasiSober Y] [NoetherianSpace Y] (Z : Closeds Y) : Z.genericPoints.Finite

In a Noetherian sober T₀ space a closed set has finitely many generic points: it is a finite union of irreducible closed sets (Mathlib's NoetherianSpace.exists_finite_set_isClosed_irreducible), a generic point of Z is the generic point of the member containing it (maximality, Closeds.mem_genericPoints_iff), and an irreducible closed set has at most one generic point (T₀).

instance TopologicalSpace.Closeds.instFiniteGenericPoints {Y : Type u_1} [TopologicalSpace Y] [T0Space Y] [QuasiSober Y] [NoetherianSpace Y] (Z : Closeds Y) : Finite ↑Z.genericPoints

The generic points of a closed set of a Noetherian sober T₀ space form a finite type.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.componentFamily {X : Scheme} (E : X.IdealSheafData) [Finite ↑E.support.genericPoints] : X.DivisorFamily

The family of the irreducible components of the closed subscheme V(E), as a divisor family with ordered index set [Kol07, Definition 31]: indexed by the generic points of V(E) (Closeds.genericPoints; one per irreducible component), each component the closed set closure {η} with its reduced structure (the vanishing ideal sheaf), the index set ordered by a well-ordering (Mathlib's WellOrderingRel; the ordering is immaterial to the dictionary). These are Hironaka's "irreducible components (i.e., maximal reduced irreducible subschemes) of E" [Hir64, Definition 2]. Finite when X is Noetherian (Closeds.genericPoints_finite).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.DivisorFamily.unionIdeal {X : Scheme} (F : X.DivisorFamily) : X.IdealSheafData

The reduced ideal sheaf of the union of the members of a divisor family: the vanishing ideal sheaf of ⋃ᵢ V(E^i), Hironaka's red(∑ E^i), the operation behind the boundary red(f⁻¹(E) ∪ f⁻¹(D)) of [Hir64, Main Theorem II (iii)], applied to Kollár's total transform [Kol07, Definition 25] with the ordering forgotten.

Equations

• F.unionIdeal = AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal F.support