The componentwise blow-up sequence of a center: definitions

Kollár's smooth centers may be disconnected; clause (i) of Hironaka's Main Theorem II [Hir64, Main Theorem II] asks for irreducible ones. The two are reconciled by blowing up a disjoint union of smooth centers component by component, in a fixed order: the resulting sequence has the same composite (the "silly counterexamples" of [Kol07, Remark 33]: blowing up disjoint Z_1, Z_2 one after the other or at once gives the same result). This module holds the definitions the lemma is about.

• AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters c D: for a list D : Fin c → X.IdealSheafData of centers on X, the sequence that blows up D 0, then the inverse image of D 1 in the blow-up, then the inverse image of D 2 in the second blow-up, and so on: π_{Z_1} ∘ π_{Z_2'} ∘ ⋯ ∘ π_{Z_c'} with Z_k' the preimage of Z_k in the intermediate scheme (for pairwise disjoint Z_k the preimage is isomorphic to Z_k, which is part of the lemma; the definition takes the inverse image for any list).
• AlgebraicGeometry.Scheme.DivisorFamily.nth F: the members of a divisor family listed in the order of its index set, as a Fin (Fintype.card F.ι)-indexed family (Mathlib's monoEquivOfFin).
• AlgebraicGeometry.Scheme.IdealSheafData.componentwiseSeq Z: the componentwise sequence of the closed subscheme V(Z), ofCenters applied to the irreducible components of V(Z) (componentFamily: indexed by the generic points of V(Z), each with its reduced structure, ordered by a well-ordering of the generic points).

The lemmas (Hironaka/Resolution/Algebraic/Kol07/ComponentwiseBlowUp.lean, ComponentwiseTransport.lean, ComponentwiseTransforms.lean) say: for pairwise disjoint centers the composite of ofCenters c D is a blow-up of X along ∏ i, D i (the universal property of the blow-up, [Hau14, Definition 4.4], iterated), canonically isomorphic to (∏ i, D i).blowUp over X; a regular closed subscheme is the product of its (pairwise disjoint) irreducible components; and the conditions of [Kol07, Definition 66] transport from the center to the componentwise sequence.

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters {X : Scheme} (c : ℕ) : (Fin c → X.IdealSheafData) → X.BlowUpSequence

The sequence blowing up the listed centers D 0, D 1, …, D (c-1) one after another, each center D k replaced by its inverse image Z_k' under the composite of the earlier blow-ups: π_{Z_1} ∘ π_{Z_2'} ∘ ⋯ ∘ π_{Z_c'}.

Equations

• One or more equations did not get rendered due to their size.
• AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters 0 x_3 = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝

@[simp]

theorem AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters_zero {X : Scheme} (D : Fin 0 → X.IdealSheafData) : ofCenters 0 D = nil X

@[simp]

theorem AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters_succ {X : Scheme} (c : ℕ) (D : Fin (c + 1) → X.IdealSheafData) : ofCenters (c + 1) D = cons X (D 0) (ofCenters c fun (i : Fin c) => (D i.succ).comap (D 0).blowUpπ)

theorem AlgebraicGeometry.Scheme.BlowUpSequence.length_ofCenters {X : Scheme} (c : ℕ) (D : Fin c → X.IdealSheafData) : (ofCenters c D).length = c

The componentwise sequence of c centers has length c.

theorem AlgebraicGeometry.Scheme.DivisorFamily.prod_orderedComponent {X : Scheme} (F : X.DivisorFamily) : ∏ k : Fin (Fintype.card F.ι), F.nth k = ∏ i : F.ι, F.component i

Listing the members in order does not change their product.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.componentwiseSeq {X : Scheme} (Z : X.IdealSheafData) [Finite ↑Z.support.genericPoints] : X.BlowUpSequence

The componentwise blow-up sequence of the closed subscheme V(Z): the irreducible components of V(Z) (componentFamily, indexed by the generic points of V(Z) with their reduced structures) blown up one after another in the order of the chosen well-ordering of the generic points, each replaced by its inverse image under the earlier blow-ups. Needs finitely many components (Finite Z.support.genericPoints, available as an instance when X is Noetherian).

Equations

• Z.componentwiseSeq = AlgebraicGeometry.Scheme.BlowUpSequence.ofCenters (Fintype.card Z.componentFamily.ι) Z.componentFamily.nth

theorem AlgebraicGeometry.Scheme.IdealSheafData.length_componentwiseSeq {X : Scheme} (Z : X.IdealSheafData) [Finite ↑Z.support.genericPoints] : Z.componentwiseSeq.length = Nat.card ↑Z.support.genericPoints

The componentwise sequence has one blow-up per irreducible component of V(Z).