Warning 38 and Example 28.1: why a blow-up sequence functor is given on disconnected schemes

By [Kol07, Warning 38] and [Kol07, Example 28.1] a blow-up sequence functor must be given on disconnected inputs, because the order in which disjoint centers are blown up is data that the connected pieces do not determine: on the two open pieces of Example 28.1 the rule "blow up the smooth curve first" produces local sequences with different first centers on the overlap, so the compatibility (37.1) of the proof of [Kol07, Proposition 37] fails and no sequence on X restricts to both. This module proves the mechanism for an arbitrary covering family and the resulting constraint on the extension of Proposition 37; the concrete model of Example 28.1 (two disjoint cusp models in 𝔸³_k) is computed in HironakaExamples/KollarExample28_1.lean.

• (37.1) is necessary (agreeOnOverlaps_of_exists_pullback_eq): the restrictions of one sequence agree on every overlap, because pullback is functorial (pullback_comp) and the two composites fst ≫ ι i, snd ≫ ι j are the same morphism (pullback.condition).
• Different first centers do not glue (not_agreeOnOverlaps_of_center_ne, not_exists_pullback_eq_of_center_ne): if the members i, j start with centers whose inverse images on the overlap differ, the pulled-back sequences differ already in their first center (cons injectivity), whatever the continuations.
• The constraint (Triple.closedUnderSigma_univ, extendFromAffine_seq_of_isSigmaOf): the class of all triples is closed under finite disjoint unions, and the extension of Proposition 37 takes, on a disjoint union of affine triples, the value the given functor B carries there: "we need to know B for the disconnected affine scheme ∐ᵢ Uᵢ" (the closure of the affine class under disjoint unions and extendFromAffine_restrict).

theorem Hironaka.Sequence.agreeOnOverlaps_of_exists_pullback_eq {X : AlgebraicGeometry.Scheme} {σ : Type u} {W : σ → AlgebraicGeometry.Scheme} (ι : (i : σ) → W i ⟶ X) (S : (i : σ) → (W i).BlowUpSequence) (h : ∃ (S₀ : X.BlowUpSequence), ∀ (i : σ), S₀.pullback (ι i) = S i) : AlgebraicGeometry.Scheme.BlowUpSequence.AgreeOnOverlaps ι S

The restrictions of one blow-up sequence on X to a family of morphisms agree on the overlaps: the compatibility (37.1) of the proof of [Kol07, Proposition 37] is necessary for gluing.

theorem Hironaka.Sequence.not_agreeOnOverlaps_of_center_ne {X : AlgebraicGeometry.Scheme} {σ : Type u} {W : σ → AlgebraicGeometry.Scheme} (ι : (i : σ) → W i ⟶ X) (S : (i : σ) → (W i).BlowUpSequence) {i j : σ} {Dᵢ : (W i).IdealSheafData} {rᵢ : Dᵢ.blowUp.BlowUpSequence} {Dⱼ : (W j).IdealSheafData} {rⱼ : Dⱼ.blowUp.BlowUpSequence} (hi : S i = AlgebraicGeometry.Scheme.BlowUpSequence.cons (W i) Dᵢ rᵢ) (hj : S j = AlgebraicGeometry.Scheme.BlowUpSequence.cons (W j) Dⱼ rⱼ) (hne : Dᵢ.comap (CategoryTheory.Limits.pullback.fst (ι i) (ι j)) ≠ Dⱼ.comap (CategoryTheory.Limits.pullback.snd (ι i) (ι j))) : ¬AlgebraicGeometry.Scheme.BlowUpSequence.AgreeOnOverlaps ι S

Two members of a family whose first centers differ on their overlap do not agree on the overlaps, whatever the continuations (the mechanism of [Kol07, Example 28.1]): the pulled-back cons sequences differ in their first center (cons_inj).

theorem Hironaka.Sequence.not_exists_pullback_eq_of_center_ne {X : AlgebraicGeometry.Scheme} {σ : Type u} {W : σ → AlgebraicGeometry.Scheme} (ι : (i : σ) → W i ⟶ X) (S : (i : σ) → (W i).BlowUpSequence) {i j : σ} {Dᵢ : (W i).IdealSheafData} {rᵢ : Dᵢ.blowUp.BlowUpSequence} {Dⱼ : (W j).IdealSheafData} {rⱼ : Dⱼ.blowUp.BlowUpSequence} (hi : S i = AlgebraicGeometry.Scheme.BlowUpSequence.cons (W i) Dᵢ rᵢ) (hj : S j = AlgebraicGeometry.Scheme.BlowUpSequence.cons (W j) Dⱼ rⱼ) (hne : Dᵢ.comap (CategoryTheory.Limits.pullback.fst (ι i) (ι j)) ≠ Dⱼ.comap (CategoryTheory.Limits.pullback.snd (ι i) (ι j))) : ¬∃ (S₀ : X.BlowUpSequence), ∀ (i : σ), S₀.pullback (ι i) = S i

No blow-up sequence on X restricts to a family two of whose members start with centers that differ on their overlap ([Kol07, Example 28.1 and Warning 38]).

theorem AlgebraicGeometry.Triple.closedUnderSigma_univ {k : Type u} [Field k] : ClosedUnderSigma fun (x : Triple k) => True

The class of all triples is closed under finite disjoint unions.

theorem Hironaka.MarkedTriple.closedUnderSigma_univ {k : Type u} [Field k] : ClosedUnderSigma fun (x : MarkedTriple k) => True

The class of all marked triples is closed under finite disjoint unions.

theorem Hironaka.OrderSeqAssignment.extendFromAffine_seq_of_isSigmaOf {k : Type u} [Field k] [CharZero k] {m : ℕ} (B : OrderSeqAssignment k m AlgebraicGeometry.Triple.IsAffineScheme) (hB : B.CommutesWithSmoothSurjections) {σ : Type u} [Finite σ] [Nonempty σ] (Ts : σ → AlgebraicGeometry.Triple k) (T : AlgebraicGeometry.Triple k) (ι : (i : σ) → (Ts i).X.left ⟶ T.X.left) (h : T.IsSigmaOf Ts ι) (hTs : ∀ (i : σ), (Ts i).IsAffineScheme) : (B.extendFromAffine hB).seq T trivial = B.seq T ⋯

On a disjoint union of affine triples the extension of [Kol07, Proposition 37] is the given functor ("we need to know B for the disconnected affine scheme", [Kol07, Warning 38]): the disjoint union is affine and the extension restricts to B on affine triples (extendFromAffine_restrict).

theorem Hironaka.OrderGeSeqAssignment.extendFromAffine_seq_of_isSigmaOf {k : Type u} [Field k] [CharZero k] (B : OrderGeSeqAssignment k MarkedTriple.IsAffineScheme) (hB : B.CommutesWithSmoothSurjections) {σ : Type u} [Finite σ] [Nonempty σ] (Ts : σ → MarkedTriple k) (T : MarkedTriple k) (ι : (i : σ) → (Ts i).X.left ⟶ T.X.left) (h : T.IsSigmaOf Ts ι) (hTs : ∀ (i : σ), (Ts i).IsAffineScheme) : (B.extendFromAffine hB).seq T trivial = B.seq T ⋯

On a disjoint union of affine marked triples the extension of [Kol07, Proposition 37] is the given functor.