The vocabulary of the algebraic main theorems

The notions in which the algebraic main theorems are stated: Hironaka's Main Theorems II and II(N) and Corollaries 1 and 3, Kollár's Theorems 35 and 36 and Włodarczyk's embedded desingularization [Wlo05, Theorem 1.0.2]. The functorial theorems assert the existence of a blow-up sequence functor [Kol07, Definition 31] with a property of each value and a functoriality package [Kol07, 34]; they differ in the inputs of the functor and in the property of the values. Hironaka's theorems assert the existence of a single succession of blow-ups with clauses on its centres, weak transforms and boundaries.

Inputs.

• AlgScheme k: algebraic k-schemes (separated and of finite type over Spec k) with the k-morphisms, as Mathlib's MorphismProperty.Over.
• ReducedEquidimensionalScheme k: the full subcategory of the reduced, equidimensional algebraic k-schemes (Scheme.IsReducedEquidimensional), the inputs of Theorem 36.
• Triple k: Kollár's triples (X, I, E) [Kol07, Notation 64], the inputs of Theorem 35; a morphism is a k-morphism along which I and E pull back.
• EmbeddedPair k: a reduced closed subscheme Y of a smooth equidimensional algebraic k-scheme X, the inputs of Włodarczyk's theorem; a morphism is a k-morphism along which Y pulls back.
• HasUnderlyingScheme C k: a category C with a functor to AlgScheme k, the underlying scheme of an input. HasChangeOfFields C: for a family of such categories, one per field, the notion of a base change of an input along a field extension.

Blow-up sequence functors and functoriality.

• BlowUpSequenceFunctor C: a succession of blow-ups of the underlying scheme of every input [Kol07, Definition 31].
• CommutesWithSmoothMorphisms [Kol07, 34.1], CommutesWithChangeOfFields [Kol07, 34.2], and, for triples, CommutesWithClosedEmbeddingsOfEmptyBoundary Kol07, 34.3 with E = ∅.
• For embedded pairs, CommutesWithSmoothMorphismsMeetingComponents [Wlo05, Theorem 1.0.2 (d)].

Properties of a succession of blow-ups.

• BlowUpSequence.HasRegularIrreducibleCenters, BlowUpSequence.HasSncBoundaries and BlowUpSequence.HasConstantPositiveOrderAlongCenters: clauses of Hironaka's Main Theorems II and II(N) and of his Corollary 1.
• Scheme.IsSncDivisor: a closed set is the support of a simple normal crossing divisor.
• BlowUpSequence.IsResolution [Kol07, (2)] and BlowUpSequence.IsStrongResolution [Kol07, (3); Theorem 36 (1)–(3)].
• BlowUpSequence.HasSmoothSncCenters and Triple.IsPrincipalizedBy [Kol07, Theorem 35 (1)–(3)].
• EmbeddedPair.IsDesingularizedBy [Wlo05, Theorem 1.0.2 (a)–(c), (e)].

Algebraic k-schemes

@[reducible, inline]

abbrev AlgebraicGeometry.AlgScheme (k : Type u) [Field k] : Type (u + 1)

The category of algebraic k-schemes, the schemes separated and of finite type over Spec k, with the k-morphisms: Mathlib's MorphismProperty.Over. An object X has the underlying scheme X.left and the structure morphism X.hom : X.left ⟶ Spec k; a morphism h : Y ⟶ X has the underlying morphism of schemes h.left.

Relation to the source.

• Translation. X : AlgScheme k is Hironaka's algebraic $B$-scheme over the field $B = k$, a scheme (separated) of finite type over $\operatorname{Spec} B$ [Hir64, Ch. 0, §1, pp. 118–119].
• Interpretation. Kollár's schemes of finite type over a field and Włodarczyk's varieties are taken separated, as Hironaka's algebraic schemes are.

Equations

• AlgebraicGeometry.AlgScheme k = (@AlgebraicGeometry.FiniteType ⊓ @AlgebraicGeometry.IsSeparated).Over ⊤ (AlgebraicGeometry.Spec ↧k)

@[instance_reducible]

instance AlgebraicGeometry.AlgScheme.over {k : Type u} [Field k] (X : AlgScheme k) : X.left.Over (Spec ↧k)

Equations

• X.over = { hom := X.hom }

instance AlgebraicGeometry.AlgScheme.finiteType {k : Type u} [Field k] (X : AlgScheme k) : FiniteType (X.left ↘ Spec ↧k)

def AlgebraicGeometry.Scheme.IsReducedEquidimensional (k : Type u) [Field k] (X : Scheme) [X.Over (Spec ↧k)] [LocallyOfFiniteType (X ↘ Spec ↧k)] : Prop

X is reduced and equidimensional over k: X is reduced and its smooth locus over k is smooth of a single relative dimension d [Kol07, Notation 64]. Over a perfect field (in the theorems k has characteristic zero) the smooth locus of a reduced scheme of finite type is dense and contains every generic point, so this says that the irreducible components of X all have dimension d; for a smooth X it says that X is smooth of relative dimension d. Over an imperfect field the smooth locus of a reduced scheme can be empty or not dense, and the condition says less.

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.ReducedEquidimensionalScheme (k : Type u) [Field k] : Type (u + 1)

The inputs of Theorem 36: the algebraic k-schemes that are reduced and equidimensional (Scheme.IsReducedEquidimensional: reduced, with smooth locus over k smooth of a single relative dimension), with the k-morphisms. The irreducible components of an input may meet, so the two axes xy = 0 in the plane and every reduced simple normal crossing scheme are inputs. An object X has X.obj : AlgScheme k.

Equations

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

Triples

structure AlgebraicGeometry.Triple (k : Type u) [Field k] : Type (u + 1)

A triple (X, I, E) [Kol07, Notation 64], the input of Theorem 35: X a smooth, equidimensional algebraic k-scheme (smooth of a single relative dimension over k), I an ideal sheaf nonzero at every point (so on every irreducible component), and E a simple normal crossing divisor family with ordered index set.

• X : AlgScheme k

  The smooth ambient scheme.

• smoothOfRelativeDimension : ∃ (n : ℕ), SmoothOfRelativeDimension n (self.X.left ↘ Spec ↧k)

  X is smooth of a single relative dimension over k (smooth and equidimensional).

• I : self.X.left.IdealSheafData

  The ideal sheaf.

• isNonzeroEverywhere : self.I.IsNonzeroEverywhere

  I is nonzero at every point.

• E : self.X.left.DivisorFamily

  The boundary.

• isSnc : self.E.IsSnc

  E is a simple normal crossing family.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Triple.instCategory {k : Type u} [Field k] : CategoryTheory.Category.{u, u + 1} (Triple k)

A morphism of triples (Y, J, F) ⟶ (X, I, E): a k-morphism h : Y ⟶ X with J = h^* I and F = h⁻¹ E, so that the source is the pull-back of the target [Kol07, 34.1].

Equations

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

Embedded pairs

structure AlgebraicGeometry.EmbeddedPair (k : Type u) [Field k] : Type (u + 1)

An embedded pair (X, Y), the input of Włodarczyk's theorem [Wlo05, Theorem 1.0.2]: X a smooth, equidimensional algebraic k-scheme (smooth of a single relative dimension over k) and Y a reduced closed subscheme of X, given by its ideal sheaf.

• X : AlgScheme k

  The smooth ambient scheme.

• smoothOfRelativeDimension : ∃ (n : ℕ), SmoothOfRelativeDimension n (self.X.left ↘ Spec ↧k)

  X is smooth of a single relative dimension over k (smooth and equidimensional).

• Y : self.X.left.IdealSheafData

  The ideal sheaf of the embedded subscheme.

• isReduced : IsReduced self.Y.subscheme

  The embedded subscheme is reduced.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.EmbeddedPair.instCategory {k : Type u} [Field k] : CategoryTheory.Category.{u, u + 1} (EmbeddedPair k)

A morphism of embedded pairs (X', Y') ⟶ (X, Y): a k-morphism h : X' ⟶ X with Y' = h⁻¹(Y), the ideal sheaf of Y' the pull-back of that of Y.

Equations

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

Blow-up sequence functors

class AlgebraicGeometry.HasUnderlyingScheme (C : Type u_1) [CategoryTheory.Category.{u, u_1} C] (k : outParam (Type u)) [Field k] : Type (max (u + 1) u_1)

A category C of inputs with an underlying algebraic k-scheme, given by a functor to AlgScheme k.

• forget : CategoryTheory.Functor C (AlgScheme k)

  The underlying algebraic k-scheme.

@[reducible, inline]

abbrev AlgebraicGeometry.HasUnderlyingScheme.scheme {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {k : Type u} [Field k] [HasUnderlyingScheme C k] (X : C) : Scheme

The underlying scheme of an input.

Equations

• AlgebraicGeometry.HasUnderlyingScheme.scheme X = (AlgebraicGeometry.HasUnderlyingScheme.forget.obj X).left

@[reducible, inline]

abbrev AlgebraicGeometry.HasUnderlyingScheme.hom {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {k : Type u} [Field k] [HasUnderlyingScheme C k] {X Y : C} (h : X ⟶ Y) : scheme X ⟶ scheme Y

The underlying morphism of schemes of a morphism of inputs.

Equations

• AlgebraicGeometry.HasUnderlyingScheme.hom h = (AlgebraicGeometry.HasUnderlyingScheme.forget.map h).left

@[instance_reducible]

noncomputable instance AlgebraicGeometry.ReducedEquidimensionalScheme.hasUnderlyingScheme (k : Type u) [Field k] : HasUnderlyingScheme (ReducedEquidimensionalScheme k) k

Equations

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

@[instance_reducible]

instance AlgebraicGeometry.Triple.hasUnderlyingScheme (k : Type u) [Field k] : HasUnderlyingScheme (Triple k) k

Equations

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

@[instance_reducible]

instance AlgebraicGeometry.EmbeddedPair.hasUnderlyingScheme (k : Type u) [Field k] : HasUnderlyingScheme (EmbeddedPair k) k

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.BlowUpSequenceFunctor (C : Type u_1) [CategoryTheory.Category.{u, u_1} C] {k : Type u} [Field k] [HasUnderlyingScheme C k] : Type (max (u + 1) u_1)

A blow-up sequence functor on the inputs C [Kol07, Definition 31]: a succession of blow-ups of the underlying scheme of every input. Kollár's inputs are triples (X, I, E); for Theorem 36 they are schemes.

Equations

• AlgebraicGeometry.BlowUpSequenceFunctor C = ((X : C) → (AlgebraicGeometry.HasUnderlyingScheme.scheme X).BlowUpSequence)

structure AlgebraicGeometry.CommutesWithSmoothMorphisms {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {k : Type u} [Field k] [HasUnderlyingScheme C k] (B : BlowUpSequenceFunctor C) : Prop

B commutes with smooth morphisms [Kol07, 34.1]: for a morphism of inputs h : Y ⟶ X whose underlying morphism is smooth, B(Y) is the pull-back h^* B(X) if h is surjective, and is obtained from h^* B(X) by deleting every blow-up with empty centre in general. (The first condition follows from the second when B has no empty blow-ups; Kollár states both.)

• eq_pullback_of_surjective ⦃X Y : C⦄ (h : Y ⟶ X) : Smooth (HasUnderlyingScheme.hom h) → Function.Surjective ⇑(HasUnderlyingScheme.hom h) → B Y = (B X).pullback (HasUnderlyingScheme.hom h)

  For smooth surjective h, B(Y) is h^* B(X) (the first condition of 34.1).

• eq_eraseEmpty_pullback ⦃X Y : C⦄ (h : Y ⟶ X) : Smooth (HasUnderlyingScheme.hom h) → B Y = ((B X).pullback (HasUnderlyingScheme.hom h)).eraseEmpty

  For smooth h, B(Y) is h^* B(X) with the empty blow-ups deleted (the second condition).

theorem AlgebraicGeometry.commutesWithSmoothMorphisms_iff {C : Type u_1} [CategoryTheory.Category.{u, u_1} C] {k : Type u} [Field k] [HasUnderlyingScheme C k] (B : BlowUpSequenceFunctor C) : CommutesWithSmoothMorphisms B ↔ (∀ ⦃X Y : C⦄ (h : Y ⟶ X), Smooth (HasUnderlyingScheme.hom h) → Function.Surjective ⇑(HasUnderlyingScheme.hom h) → B Y = (B X).pullback (HasUnderlyingScheme.hom h)) ∧ ∀ ⦃X Y : C⦄ (h : Y ⟶ X), Smooth (HasUnderlyingScheme.hom h) → B Y = ((B X).pullback (HasUnderlyingScheme.hom h)).eraseEmpty

class AlgebraicGeometry.HasChangeOfFields (C : (k : Type u) → [Field k] → Type u_1) [(k : Type u) → [inst : Field k] → CategoryTheory.Category.{u, u_1} (C k)] [(k : Type u) → [inst : Field k] → HasUnderlyingScheme (C k) k] : Type (max (u + 1) u_1)

For a family C of categories of inputs, one for each field, the notion of a base change of an input along a field extension [Kol07, 34.2]: IsFieldBaseChange σ p for inputs X over k and XL over L, a field extension σ : k → L and a morphism p of underlying schemes, says that p exhibits XL as the base change X ×_{Spec k} Spec L together with its extra structure.

• IsFieldBaseChange {k L : Type u} [Field k] [Field L] (σ : k →+* L) {X : C k} {XL : C L} (p : HasUnderlyingScheme.scheme XL ⟶ HasUnderlyingScheme.scheme X) : Prop

  p exhibits XL as the base change of X along σ.

@[instance_reducible]

instance AlgebraicGeometry.ReducedEquidimensionalScheme.hasChangeOfFields : HasChangeOfFields ReducedEquidimensionalScheme

For reduced equidimensional schemes, a base change is a cartesian square over Spec σ.

Equations

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

@[instance_reducible]

instance AlgebraicGeometry.Triple.hasChangeOfFields : HasChangeOfFields Triple

For triples, a base change is a cartesian square over Spec σ along which the ideal sheaf and the boundary pull back.

Equations

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

def AlgebraicGeometry.CommutesWithChangeOfFields {C : (k : Type u) → [Field k] → Type u_1} [(k : Type u) → [inst : Field k] → CategoryTheory.Category.{u, u_1} (C k)] [(k : Type u) → [inst : Field k] → HasUnderlyingScheme (C k) k] [HasChangeOfFields C] (B : (k : Type u) → [inst : Field k] → [CharZero k] → BlowUpSequenceFunctor (C k)) : Prop

A family of blow-up sequence functors, one for each field of characteristic zero, commutes with change of fields [Kol07, 34.2]: for a field extension σ : k → L and an input XL over L exhibited as the base change of an input X over k by p, B_L(XL) is the pull-back p^* B_k(X). The ring map σ may be an automorphism (L = k), so the condition includes invariance under the automorphisms of k, as Kollár's does.

Equations

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

def AlgebraicGeometry.CommutesWithClosedEmbeddingsOfEmptyBoundary {k : Type u} [Field k] (B : BlowUpSequenceFunctor (Triple k)) : Prop

A blow-up sequence functor on triples commutes with closed embeddings when the boundary is empty Kol07, 34.3, for E = ∅: for a closed embedding j : Y ↪ X of smooth schemes and triples (Y, I_Y, ∅) and (X, j_* I_Y, ∅), B(X, j_* I_Y, ∅) is the push-forward j_* B(Y, I_Y, ∅). A boundary is empty when it has no components (its index type is empty), however it is indexed. Kollár states 34.3 for a boundary with simple normal crossings with Y; Theorem 35 (5) asserts it only for E = ∅.

Equations

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

structure AlgebraicGeometry.CommutesWithSmoothMorphismsMeetingComponents {k : Type u} [Field k] (B : BlowUpSequenceFunctor (EmbeddedPair k)) : Prop

A blow-up sequence functor on embedded pairs commutes with smooth morphisms meeting the components [Wlo05, Theorem 1.0.2 (d)]: for a morphism of embedded pairs h : (X', Y') ⟶ (X, Y) whose underlying morphism is smooth, B(X', Y') is the pull-back h^* B(X, Y) if h is surjective, and is obtained from h^* B(X, Y) by deleting every blow-up with empty centre if the image of h meets every irreducible component of Y. Włodarczyk's (d), read through his Definition 2.1.5 (extensions by isomorphisms) and Proposition 2.4.2, asserts the second condition for every smooth h; here it is asserted only when the image meets every component of Y.

• eq_pullback_of_surjective ⦃P Q : EmbeddedPair k⦄ (h : Q ⟶ P) : Smooth (HasUnderlyingScheme.hom h) → Function.Surjective ⇑(HasUnderlyingScheme.hom h) → B Q = (B P).pullback (HasUnderlyingScheme.hom h)

  For smooth surjective h, B(X', Y') is h^* B(X, Y).

• eq_eraseEmpty_pullback ⦃P Q : EmbeddedPair k⦄ (h : Q ⟶ P) : Smooth (HasUnderlyingScheme.hom h) → (∀ Z ∈ irreducibleComponents ↥P.Y.subscheme, (Set.range ⇑(HasUnderlyingScheme.hom h) ∩ ⇑P.Y.subschemeι '' Z).Nonempty) → B Q = ((B P).pullback (HasUnderlyingScheme.hom h)).eraseEmpty

  For smooth h whose image meets every irreducible component of Y, B(X', Y') is h^* B(X, Y) with the empty blow-ups deleted.

theorem AlgebraicGeometry.commutesWithSmoothMorphismsMeetingComponents_iff {k : Type u} [Field k] (B : BlowUpSequenceFunctor (EmbeddedPair k)) : CommutesWithSmoothMorphismsMeetingComponents B ↔ (∀ ⦃P Q : EmbeddedPair k⦄ (h : Q ⟶ P), Smooth (HasUnderlyingScheme.hom h) → Function.Surjective ⇑(HasUnderlyingScheme.hom h) → B Q = (B P).pullback (HasUnderlyingScheme.hom h)) ∧ ∀ ⦃P Q : EmbeddedPair k⦄ (h : Q ⟶ P), Smooth (HasUnderlyingScheme.hom h) → (∀ Z ∈ irreducibleComponents ↥P.Y.subscheme, (Set.range ⇑(HasUnderlyingScheme.hom h) ∩ ⇑P.Y.subschemeι '' Z).Nonempty) → B Q = ((B P).pullback (HasUnderlyingScheme.hom h)).eraseEmpty

Properties of the values

def AlgebraicGeometry.Scheme.IsSncDivisor {X : Scheme} (Z : Set ↥X) : Prop

Z is the support of a simple normal crossing divisor on X [Kol07, Definition 24].

Equations

• AlgebraicGeometry.Scheme.IsSncDivisor Z = ∃ (F : X.DivisorFamily), F.IsSnc ∧ ↑F.support = Z

def AlgebraicGeometry.Scheme.BlowUpSequence.HasRegularIrreducibleCenters {X : Scheme} (S : X.BlowUpSequence) : Prop

Every centre of the succession is non-singular (every local ring is regular) and irreducible Hir64, Main Theorem II (i), Main Theorem II(N) (1); Corollary 1, "non-singular irreducible centers D(i)", p. 143.

Equations

• S.HasRegularIrreducibleCenters = ∀ (i : Fin S.length), AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme

structure AlgebraicGeometry.Scheme.BlowUpSequence.HasSncBoundaries {X : Scheme} (S : X.BlowUpSequence) (E : X.IdealSheafData) : Prop

Starting from E, every boundary E_i has only normal crossings with the centre D_i, and the last boundary E_r has only normal crossings Hir64, Main Theorem II (iii) and the first half of (iv); Main Theorem II(N) (3) and the first half of (4). The boundaries are S.boundarySeq E: E_0 = E and E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)); "has only normal crossings (with)" is Hironaka's Definition 2 (IsSncBoundary, IsSncBoundaryWith).

• isSncBoundaryWith_center (i : Fin S.length) : (S.boundarySeq E i.castSucc).IsSncBoundaryWith (S.center i)

  E_i has only normal crossings with D_i Hir64, Main Theorem II (iii); Main Theorem II(N) (3).

• isSncBoundary_last : (S.boundarySeq E (Fin.last S.length)).IsSncBoundary

  E_r has only normal crossings Hir64, Main Theorem II (iv), Main Theorem II(N) (4), first half.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.hasSncBoundaries_iff {X : Scheme} (S : X.BlowUpSequence) (E : X.IdealSheafData) : S.HasSncBoundaries E ↔ (∀ (i : Fin S.length), (S.boundarySeq E i.castSucc).IsSncBoundaryWith (S.center i)) ∧ (S.boundarySeq E (Fin.last S.length)).IsSncBoundary

def AlgebraicGeometry.Scheme.BlowUpSequence.HasConstantPositiveOrderAlongCenters {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) : Prop

The weak transform of J has a constant positive order along every centre: for every i there is a positive integer c such that the weak transform J_i on the stage X_i has order c at every point of the centre D_i [Hir64, Corollary 1 (1)].

Equations

• S.HasConstantPositiveOrderAlongCenters J = ∀ (i : Fin S.length), ∃ (c : ℕ), 0 < c ∧ ∀ y ∈ (S.center i).support, (S.weakTransformSeq J i.castSucc).ord y = ↑c

structure AlgebraicGeometry.Scheme.BlowUpSequence.IsResolution {k : Type u} [Field k] {X : AlgScheme k} (S : X.left.BlowUpSequence) : Prop

A succession of blow-ups Π : X_r → X is a resolution of X [Kol07, (2)]: X_r is smooth over k, Π is projective (IsProjective, hence proper), and Π is birational, an isomorphism over a dense open subset of X. Reading birationality as an isomorphism over a dense open subset is right for a reduced X, the case of the theorems.

• smooth : Smooth (CategoryTheory.CategoryStruct.comp S.composite X.hom)

  X_r is smooth over k.

• isProjective : IsProjective S.composite

  Π is projective [Kol07, (2)].

• exists_dense_isIso : ∃ (U : X.left.Opens), Dense ↑U ∧ CategoryTheory.IsIso (S.composite ∣_ U)

  Π is an isomorphism over a dense open subset.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.isResolution_iff {k : Type u} [Field k] {X : AlgScheme k} (S : X.left.BlowUpSequence) : S.IsResolution ↔ Smooth (CategoryTheory.CategoryStruct.comp S.composite X.hom) ∧ IsProjective S.composite ∧ ∃ (U : X.left.Opens), Dense ↑U ∧ CategoryTheory.IsIso (S.composite ∣_ U)

structure AlgebraicGeometry.Scheme.BlowUpSequence.IsStrongResolution {k : Type u} [Field k] {X : AlgScheme k} (S : X.left.BlowUpSequence) extends S.IsResolution : Prop

A succession of blow-ups Π : X_r → X is a strong resolution of X [Kol07, (3)], clauses (1)–(3) of Theorem 36: a resolution (smooth over k, projective, birational) that is an isomorphism over the smooth locus X^{ns} of X, and such that Π⁻¹(Sing X), Sing X the complement of the smooth locus, is the support of a simple normal crossing divisor.

• smooth : Smooth (CategoryTheory.CategoryStruct.comp S.composite X.hom)
• isProjective : IsProjective S.composite
• exists_dense_isIso : ∃ (U : X.left.Opens), Dense ↑U ∧ CategoryTheory.IsIso (S.composite ∣_ U)
• isIso_restrict_smoothLocus : CategoryTheory.IsIso (S.composite ∣_ Hom.smoothLocus (X.left ↘ Spec ↧k))

  Π is an isomorphism over X^{ns}.

• isSncDivisor_preimage : IsSncDivisor (⇑S.composite ⁻¹' (↑(Hom.smoothLocus (X.left ↘ Spec ↧k)))ᶜ)

  Π⁻¹(Sing X) is the support of a simple normal crossing divisor.

theorem AlgebraicGeometry.Scheme.BlowUpSequence.isStrongResolution_iff {k : Type u} [Field k] {X : AlgScheme k} (S : X.left.BlowUpSequence) : S.IsStrongResolution ↔ S.IsResolution ∧ CategoryTheory.IsIso (S.composite ∣_ Hom.smoothLocus (X.left ↘ Spec ↧k)) ∧ IsSncDivisor (⇑S.composite ⁻¹' (↑(Hom.smoothLocus (X.left ↘ Spec ↧k)))ᶜ)

def AlgebraicGeometry.Scheme.BlowUpSequence.HasSmoothSncCenters {k : Type u} [Field k] {X : AlgScheme k} (S : X.left.BlowUpSequence) (E : X.left.DivisorFamily) : Prop

Every centre of the succession is smooth over k and has simple normal crossings with the total transform of the divisor family E at its stage [Kol07, Theorem 35 (1)].

Equations

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

structure AlgebraicGeometry.Triple.IsPrincipalizedBy {k : Type u} [Field k] (T : Triple k) (S : T.X.left.BlowUpSequence) : Prop

The triple T = (X, I, E) is principalized by a succession of blow-ups Π : X_r → X [Kol07, Theorem 35 (1)–(3)]: its centres are smooth with simple normal crossings with the total transforms of E, the pull-back Π^* I is the ideal sheaf of a simple normal crossing divisor, and Π is an isomorphism over X ∖ (cosupp I ∪ Sing E). (Kollár prints X ∖ cosupp I; his construction first blows up intersections of components of E, which need not lie in cosupp I.)

• hasSmoothSncCenters : S.HasSmoothSncCenters T.E

  (1) Smooth centres with simple normal crossings with the boundary.

• isIdealOfSncDivisor : (T.I.comap S.composite).IsIdealOfSncDivisor

  (2) Π^* I is the ideal sheaf of a simple normal crossing divisor.

• isIso_restrict : CategoryTheory.IsIso (S.composite ∣_ (T.I.support ⊔ T.E.singularLocus).compl)

  (3) Π is an isomorphism over X ∖ (cosupp I ∪ Sing E).

theorem AlgebraicGeometry.Triple.isPrincipalizedBy_iff {k : Type u} [Field k] (T : Triple k) (S : T.X.left.BlowUpSequence) : T.IsPrincipalizedBy S ↔ S.HasSmoothSncCenters T.E ∧ (T.I.comap S.composite).IsIdealOfSncDivisor ∧ CategoryTheory.IsIso (S.composite ∣_ (T.I.support ⊔ T.E.singularLocus).compl)

structure AlgebraicGeometry.EmbeddedPair.IsDesingularizedBy {k : Type u} [Field k] (P : EmbeddedPair k) (S : P.X.left.BlowUpSequence) : Prop

The embedded pair P = (X, Y) is desingularized by a succession of blow-ups σ : X_r → X [Wlo05, Theorem 1.0.2 (a)–(c), (e)]. With exceptional divisors E_i (the total transforms of the empty divisor family) and strict transforms Y_i of Y: every centre C_i is smooth over k and has simple normal crossings with E_i; every E_i is a simple normal crossing family; no point of C_i ∩ Y_i lies over a point of Reg(Y), the image in X of the smooth locus of Y over k; Ỹ = Y_r is smooth over k and has simple normal crossings with E_r; and σ^*(I_Y) = I_Ỹ · J for the ideal sheaf J of a simple normal crossing divisor supported in E_r.

• hasSmoothSncCenters : S.HasSmoothSncCenters (Scheme.DivisorFamily.empty P.X.left)

  Every centre C_i is smooth over k and has simple normal crossings with E_i [Wlo05, Theorem 1.0.2, the smoothness of the centres and the second half of (a)].

• isSnc_totalTransformSeq (i : Fin (S.length + 1)) : (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) i).IsSnc

  (a) Every E_i, the last included, is a simple normal crossing family.

• stageMap_notMem_smoothLocus (i : Fin S.length) (x : ↥(S.stage i.castSucc)) : x ∈ (S.center i).support → x ∈ (S.strictTransformSeq P.Y i.castSucc).support → (S.stageMap i.castSucc) x ∉ ⇑P.Y.subschemeι '' ↑(Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp P.Y.subschemeι (P.X.left ↘ Spec ↧k)))

  (b) No point of C_i ∩ Y_i lies over a point of Reg(Y), the image in X of the smooth locus of Y → Spec k.

• smooth_strictTransformSeq_last : Smooth (CategoryTheory.CategoryStruct.comp (S.strictTransformSeq P.Y (Fin.last S.length)).subschemeι (CategoryTheory.CategoryStruct.comp S.composite P.X.hom))

  (c) The strict transform Ỹ = Y_r is smooth over k.

• hasSncWith_strictTransformSeq_last : (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) (Fin.last S.length)).HasSncWith (S.strictTransformSeq P.Y (Fin.last S.length))

  (c) Ỹ has simple normal crossings with E_r.

• exists_comap_composite_eq_mul : ∃ (J : (S.stage (Fin.last S.length)).IdealSheafData), J.IsIdealOfSncDivisor ∧ J.support ≤ (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) (Fin.last S.length)).support ∧ P.Y.comap S.composite = S.strictTransformSeq P.Y (Fin.last S.length) * J

  (e) σ^*(I_Y) = I_Ỹ · J for the ideal sheaf J of a simple normal crossing divisor supported in E_r.

theorem AlgebraicGeometry.EmbeddedPair.isDesingularizedBy_iff {k : Type u} [Field k] (P : EmbeddedPair k) (S : P.X.left.BlowUpSequence) : P.IsDesingularizedBy S ↔ S.HasSmoothSncCenters (Scheme.DivisorFamily.empty P.X.left) ∧ (∀ (i : Fin (S.length + 1)), (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) i).IsSnc) ∧ (∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, x ∈ (S.strictTransformSeq P.Y i.castSucc).support → (S.stageMap i.castSucc) x ∉ ⇑P.Y.subschemeι '' ↑(Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp P.Y.subschemeι (P.X.left ↘ Spec ↧k)))) ∧ Smooth (CategoryTheory.CategoryStruct.comp (S.strictTransformSeq P.Y (Fin.last S.length)).subschemeι (CategoryTheory.CategoryStruct.comp S.composite P.X.hom)) ∧ (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) (Fin.last S.length)).HasSncWith (S.strictTransformSeq P.Y (Fin.last S.length)) ∧ ∃ (J : (S.stage (Fin.last S.length)).IdealSheafData), J.IsIdealOfSncDivisor ∧ J.support ≤ (S.totalTransformSeq (Scheme.DivisorFamily.empty P.X.left) (Fin.last S.length)).support ∧ P.Y.comap S.composite = S.strictTransformSeq P.Y (Fin.last S.length) * J