The center of a disjoining step is smooth and has normal crossings with the family

Kollár's next center Z_1 ⊂ X_1 is the subset where k − 1 of the (π_0)^{-1}_* E_i intersect, and "Z_1 is smooth since" these transforms have no k-fold intersections [Kol07, 72]. At a point x of the meet locus at multiplicity m + 1 exactly m + 1 members pass (at least m + 1 by membership, at most m + 1 since there are no (m+2)-fold intersections); the coordinates z at x of [Kol07, Definition 24] for the snc family the members belong to make those members the coordinate hyperplanes z_{c(i)} = 0, and the center ∏_{|s| = m+1} ∑_{i ∈ s} G_i has stalk (z_{c(i)} : i through x): the factor for the set of members through x is that ideal, every other (m+1)-set contains a member missing x, whose stalk is the unit ideal, so its factor is the unit ideal. Hence the center has simple normal crossings with the family ([Kol07, Definition 24 (4)]), and is smooth over k.

• mem_meetLocus_iff_le_card: x lies on at least m members iff the set of members through x has at least m elements.
• exists_stalkIdeal_disjoinCenter_eq_span: the stalk computation.
• hasSncWith_disjoinCenter, smooth_disjoinCenter: one disjoining step.
• isRegular_subscheme_of_hasSncWith, smooth_of_hasSncWith: a closed subscheme with simple normal crossings with a family is regular, and smooth over a perfect field; restatements of AlgebraicGeometry.HasSncWith.isRegular and HasSncWith.smooth under the names used here.

theorem Hironaka.Sequence.stalkIdeal_biSup_finset {X : AlgebraicGeometry.Scheme} {σ : Type u_1} (s : Finset σ) (J : σ → X.IdealSheafData) (x : ↥X) : (⨆ i ∈ s, J i).stalkIdeal x = ⨆ i ∈ s, (J i).stalkIdeal x

The stalk of a supremum over a finite set is the supremum of the stalks.

theorem Hironaka.Sequence.mem_meetLocus_iff_le_card {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (m : ℕ) (x : ↥X) [DecidablePred fun (i : ι) => x ∈ (G i).support] : x ∈ meetLocus G m ↔ m ≤ {i : ι | x ∈ (G i).support}.card

x lies on at least m members of G iff at least m members pass through x.

theorem Hironaka.Sequence.exists_stalkIdeal_disjoinCenter_eq_span {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] {F : X.DivisorFamily} (G : ι → X.IdealSheafData) (hG : ∀ (i : ι), G i ∈ Set.range F.component) {m : ℕ} (hm : meetLocus G (m + 2) = ⊥) {x : ↥X} (hx : x ∈ meetLocus G (m + 1)) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (hz : F.IsSncAt x z) : ∃ (s : Finset (Fin n)), (disjoinCenter G (m + 1)).stalkIdeal x = Ideal.span (z '' ↑s) ∧ (∀ (i : ι), x ∈ (G i).support → ∃ j ∈ s, (G i).stalkIdeal x = Ideal.span {z j}) ∧ ∀ j ∈ s, ∃ (i : ι), x ∈ (G i).support ∧ (G i).stalkIdeal x = Ideal.span {z j}

At a point x of the meet locus at multiplicity m + 1, for members G of a family with Kollár's coordinates z at x and no (m+2)-fold intersections, the center's stalk is generated by the coordinates of the members through x [Kol07, 72].

theorem Hironaka.Sequence.hasSncWith_disjoinCenter {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] {F : X.DivisorFamily} (hF : F.IsSnc) (G : ι → X.IdealSheafData) (hG : ∀ (i : ι), G i ∈ Set.range F.component) (m : ℕ) (hm : meetLocus G (m + 2) = ⊥) : F.HasSncWith (disjoinCenter G (m + 1))

"Z_1 is smooth since the (π_0)^{-1}_* E_i do not have any k-fold intersections" [Kol07, 72]: the center at multiplicity m + 1 of members of an snc family with no (m+2)-fold intersections has simple normal crossings with the family ([Kol07, Definition 24 (4)]).

theorem Hironaka.Sequence.isRegular_subscheme_of_hasSncWith {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} {Z : X.IdealSheafData} (h : E.HasSncWith Z) : AlgebraicGeometry.IsRegular Z.subscheme

A closed subscheme with simple normal crossings with a family is regular ("in particular, Z is smooth", [Kol07, Definition 24]); a restatement of AlgebraicGeometry.HasSncWith.isRegular under the name used in this directory.

theorem Hironaka.Sequence.smooth_of_hasSncWith {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {E : X.DivisorFamily} {Z : X.IdealSheafData} (h : E.HasSncWith Z) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)

A closed subscheme with simple normal crossings with a family is smooth over the perfect ground field (regular and smooth agree over a perfect field); a restatement of AlgebraicGeometry.HasSncWith.smooth under the name used in this directory.

theorem Hironaka.Sequence.smooth_disjoinCenter {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [PerfectField k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} (hF : F.IsSnc) {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (hG : ∀ (i : ι), G i ∈ Set.range F.component) (m : ℕ) (hm : meetLocus G (m + 2) = ⊥) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (disjoinCenter G (m + 1)).subschemeι f)

The center of a disjoining step is smooth over k [Kol07, 72].