Declaring pairwise disjoint components a single divisor

If the irreducible components of E happen to be disjoint, "we can just declare that E is a single divisor", since Theorem 68 allows the components of E to be reducible [Kol07, 72]. The single divisor is E_1 + ⋯ + E_k, with ideal sheaf ∏_i E_i; at a point x at most one E_i passes, and the stalk of the product is the stalk of that one component (the others contribute the unit ideal), so conditions (1)–(3) of [Kol07, Definition 24] hold for the one-component family with the same coordinates, and the divisor is regular because each E_i is.

The same argument applies to any set of pairwise disjoint components of an snc family F collapsed into one component (DivisorFamily.collapse), which is how Kollár's ordered family E^0 < E^1 < ⋯ < E^{k-1} is assembled: the general statement is isSnc_collapse; the one-component family is asSingle_isSnc.

• mem_support_finset_prod_iff: supports of finite products (the stalks are stalkIdeal_finset_prod, Hironaka/Scheme/IdealSheaf/StalkLe.lean).
• exists_stalkIdeal_prod_eq_of_disjoint: at a point of the union of pairwise disjoint closed subschemes, the stalk of the product is the stalk of the unique member through the point.
• isSncAt_of_stalk_injection: conditions (1)–(3) of Definition 24 transport along a stalk-matching injection of the components through a point.
• isSnc_collapse, asSingle_isSnc: the collapsed families are snc.

theorem Hironaka.Sequence.mem_support_finset_prod_iff {X : AlgebraicGeometry.Scheme} {σ : Type u_1} (S : Finset σ) (J : σ → X.IdealSheafData) (x : ↥X) : x ∈ (∏ s ∈ S, J s).support ↔ ∃ s ∈ S, x ∈ (J s).support

A point lies on a finite product of ideal sheaves iff it lies on one of the factors.

theorem Hironaka.Sequence.exists_stalkIdeal_prod_eq_of_disjoint {X : AlgebraicGeometry.Scheme} {κ : Type u_1} [Fintype κ] {G : κ → X.IdealSheafData} (hdisj : ∀ (x : ↥X) (j j' : κ), x ∈ (G j).support → x ∈ (G j').support → j = j') {x : ↥X} (hx : x ∈ (∏ j : κ, G j).support) : ∃ (j : κ), x ∈ (G j).support ∧ (∏ j : κ, G j).stalkIdeal x = (G j).stalkIdeal x

At a point of the union of pairwise disjoint closed subschemes, the stalk of their product is the stalk of the unique member through the point (the others contribute the unit ideal).

theorem Hironaka.Sequence.isSncAt_of_stalk_injection {X : AlgebraicGeometry.Scheme} {F F' : X.DivisorFamily} {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (h : F.IsSncAt x z) (θ : { i : F'.ι // x ∈ (F'.component i).support } → { a : F.ι // x ∈ (F.component a).support }) (hθ : Function.Injective θ) (hst : ∀ (i : { i : F'.ι // x ∈ (F'.component i).support }), (F'.component ↑i).stalkIdeal x = (F.component ↑(θ i)).stalkIdeal x) : F'.IsSncAt x z

Bookkeeping: Kollár's conditions (1)–(3) at x transport along an injection of the components of F' through x into those of F through x that matches the stalks at x.

theorem Hironaka.Sequence.isRegularLocalRing_quotient_span_singleton_of_isSncAt {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (hrs : IsLocalRing.IsRegularSystemOfParameters z) (j : Fin n) : IsRegularLocalRing (↑(X.presheaf.stalk x) ⧸ Ideal.span {z j})

At a point of a smooth k-scheme, the quotient of the stalk by a coordinate of a regular system of parameters is a regular local ring.

theorem Hironaka.Sequence.collapse_disjoint {X : AlgebraicGeometry.Scheme} {F : X.DivisorFamily} {p : F.ι → Prop} (hp : ∀ (x : ↥X) (a b : F.ι), p a → p b → x ∈ (F.component a).support → x ∈ (F.component b).support → a = b) (x : ↥X) (j j' : { a : F.ι // p a }) (hj : x ∈ (F.component ↑j).support) (hj' : x ∈ (F.component ↑j').support) : j = j'

The members to collapse are pairwise disjoint, as a family over the collapsed indices.

theorem Hironaka.Sequence.collapse_component_bot {X : AlgebraicGeometry.Scheme} {F : X.DivisorFamily} (p : F.ι → Prop) [DecidablePred p] : (F.collapse p).component ⊥ = ∏ a : { a : F.ι // p a }, F.component ↑a

The collapsed component is the product of the collapsed members.

theorem Hironaka.Sequence.collapse_component_coe {X : AlgebraicGeometry.Scheme} {F : X.DivisorFamily} (p : F.ι → Prop) [DecidablePred p] (a : { a : F.ι // ¬p a }) : (F.collapse p).component ↑a = F.component ↑a

The other components are unchanged.

theorem Hironaka.Sequence.isSnc_collapse {X : AlgebraicGeometry.Scheme} {F : X.DivisorFamily} {p : F.ι → Prop} [DecidablePred p] {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (hF : F.IsSnc) (hp : ∀ (x : ↥X) (a b : F.ι), p a → p b → x ∈ (F.component a).support → x ∈ (F.component b).support → a = b) : (F.collapse p).IsSnc

Collapsing a pairwise disjoint set of components of an snc family into one component gives an snc family ("in (68) we allow the components of E to be reducible", [Kol07, 72]).

theorem Hironaka.Sequence.asSingle_component {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : E.asSingle.component PUnit.unit = ∏ i : E.ι, E.component i

The single divisor is E_1 + ⋯ + E_k, with ideal sheaf ∏_i E_i [Kol07, 72].

theorem Hironaka.Sequence.support_asSingle {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : E.asSingle.support = E.support

The single divisor has the support of E.

theorem Hironaka.Sequence.eq_of_mem_support_of_sing_eq_bot {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} (hsing : E.singularLocus = ⊥) {x : ↥X} {i j : E.ι} (hi : x ∈ (E.component i).support) (hj : x ∈ (E.component j).support) : i = j

Pairwise disjoint components: Sing E = ∅ means that no point lies on two components.

theorem Hironaka.Sequence.asSingle_isSnc {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) (hsing : E.singularLocus = ⊥) : E.asSingle.IsSnc

If the components of the snc divisor E are pairwise disjoint, then E declared a single (reducible) divisor is an snc family [Kol07, 72], a legal input for [Kol07, Theorems 68 and 69].