Subdivisions along a set, and the order condition along the cosupport

Subdivides F G (Hironaka/Resolution/Algebraic/Kol07/RefineFamily.lean), the relation "at every point the members of F through the point are assigned injectively to members of G with the same stalks", transports the order condition of [Kol07, Definition 66] from G to F (isOrderSeq_of_subdivides), because simple normal crossings with a center [Kol07, Definition 24 (4)] only see the members through a point and their stalks. The restriction to the hypersurface of maximal contact in the proof of Theorem 103 [Kol07, 104, Step 2.2] needs the same transport when the assignment exists only along a set s containing every center: SubdividesOn F G s. Every center of a smooth blow-up sequence of order m lies in cosupp(I, m) (condition (4) of Definition 66, le_ord_of_mem_center), and the cosupport of the weak transform maps into the cosupport (le_ord_of_le_ord_weakTransform), so an assignment along cosupp(I, m) transports stage by stage exactly as a global one does (subdividesOn_totalTransformAlong), and a smooth blow-up sequence of order m for (I, G) is one for (I, F) (isOrderSeq_of_subdividesOn_cosupp).

This is the lemma by which the sequence of Step 2.2, a sequence of order m for (I_r, F_r + H_r) with F_r the exceptional sub-family, is one for the original (I_r, E_r): the transforms of the original members of E are disjoint from the cosupport, so along the cosupport every member of E_r is a member of F_r.

def AlgebraicGeometry.Scheme.DivisorFamily.SubdividesOn {X : Scheme} (F G : X.DivisorFamily) (s : Set ↥X) : Prop

F subdivides G along s (Subdivides restricted to a set): at every point of s, the members of F through the point are assigned injectively to members of G with the same stalks.

Equations

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

theorem AlgebraicGeometry.Scheme.DivisorFamily.SubdividesOn.mono {X : Scheme} {F G : X.DivisorFamily} {s t : Set ↥X} (h : F.SubdividesOn G t) (hst : s ⊆ t) : F.SubdividesOn G s

A subdivision along t is one along every s ⊆ t.

theorem AlgebraicGeometry.Scheme.DivisorFamily.Subdivides.subdividesOn {X : Scheme} {F G : X.DivisorFamily} (h : F.Subdivides G) (s : Set ↥X) : F.SubdividesOn G s

A subdivision everywhere is one along every set.

theorem Hironaka.Sequence.hasSncWith_of_subdividesOn {X : AlgebraicGeometry.Scheme} {F G : X.DivisorFamily} {s : Set ↥X} (h : F.SubdividesOn G s) {Z : X.IdealSheafData} (hZs : ∀ x ∈ Z.support, x ∈ s) (hZ : G.HasSncWith Z) : F.HasSncWith Z

Simple normal crossings with Z pass from G to F when F subdivides G along a set containing V(Z) (hasSncWith_of_subdivides along a set).

theorem Hironaka.Sequence.subdividesOn_totalTransformAlong {X : AlgebraicGeometry.Scheme} {F G : X.DivisorFamily} {s : Set ↥X} (h : F.SubdividesOn G s) {B : AlgebraicGeometry.Scheme} (π : B ⟶ X) {K : B.IdealSheafData} (hK : K.IsInvertible) : (AlgebraicGeometry.Scheme.DivisorFamily.totalTransformAlong π K F).SubdividesOn (AlgebraicGeometry.Scheme.DivisorFamily.totalTransformAlong π K G) (⇑π ⁻¹' s)

A subdivision along s is preserved by the total transform along π with an invertible distinguished divisor, along the preimage of s (subdivides_totalTransformAlong along a set).

theorem Hironaka.Sequence.subdividesOn_totalTransform {X : AlgebraicGeometry.Scheme} {F G : X.DivisorFamily} {s : Set ↥X} (h : F.SubdividesOn G s) (D : X.IdealSheafData) : (F.totalTransform D).SubdividesOn (G.totalTransform D) (⇑D.blowUpπ ⁻¹' s)

A subdivision along s is preserved by the total transform under a blow-up, along the preimage of s (subdivides_totalTransform along a set).

theorem Hironaka.Sequence.isOrderSeq_of_subdividesOn_cosupp {k : Type u} [Field k] [CharZero k] (n : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) {J : X.IdealSheafData} {G F : X.DivisorFamily} {m : ℕ} : F.SubdividesOn G {x : ↥X | ↑m ≤ J.ord x} → S.IsOrderSeq f J G m → S.IsOrderSeq f J F m

A smooth blow-up sequence of order m for (J, G) is one for (J, F) when F subdivides G along cosupp(J, m) ([Kol07, Definition 66]; used in [Kol07, 104, Step 2.2]): every center lies in the cosupport (condition (4) of Definition 66) and the cosupport of the weak transform maps into the cosupport, so the subdivision transports stage by stage (isOrderSeq_of_subdivides along the cosupport).