Transport of simple normal crossings along reindexings

[Kol07, Definition 24] at a point (IsSncAt) is a statement about the members THROUGH the point: it transfers along any injection of index sets that matches the members (isSncAt_of_stalk_injection, restated here for a global injection with equal members, isSncAt_of_injective_components), hence to sub-families (isSncOn_subfamily_append_mono) and along the reindexing that the induction of Hironaka.Resolution.Algebraic.Kol07.SncGlobalSubfamily (Step 2.1 of [Kol07, 104]) needs at each blow-up: the members of ((E.totalTransform D).subfamily (extendPred p)).append (strictTransform D H) — the selected members of the total transform, the new exceptional divisor, the birational transform of H — are those of ((E.subfamily p).append H).totalTransform D (stepIdx, component_stepIdx, stepIdx_injective). The base of that induction, a smooth divisor alone, is isSnc_append_empty_of_isSmoothDivisor of Hironaka.Scheme.Snc.RestrictHypersurface read on the empty sub-family (isSncOn_subfamily_false_append).

Sources: [Kol07, Definition 24; Definition 25; 104] (Step 2.1).

theorem Hironaka.Snc.isSncAt_of_injective_components {X : AlgebraicGeometry.Scheme} {F F' : X.DivisorFamily} (θ : F'.ι → F.ι) (hθ : Function.Injective θ) (hcomp : ∀ (i : F'.ι), F'.component i = F.component (θ i)) {x : ↥X} {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (h : F.IsSncAt x z) : F'.IsSncAt x z

Definition 24 at a point transfers along an injection of index sets matching the members.

theorem Hironaka.Snc.isSncOn_of_injective_components {X : AlgebraicGeometry.Scheme} {F F' : X.DivisorFamily} (θ : F'.ι → F.ι) (hθ : Function.Injective θ) (hcomp : ∀ (i : F'.ι), F'.component i = F.component (θ i)) {s : Set ↥X} (h : F.IsSncOn s) : F'.IsSncOn s

Snc along a set transfers along an injection of index sets matching the members.

theorem Hironaka.Snc.isSncOn_subfamily_append_mono {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {p q : E.ι → Prop} (hpq : ∀ (i : E.ι), p i → q i) (H : X.IdealSheafData) {s : Set ↥X} (h : ((E.subfamily q).append H).IsSncOn s) : ((E.subfamily p).append H).IsSncOn s

A sub-family of a family with an appended member: shrinking the selected set keeps snc along a set.

def Hironaka.Snc.extendPred {ι : Type u} (p : ι → Prop) : ι ⊕ₗ PUnit.{u + 1} → Prop

Extend a predicate on the members of E to the members of E.totalTransform D: the new exceptional member is selected.

Equations

• Hironaka.Snc.extendPred p i = Sum.elim p (fun (x : PUnit.{?u.1 + 1}) => True) (ofLex i)

def Hironaka.Snc.stepIdx {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) : { i : E.ι ⊕ₗ PUnit.{u + 1} // extendPred p i } ⊕ₗ PUnit.{u + 1} → ({ a : E.ι // p a } ⊕ₗ PUnit.{u + 1}) ⊕ₗ PUnit.{u + 1}

The reindexing of the induction step of Hironaka.Resolution.Algebraic.Kol07.SncGlobalSubfamily: the members of ((E.totalTransform D).subfamily (extendPred p)).append (strictTransform D H) among those of ((E.subfamily p).append H).totalTransform D.

Equations

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

theorem Hironaka.Snc.component_stepIdx {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) (D H : X.IdealSheafData) (i : (((E.totalTransform D).subfamily (extendPred p)).append (H.strictTransform D)).ι) : (((E.totalTransform D).subfamily (extendPred p)).append (H.strictTransform D)).component i = (((E.subfamily p).append H).totalTransform D).component (stepIdx E p i)

stepIdx matches the members.

def Hironaka.Snc.stepIdxInv {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) : ({ a : E.ι // p a } ⊕ₗ PUnit.{u + 1}) ⊕ₗ PUnit.{u + 1} → { i : E.ι ⊕ₗ PUnit.{u + 1} // extendPred p i } ⊕ₗ PUnit.{u + 1}

The left inverse of stepIdx.

Equations

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

theorem Hironaka.Snc.stepIdxInv_stepIdx {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) (i : { i : E.ι ⊕ₗ PUnit.{u + 1} // extendPred p i } ⊕ₗ PUnit.{u + 1}) : stepIdxInv E p (stepIdx E p i) = i

theorem Hironaka.Snc.stepIdx_injective {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (p : E.ι → Prop) : Function.Injective (stepIdx E p)

stepIdx is injective.

theorem Hironaka.Snc.isSncAt_append_of_subfamily {X : AlgebraicGeometry.Scheme} {E : X.DivisorFamily} {p : E.ι → Prop} {H : X.IdealSheafData} {x : ↥X} (hP : ∀ (i : E.ι), x ∈ (E.component i).support → p i) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk x)} (h : ((E.subfamily p).append H).IsSncAt x z) : (E.append H).IsSncAt x z

Definition 24 at a point for a family with an appended member, from the sub-family of the members selected by p, when every member through the point is selected (the final step of the induction: at a point of the cosupport every member of E_r is exceptional).

theorem Hironaka.Snc.isSncOn_subfamily_false_append {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (s : Set ↥X) : ((E.subfamily fun (x : E.ι) => False).append H).IsSncOn s

isSnc_append_empty_of_isSmoothDivisor of Hironaka.Scheme.Snc.RestrictHypersurface on the empty sub-family: a smooth divisor alone has simple normal crossings along every set.