Simple normal crossings along a set; sub-families

Step 2.1 of [Kol07, 104] ends with the divisor H_{r(s)} + E_{r(s)} having "simple normal crossing along cosupp(I_{r(s)}, m)": the pointwise condition of [Kol07, Definition 24] (IsSncAt) at every point of a set, not on the whole scheme — the transforms of the original components of E may still meet H_{r(s)} badly away from the cosupport. This module holds that predicate (DivisorFamily.IsSncOn) and the sub-family of a family on a subset of its index set (DivisorFamily.subfamily; erase E j of Hironaka.Scheme.Snc.EraseFamily is the case p := (· ≠ j)), which the induction of Hironaka.Resolution.Algebraic.Kol07.SncGlobalSubfamily uses for the exceptional members of the boundary. The global IsSnc is the regularity of the members together with IsSncOn on the whole scheme (isSnc_iff_isSncOn_univ).

Sources: [Kol07, Definition 24]; [Kol07, 104] (Step 2.1); [Kol07, Notation 64 (3)] (the ordered index set).

def AlgebraicGeometry.Scheme.DivisorFamily.IsSncOn {X : Scheme} (E : X.DivisorFamily) (s : Set ↥X) : Prop

The family E has simple normal crossings along the set s — the local coordinates of [Kol07, Definition 24] exist at every point of s (IsSncAt); Kollár's "has simple normal crossing along cosupp(I_{r(s)}, m)", Step 2.1 of [Kol07, 104].

Equations

• E.IsSncOn s = ∀ x ∈ s, ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)), E.IsSncAt x z

noncomputable def AlgebraicGeometry.Scheme.DivisorFamily.subfamily {X : Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) : X.DivisorFamily

The sub-family of E on the indices satisfying p, with the induced order (the boundary is an ordered set of divisors, [Kol07, Notation 64 (3)]). erase E j of Hironaka.Scheme.Snc.EraseFamily is the case p := (· ≠ j).

Equations

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

theorem AlgebraicGeometry.Scheme.DivisorFamily.subfamily_component {X : Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) (a : { a : E.ι // p a }) : (E.subfamily p).component a = E.component ↑a

The members of a sub-family are the members of the family at the selected indices.

theorem AlgebraicGeometry.Scheme.DivisorFamily.IsSnc.isSncOn {X : Scheme} {E : X.DivisorFamily} (hE : E.IsSnc) (s : Set ↥X) : E.IsSncOn s

A simple normal crossing family has simple normal crossings along every set.

theorem AlgebraicGeometry.Scheme.DivisorFamily.isSnc_iff_isSncOn_univ {X : Scheme} (E : X.DivisorFamily) : E.IsSnc ↔ (∀ (i : E.ι), IsRegular (E.component i).subscheme) ∧ E.IsSncOn Set.univ

IsSnc is the regularity of the members together with IsSncOn on the whole scheme ([Kol07, Definition 24 (1)–(3)]): the new predicate is the old one relativised to a set.