Functoriality of the disjoining sequence

The loci Z_t are defined from E alone, so for a smooth h : Y → X the disjoining sequence of h^{-1} E is the pull-back of the disjoining sequence of E [Kol07, 72]. The proof is an induction along the steps: the center ∏_{|s| = m} ∑_{i ∈ s} G_i commutes with inverse images because the inverse image ideal sheaf is multiplicative and commutes with sums (disjoinCenter_comap), the pull-back of a cons is the cons of the inverse image center and the pull-back of the tail along the induced morphism of blow-ups (pullback_cons), and strict transforms commute with flat base change along that morphism (strictTransform_comap_of_flat). No empty blow-up has to be deleted: the identity holds on the nose for every flat h (disjoinSeq_comap_of_flat), in particular for smooth h (disjoin_functorial, the functoriality of [Kol07, 34.1]) and for the base-change squares of [Kol07, 34.2], which are flat; the "up to empty blow-ups" of Kollár's parenthetical remark concerns the alternative construction with dim X-fold intersections, and the form with the empty blow-ups deleted is disjoin_functorial_eraseEmpty.

Kollár's first paragraph, "we should not introduce arbitrary choices in the process", is the statement disjoinSeq_of_equiv: the sequence does not depend on the order of the index set.

theorem Hironaka.Sequence.disjoinSeqAux_comap_of_flat {ι : Type u_1} [Fintype ι] (m : ℕ) {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (G : ι → X.IdealSheafData) : (disjoinSeqAux m fun (i : ι) => (G i).comap h) = (disjoinSeqAux m G).pullback h

The disjoining steps of the inverse images are the pull-back of the disjoining steps, on the nose, for flat h [Kol07, 72].

theorem Hironaka.Sequence.disjoinSeq_comap_of_flat {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (E : X.DivisorFamily) : disjoinSeq (E.comap h) = (disjoinSeq E).pullback h

For a flat h : Y ⟶ X the disjoining sequence of h^{-1} E is the pull-back ([Kol07, 30.1]) of the disjoining sequence of E [Kol07, 72], with no empty blow-up to delete.

theorem Hironaka.Sequence.disjoin_functorial {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] (E : X.DivisorFamily) : disjoinSeq (E.comap h) = (disjoinSeq E).pullback h

The disjoining commutes with smooth morphisms [Kol07, 72 and 34.1].

theorem Hironaka.Sequence.disjoin_functorial_eraseEmpty {X Y : AlgebraicGeometry.Scheme} (h : Y ⟶ X) [AlgebraicGeometry.Smooth h] (E : X.DivisorFamily) : (disjoinSeq (E.comap h)).eraseEmpty = ((disjoinSeq E).pullback h).eraseEmpty

The disjoining commutes with smooth morphisms up to the deletion of empty blow-ups, the form of the second clause of [Kol07, 34.1].

theorem Hironaka.Sequence.disjoinCenter_equiv {X : AlgebraicGeometry.Scheme} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [Fintype ι₂] (σ : ι₁ ≃ ι₂) {G₁ : ι₁ → X.IdealSheafData} {G₂ : ι₂ → X.IdealSheafData} (hσ : ∀ (a : ι₁), G₂ (σ a) = G₁ a) (m : ℕ) : disjoinCenter G₂ m = disjoinCenter G₁ m

The center does not depend on the indexing of the members.

theorem Hironaka.Sequence.disjoinSeqAux_equiv {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [Fintype ι₂] (m : ℕ) {X : AlgebraicGeometry.Scheme} (σ : ι₁ ≃ ι₂) {G₁ : ι₁ → X.IdealSheafData} {G₂ : ι₂ → X.IdealSheafData} : (∀ (a : ι₁), G₂ (σ a) = G₁ a) → disjoinSeqAux m G₂ = disjoinSeqAux m G₁

The disjoining steps do not depend on the indexing of the members.

theorem Hironaka.Sequence.disjoinSeq_of_equiv {X : AlgebraicGeometry.Scheme} {E₁ E₂ : X.DivisorFamily} (σ : E₁.ι ≃ E₂.ι) (hσ : ∀ (a : E₁.ι), E₂.component (σ a) = E₁.component a) : disjoinSeq E₂ = disjoinSeq E₁

"We should not introduce arbitrary choices in the process" [Kol07, 72]: the disjoining sequence does not depend on the order of the index set; two families with the same components under a bijection of indices have the same disjoining sequence.