Making the components of a divisor disjoint: the definitions

The principalization theorem [Kol07, Theorem 35] takes a simple normal crossing divisor E = E_1 + ⋯ + E_k without an order on its components (a DivisorFamily, whose index order the construction must not use), while the order reduction theorems [Kol07, Theorems 68 and 69] take a divisor with an ordered index set. Kollár removes the mismatch without choosing an order [Kol07, 72]: if the irreducible components of E happen to be disjoint, "we can just declare that E is a single divisor", the components of E being allowed to be reducible in Theorem 68; and disjointness is achieved by k − 1 preliminary smooth blow-ups whose centers are defined from E alone: Z_t ⊆ X_t is the subset where k − t of the birational transforms (π_0 ⋯ π_{t-1})^{-1}_* E_i intersect (Kollár writes out the first two steps, Z_1 being "the subset where k − 1 of the (π_0)^{-1}_* E_i intersect").

This module holds the definitions; their properties are proved in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/.

• meetLocus G m: the points lying on at least m members of a finite family G of closed subschemes (Kollár's "subset where m of the E_i intersect"); DivisorFamily.singularLocus is the case m = 2.
• disjoinCenter G m: the ideal sheaf of the union of the m-fold intersections, each taken with the scheme structure ∑_{i ∈ s} G_i, that is ∏_{s, |s| = m} ∑_{i ∈ s} G_i. Its support is meetLocus G m; under the hypotheses of the construction (an snc family with no (m+1)-fold intersections) its stalks are generated by coordinates, so it is the reduced subscheme on Kollár's subset. The product-and-sum form is chosen because the inverse image ideal sheaf commutes with ∏ and ⨆ on the nose, which is what makes the construction functorial with no reducedness argument.
• disjoinSeqAux m G: the blow-up sequence of Kollár's steps at the multiplicities m, m − 1, …, 2: blow up disjoinCenter G m, replace every G_i by its strict transform, and continue with m − 1; nothing to do for m ≤ 1. disjoinSeq E := disjoinSeqAux k E.component with k the number of components: k − 1 steps.
• DivisorFamily.collapse F p: the components of F satisfying p declared a single (reducible) divisor ∏_{p a} F_a, placed first; the other components keep their order. asSingle E is the one-component family ∏_i E_i (Kollár's "declare that E is a single divisor").
• BlowUpSequence.originalIdx S E i: the index, inside the total transform totalTransformSeq E i at stage i ([Kol07, Definition 25], each exceptional divisor receiving the largest index as in [Kol07, Definition 65]), of the birational transform (π_0 ⋯ π_{i-1})^{-1}_* E_a of the component E_a: the iterated inl.
• collapsedFamily S E: the total transform of E at the end of a sequence S with the transforms of the original components collapsed into one member. At S = disjoinSeq E it is Kollár's E^0 < E^1 < ⋯ < E^{k-1} on X', with E^0 = π^{-1}_*(E_1 + ⋯ + E_k); the remaining components are the birational transforms of the exceptional divisors F^1, …, F^{k-1} in the order of the total transform.

The disjoined triple (X', π^* I, ∑ E^i) (Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin/Triple.lean) is the input of the marked order reduction functor in the construction of the principalization functor.

def Hironaka.Sequence.meetLocus {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (m : ℕ) : TopologicalSpace.Closeds ↥X

The closed set of points lying on at least m members of the family G, Kollár's "subset where m of the E_i intersect" [Kol07, 72]. For m = 2 this is DivisorFamily.singularLocus; for m = 0 it is everything; for m larger than the number of members it is empty.

Equations

• Hironaka.Sequence.meetLocus G m = ⨆ s ∈ Finset.powersetCard m Finset.univ, ⨅ i ∈ s, (G i).support

noncomputable def Hironaka.Sequence.disjoinCenter {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (m : ℕ) : X.IdealSheafData

The center of a disjoining step [Kol07, 72]: the ideal sheaf of the union of the m-fold intersections of the members of G, the intersection over s carrying the scheme structure ∑_{i ∈ s} G_i. Its support is meetLocus G m (support_disjoinCenter); for an snc family with no (m+1)-fold intersections it is the reduced subscheme on that set (disjoinCenter_eq_vanishingIdeal).

Equations

• Hironaka.Sequence.disjoinCenter G m = ∏ s ∈ Finset.powersetCard m Finset.univ, ⨆ i ∈ s, G i

noncomputable def Hironaka.Sequence.disjoinSeqAux {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} : (ι → X.IdealSheafData) → X.BlowUpSequence

The disjoining steps of [Kol07, 72] at the multiplicities m, m − 1, …, 2: blow up disjoinCenter G m, replace each member by its strict transform (Kollár's (π_t)^{-1}_* E_i), continue at multiplicity m − 1; the empty sequence for m ≤ 1.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Sequence.disjoinSeqAux 0 x✝ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹
• Hironaka.Sequence.disjoinSeqAux 1 x✝ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹

noncomputable def Hironaka.Sequence.disjoinSeq {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : X.BlowUpSequence

The disjoining sequence of E [Kol07, 72]: with k the number of components, Z_0 the locus where all k meet, Z_1 ⊆ X_1 where k − 1 of the birational transforms meet, and so on down to the pairwise intersections; k − 1 smooth blow-ups (length_disjoinSeq). Defined from E.component alone: the order of E.ι plays no role (disjoinSeq_of_equiv).

Equations

• Hironaka.Sequence.disjoinSeq E = Hironaka.Sequence.disjoinSeqAux (Fintype.card E.ι) E.component

def AlgebraicGeometry.Scheme.DivisorFamily.asSingle {X : Scheme} (E : X.DivisorFamily) : X.DivisorFamily

"Declare that E is a single divisor" [Kol07, 72]: the one-component family whose component is the divisor E_1 + ⋯ + E_k, that is the ideal sheaf ∏_i E_i (the convention for the ideal of an effective divisor supported on the family, IsIdealOfSncDivisor). It is an snc family exactly when the E_i are pairwise disjoint (asSingle_isSnc).

Equations

• E.asSingle = { ι := PUnit.{?u.1 + 1}, fintype := PUnit.fintype, linearOrder := PUnit.instLinearOrder, component := fun (x : PUnit.{?u.1 + 1}) => ∏ i : E.ι, E.component i }

noncomputable def AlgebraicGeometry.Scheme.DivisorFamily.collapse {X : Scheme} (F : X.DivisorFamily) (p : F.ι → Prop) [DecidablePred p] : X.DivisorFamily

The components of F satisfying p declared a single (reducible) divisor ∏_{p a} F_a and placed first (⊥), the other components in their original order. Kollár's E^0 < E^1 < ⋯ < E^{k-1} [Kol07, 72] is the collapse of the total transform of E along the disjoining sequence onto the transforms of the original components (collapsedFamily).

Equations

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

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.originalIdx {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) : E.ι → (S.totalTransformSeq E i).ι

The index of the birational transform (π_0 ⋯ π_{i-1})^{-1}_* E_a of the component E_a inside the total transform totalTransformSeq E i at stage i ([Kol07, Definition 25], each blow-up appending its exceptional divisor at the end as in [Kol07, Definition 65]): the iterated inl.

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝²).originalIdx x✝¹ x_7 x✝ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝² D rest).originalIdx x✝¹ ⟨0, isLt⟩ x✝ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝² D rest).originalIdx x✝¹ ⟨j.succ, h⟩ x✝ = rest.originalIdx (x✝¹.totalTransform D) ⟨j, ⋯⟩ (toLex (Sum.inl x✝))

noncomputable def Hironaka.Sequence.collapsedFamily {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) : S.last.DivisorFamily

The total transform of E at the last stage of a sequence S ([Kol07, Definition 25]) with the birational transforms of the original components collapsed into one member. At the disjoining sequence it is Kollár's ordered family E^0 < E^1 < ⋯ < E^{k-1} on X' = X_{k-1} [Kol07, 72], with E^0 = π^{-1}_*(E_1 + ⋯ + E_k) (disjoinedFamily_component_bot), the remaining components being the birational transforms of the exceptional divisors F^1, …, F^{k-1} in the order of the total transform (disjoinedFamily_component_coe).

Equations

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