The disjoining sequence: smooth snc centers and a disjoint end result

The one-step facts of Center.lean and Step.lean are threaded along the steps of disjoinSeqAux m G by induction on m, generalising the ambient scheme X, the snc family F (Kollár's running total transform, totalTransformSeq) and the members G (the transforms of the original components), with the invariant "no (m+1)-fold intersections among the members". At each step the center disjoinCenter G (m+2) has snc with F and is smooth over k (Center.lean), the total transform F.totalTransform Z is snc, the strict transforms of the members are components of it (totalTransform_component_inl), and they have no (m+2)-fold intersections (Step.lean); the induction continues on B_Z X with the smooth structure morphism Z.blowUpπ ≫ f.

• disjoinSeqAux_isSmooth, disjoinSeqAux_hasSncWith: clause (1) of [Kol07, Theorem 35] for the disjoining part, in the forms IsSmooth and (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i).
• isSnc_totalTransformSeq_disjoinSeqAux: the total transform of [Kol07, Definition 25] is snc at every stage.
• meetLocus_strictTransformSeq_disjoinSeqAux: "after (k − 1)-steps we get rid of all pairwise intersections" [Kol07, 72].
• The disjoinSeq forms of all of these.

theorem Hironaka.Sequence.strictTransform_mem_range_totalTransform {ι : Type u_1} {X : AlgebraicGeometry.Scheme} {F : X.DivisorFamily} {G : ι → X.IdealSheafData} (hG : ∀ (i : ι), G i ∈ Set.range F.component) (Z : X.IdealSheafData) (i : ι) : (G i).strictTransform Z ∈ Set.range (F.totalTransform Z).component

The strict transforms of members of F are members of the total transform.

theorem Hironaka.Sequence.meetLocus_component_card_succ {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : meetLocus E.component (Fintype.card E.ι + 1) = ⊥

The invariant at the start: no (k+1)-fold intersections among k components.

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

The total transform of F under a disjoining step is snc.

theorem Hironaka.Sequence.disjoinSeqAux_isSmooth {k : Type u} [Field k] [PerfectField k] {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} : F.IsSnc → ∀ (G : ι → X.IdealSheafData), (∀ (i : ι), G i ∈ Set.range F.component) → meetLocus G (m + 1) = ⊥ → (disjoinSeqAux m G).IsSmooth f

Every center of the disjoining steps is smooth over k [Kol07, 72]; the first half of clause (1) of [Kol07, Theorem 35] for the disjoining part.

theorem Hironaka.Sequence.disjoinSeqAux_hasSncWith {k : Type u} [Field k] [PerfectField k] {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} : F.IsSnc → ∀ (G : ι → X.IdealSheafData), (∀ (i : ι), G i ∈ Set.range F.component) → meetLocus G (m + 1) = ⊥ → ∀ (i : Fin (disjoinSeqAux m G).length), ((disjoinSeqAux m G).totalTransformSeq F i.castSucc).HasSncWith ((disjoinSeqAux m G).center i)

Every center of the disjoining steps has simple normal crossings with the total transform of F at its stage [Kol07, 72]; the second half of clause (1) of [Kol07, Theorem 35] for the disjoining part, with the total transform of [Kol07, Definition 25].

theorem Hironaka.Sequence.isSnc_totalTransformSeq_disjoinSeqAux {k : Type u} [Field k] [PerfectField k] {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} : F.IsSnc → ∀ (G : ι → X.IdealSheafData), (∀ (i : ι), G i ∈ Set.range F.component) → meetLocus G (m + 1) = ⊥ → ∀ (i : Fin ((disjoinSeqAux m G).length + 1)), ((disjoinSeqAux m G).totalTransformSeq F i).IsSnc

The total transform of F ([Kol07, Definition 25]) is snc at every stage of the disjoining steps.

theorem Hironaka.Sequence.meetLocus_strictTransformSeq_disjoinSeqAux {k : Type u} [Field k] [PerfectField k] {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] {F : X.DivisorFamily} : F.IsSnc → ∀ (G : ι → X.IdealSheafData), (∀ (i : ι), G i ∈ Set.range F.component) → meetLocus G (m + 1) = ⊥ → meetLocus (fun (i : ι) => (disjoinSeqAux m G).strictTransformSeq (G i) (Fin.last (disjoinSeqAux m G).length)) 2 = ⊥

"After (k − 1)-steps we get rid of all pairwise intersections as well" [Kol07, 72]: the final strict transforms of the members are pairwise disjoint.

theorem Hironaka.Sequence.disjoinSeq_isSmooth {k : Type u} [Field k] [PerfectField k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) : (disjoinSeq E).IsSmooth f

Every center of the disjoining sequence is smooth over k [Kol07, 72].

theorem Hironaka.Sequence.disjoinSeq_hasSncWith {k : Type u} [Field k] [PerfectField k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) (i : Fin (disjoinSeq E).length) : ((disjoinSeq E).totalTransformSeq E i.castSucc).HasSncWith ((disjoinSeq E).center i)

Every center of the disjoining sequence has simple normal crossings with the total transform of E at its stage [Kol07, 72].

theorem Hironaka.Sequence.isSnc_totalTransformSeq_disjoinSeq {k : Type u} [Field k] [PerfectField k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) (i : Fin ((disjoinSeq E).length + 1)) : ((disjoinSeq E).totalTransformSeq E i).IsSnc

The total transform of E is snc at every stage of the disjoining sequence.

theorem Hironaka.Sequence.meetLocus_strictTransformSeq_disjoinSeq {k : Type u} [Field k] [PerfectField k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] (E : X.DivisorFamily) (hE : E.IsSnc) : meetLocus (fun (a : E.ι) => (disjoinSeq E).strictTransformSeq (E.component a) (Fin.last (disjoinSeq E).length)) 2 = ⊥

The final birational transforms of the components are pairwise disjoint [Kol07, 72].