54.15 Embedded resolution to 54.17 Factorization birational…

Section54.15 Embedded resolution #

Section 54.15 of the Stacks Project, Tag 0BI3. 7 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BI4, a lemma

Tag 0BI4 in the Stacks Project.

AlgebraicGeometry.resolveCurve_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveResolution.lean, line 549. References: EGA IV (7.9.1), “more general”.

Stacks Project, Tag 0BI4. For a one-dimensional integral Noetherian scheme Y the following are equivalent: there is an alteration X → Y with X regular; there is a resolution of singularities of Y; there is a finite sequence of blowups in closed points Y_n → … → Y_1 → Y with Y_n regular; and the normalization Y^ν → Y is finite.

theorem resolveCurve_tfae (Y : Scheme.{u}) [IsIntegral Y] [IsNoetherian Y]
    (hYdim : topologicalKrullDim Y = 1) :
    List.TFAE [
      ∃ (X : Scheme.{u}) (f : X ⟶ Y), IsAlteration f ∧ IsRegular X,
      ∃ (X : Scheme.{u}) (f : X ⟶ Y), IsResolution f,
      ∃ (X : Scheme.{u}) (f : X ⟶ Y), PointBlowupChain Y Set.univ X f ∧ IsRegular X,
      IsFinite (Scheme.normalization Y
        finite_irreducibleComponents_isCompactOpen_of_isNoetherian)]

Tag 0BI5, a lemma

Tag 0BI5 in the Stacks Project.

AlgebraicGeometry.exists_pointBlowupChain_chainTransform_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/AmbientCurveResolution.lean, line 257.

Let X be a Noetherian scheme and let Y ⊆ X be an integral closed subscheme of dimension one admitting an alteration by a regular scheme — one of the equivalent conditions of [Stacks, Tag 0BI4]. Then there is a finite chain of blowups of X at closed points along which the strict transform of Y becomes a regular curve.

public theorem exists_pointBlowupChain_chainTransform_isRegular {X : Scheme.{u}}
    [IsNoetherian X] (Y : X.IdealSheafData) [IsIntegral Y.subscheme]
    (hYdim : topologicalKrullDim Y.subscheme = 1)
    (hY : ∃ (Z : Scheme.{u}) (g : Z ⟶ Y.subscheme), IsAlteration g ∧ IsRegular Z) :
    ∃ (W : Scheme.{u}) (f : W ⟶ X) (J : W.IdealSheafData),
      PointBlowupChain X Set.univ W f ∧ ChainTransform Y f J ∧ IsIntegral J.subscheme ∧
        topologicalKrullDim J.subscheme = 1 ∧ IsRegular J.subscheme

Tag 0BI6, an equation

Tag 0BI6 in the Stacks Project.

AlgebraicGeometry.IntersectionMultiplicityContext.intersectionMultiplicity_natCast_eq_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/IntersectionMultiplicity.lean, line 201.

Stacks Project, Tag 0BI6. The intersection multiplicity at p is the length of the local ring of the scheme-theoretic intersection as an 𝒪_{X,p}-module.

theorem intersectionMultiplicity_natCast_eq_length
    (S : IntersectionMultiplicityContext) :
    (S.intersectionMultiplicity : ℕ∞) =
      Module.length (S.X.presheaf.stalk S.p) S.intersectionLocalRing

Tag 0BI7, a lemma

Tag 0BI7 in the Stacks Project.

AlgebraicGeometry.strictTransformToCurve_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveStrictTransform.lean, line 654. The attribute's comment: “part (1)”.

Part (1): a curve regular at the centre is unchanged by strict transform.

public theorem strictTransformToCurve_isIso
    {X : Scheme.{u}} [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [IsIntegral Y.subscheme] (hYdim : topologicalKrullDim Y.subscheme = 1)
    (p : X) (hp : IsClosed ({p} : Set X))
    (yPoint : Y.subscheme) (hyPoint : Y.subschemeι yPoint = p)
    (hregular : IsRegularLocalRing (Y.subscheme.presheaf.stalk yPoint)) :
    IsIso (transformToCurve Y p hp)

AlgebraicGeometry.strictTransform_exceptional_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveStrictTransform.lean, line 726. The attribute's comment: “part (2), unique point”.

Part (2): the strict transform has exactly one point on the exceptional fibre.

public theorem strictTransform_exceptional_unique
    {X : Scheme.{u}} [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [IsIntegral Y.subscheme] (hYdim : topologicalKrullDim Y.subscheme = 1)
    (p : X) (hp : IsClosed ({p} : Set X))
    (yPoint : Y.subscheme) (hyPoint : Y.subschemeι yPoint = p)
    (hregular : IsRegularLocalRing (Y.subscheme.presheaf.stalk yPoint)) :
    ∃! q : (AlgebraicGeometry.blowUp (centerIdeal p hp)),
      q ∈ (transformIdeal Y p hp).support ∧
      q ∈ (AlgebraicGeometry.exceptionalIdeal (centerIdeal p hp)).support

AlgebraicGeometry.strictTransform_exceptional_multiplicity_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveStrictTransform.lean, line 776. The attribute's comment: “part (2), multiplicity”.

Part (2): the exceptional intersection has multiplicity one.

public theorem
    strictTransform_exceptional_multiplicity_one
    {X : Scheme.{u}} [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [IsIntegral Y.subscheme] (hYdim : topologicalKrullDim Y.subscheme = 1)
    (p : X) (hp : IsClosed ({p} : Set X))
    (yPoint : Y.subscheme) (hyPoint : Y.subschemeι yPoint = p)
    (hregular : IsRegularLocalRing (Y.subscheme.presheaf.stalk yPoint))
    (q : (AlgebraicGeometry.blowUp (centerIdeal p hp)))
    (hq : q ∈ ((transformIdeal Y p hp) ⊔
      AlgebraicGeometry.exceptionalIdeal (centerIdeal p hp)).support) :
    intersectionLength (transformIdeal Y p hp)
      (AlgebraicGeometry.exceptionalIdeal (centerIdeal p hp)) q hq = 1

AlgebraicGeometry.strictTransform_intersectionMultiplicity_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveStrictTransform.lean, line 1168. The attribute's comment: “part (3)”.

Part (3): an intersection surviving the blowup has smaller multiplicity.

public theorem
    strictTransform_intersectionMultiplicity_lt
    (S : AlgebraicGeometry.IntersectionMultiplicityContext.{u})
    (yPoint : S.y.subscheme) (hyPoint : S.y.subschemeι yPoint = S.p)
    (hregular : IsRegularLocalRing (S.y.subscheme.presheaf.stalk yPoint))
    (q : (AlgebraicGeometry.blowUp (centerIdeal S.p S.p_isClosed)))
    (hqExceptional : q ∈
      (AlgebraicGeometry.exceptionalIdeal (centerIdeal S.p S.p_isClosed)).support)
    (hq : q ∈ ((transformIdeal S.y S.p S.p_isClosed) ⊔
      (transformIdeal S.z S.p S.p_isClosed)).support) :
    intersectionLength (transformIdeal S.y S.p S.p_isClosed)
      (transformIdeal S.z S.p S.p_isClosed) q hq <
      S.intersectionMultiplicity

Tag 0BI8, a lemma

Tag 0BI8 in the Stacks Project.

AlgebraicGeometry.exists_pointBlowupChain_familyTransform_isRegular_pairwise_disjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CurveFamilyResolution.lean, line 1195.

Stacks Project, Tag 0BI8. Let X be a Noetherian scheme and let Y : Fin n → X.IdealSheafData be pairwise distinct integral closed subschemes of dimension one, each admitting a finite chain of blowups in closed points with regular source — one of the equivalent conditions of [Stacks, Tag 0BI4]. Then there is a finite chain of blowups of X at closed points along which the strict transforms of the Y i become pairwise disjoint regular curves.

public theorem exists_pointBlowupChain_familyTransform_isRegular_pairwise_disjoint
    {X : Scheme.{u}} [IsNoetherian X] {n : ℕ} (Y : Fin n → X.IdealSheafData)
    (hYne : Function.Injective Y) (hYint : ∀ i, IsIntegral (Y i).subscheme)
    (hYdim : ∀ i, topologicalKrullDim (Y i).subscheme = 1)
    (hYres : ∀ i, ∃ (V : Scheme.{u}) (g : V ⟶ (Y i).subscheme),
      PointBlowupChain (Y i).subscheme Set.univ V g ∧ IsRegular V) :
    ∃ (W : Scheme.{u}) (f : W ⟶ X) (J : Fin n → W.IdealSheafData),
      PointBlowupChain X Set.univ W f ∧ FamilyTransform Y f J ∧
        (∀ i, IsIntegral (J i).subscheme ∧ topologicalKrullDim (J i).subscheme = 1 ∧
          IsRegular (J i).subscheme) ∧
        Pairwise fun i j : Fin n => Disjoint (J i).support (J j).support

Tag 0BIB, a lemma

Tag 0BIB in the Stacks Project.

Stacks.ResolutionOfSurfaces.exists_pointBlowupChain_comap_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CartierAfterPointBlowups.lean, line 229. The attribute's comment: “granted the local splitting of Tag 0AGT that the formalized Tag 0AHH consumes”.

Stacks Project, Tag 0BIB. Let X be a regular Noetherian scheme of dimension 2 and let Z ⊆ X be a closed subscheme containing no irreducible component of X — the source's "proper closed subscheme". Then there is a sequence Xₙ → … → X₁ → X of blowups at closed points such that the inverse image Zₙ of Z in Xₙ is an effective Cartier divisor.

The first hypothesis is the local splitting of [Stacks, Tag 0AGT] that the library's form of [Stacks, Tag 0AHH] consumes; it is threaded through unchanged.

public theorem exists_pointBlowupChain_comap_isEffectiveCartierDivisor
    (descent : ∀ (Y : Scheme.{u}) (S : Finset Y) (J : Y.IdealSheafData),
      (∀ y ∈ S, IsClosed ({y} : Set Y)) →
      (∀ y ∈ S, IsRegularLocalRing (Y.presheaf.stalk y)) →
      (∀ y ∈ S, ringKrullDim (Y.presheaf.stalk y) = 2) →
      (J.support : Set Y) ⊆ (S : Set Y) →
      ∀ y ∈ (J.support : Set Y), ∀ hy : IsClosed ({y} : Set Y),
      ∀ M : Y.IdealSheafData, M = Scheme.IdealSheafData.vanishingIdeal ⟨{y}, hy⟩ →
        ∃ (d : ℕ) (S' : Finset (blowUp M)) (J' : (blowUp M).IdealSheafData),
          exceptionalIdeal M ^ d * J' = J.comap (blowUpToBase M) ∧
          (∀ z ∈ S', IsClosed ({z} : Set (blowUp M))) ∧
          (∀ z ∈ S', IsRegularLocalRing ((blowUp M).presheaf.stalk z)) ∧
          (∀ z ∈ S', ringKrullDim ((blowUp M).presheaf.stalk z) = 2) ∧
          (J'.support : Set (blowUp M)) ⊆ (S' : Set (blowUp M)) ∧
          (∀ z ∈ S', (blowUpToBase M).base z ∈ S) ∧
          totalColength J' S' < totalColength J S)
    (X : Scheme.{u}) [IsNoetherian X] (hX : AlgebraicGeometry.IsRegular X)
    (hdim : topologicalKrullDim X = 2) (Z : X.IdealSheafData)
    (hZ : IsNowhereDense (Z.support : Set X)) :
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X), PointBlowupChain X Set.univ Y f ∧
      Stacks.Divisors.IsEffectiveCartierDivisor (Z.comap f)

Stacks.ResolutionOfSurfaces.exists_pointBlowupChain_comap_isEffectiveCartierDivisor_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/CartierInverseImage.lean, line 403. The attribute's comment: “a closed subscheme containing no positive-dimensional irreducible component of a regular quasi-compact scheme of dimension at most two becomes an effective Cartier divisor after finitely many blowups at closed points lying over it”.

Stacks Project, Tag 0BIB. Let X be a regular scheme of dimension (at most) two which is quasi-compact, and let Z ⊆ X be a closed subscheme containing no irreducible component of X of positive dimension: every point in the interior of Z is an isolated closed point of X. Then there is a finite sequence Xₙ → … → X₁ → X of blowups at closed points, each lying over a point of Z, such that the inverse image Zₙ of Z in Xₙ is an effective Cartier divisor.

On a locally Noetherian scheme the condition says exactly that every irreducible component of X contained in Z is a single point; it holds in particular when Z contains no irreducible component of X at all (IsNowhereDense). The isolated points of X inside Z are blown up first, which removes them (isOpenImmersion_blowUpToBase_of_isClopen); what is left of Z then contains no irreducible component, and exists_pointBlowupChain_comap_isEffectiveCartierDivisor_of_isNowhereDense applies.

Both deviations from the literal source are forced. Without quasi-compactness the statement is false: Stacks.ResolutionOfSurfaces.not_forall_isEffectiveCartierDivisor_comap_of_isNowhereDense (countably many copies of 𝔸²_ℚ, Z one closed point in each). "Proper closed subscheme" cannot be read literally as Z ≠ X, even for Noetherian X: Stacks.ResolutionOfSurfaces.not_forall_isEffectiveCartierDivisor_comap_of_ne_bot (X = 𝔸²_ℚ ⊔ 𝔸²_ℚ, Z one copy, a component of dimension two). On an irreducible X the literal reading implies the one used here (isNowhereDense_support_of_ne_bot). Both counterexamples are in the sibling module CartierInverseImageCounterexamples (same directory).

public theorem exists_pointBlowupChain_comap_isEffectiveCartierDivisor_of_isRegular
    (X : Scheme.{u}) [CompactSpace X] (hX : AlgebraicGeometry.IsRegular X)
    (hdim : topologicalKrullDim X ≤ 2) (Z : X.IdealSheafData)
    (hZ : ∀ x ∈ interior (Z.support : Set X), IsClopen ({x} : Set X)) :
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X), PointBlowupChain X (Z.support : Set X) Y f ∧
      Stacks.Divisors.IsEffectiveCartierDivisor (Z.comap f)

Tag 0BIC, a lemma

Tag 0BIC in the Stacks Project.

Stacks.ResolutionOfSurfaces.exists_pointBlowupChain_comap_isStrictNormalCrossings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/NormalCrossingsAfterPointBlowups.lean, line 317. The attribute's comment: “granted four hypotheses: normalPosition, that finitely many blowups at closed points bring the components of an effective Cartier divisor on a regular Noetherian surface into normal position (every component regular, any two meeting in a regular scheme at points whose ambient local ring has dimension two, no three with a common point), which is the intersection-multiplicity iteration in the middle of the source's proof; blowupRegular, the global form of Tag 0AGR, that a blowup at a closed point of a regular Noetherian scheme of dimension two is again regular of dimension two, Tag 0AGR being available only for the spectrum of a regular local ring; resInherited, that the resolution hypothesis on one-dimensional components passes to the components of the inverse image along a chain of blowups at closed points; and descent, the local splitting of Tag 0AGT that Tag 0BIB consumes, passed on unchanged”.

Stacks Project, Tag 0BIC. Let X be a regular Noetherian scheme of dimension two and let Z ⊆ X be a closed subscheme containing no irreducible component of X — the source's "proper closed subscheme" — each of whose one-dimensional irreducible components satisfies the equivalent conditions of [Stacks, Tag 0BI4], in the point-blowup form of clause (3) there. Then there is a sequence Xₙ → … → X₁ → X of blowups at closed points such that the inverse image Zₙ of Z in Xₙ is an effective Cartier divisor whose support carries a strict normal crossings divisor.

Four statements are threaded through as hypotheses rather than discharged. descent is the local splitting of [Stacks, Tag 0AGT] that [Stacks, Tag 0BIB] consumes, passed on unchanged. blowupRegular is the global form of [Stacks, Tag 0AGR], proved only for the spectrum of a regular local ring. resInherited says the resolution hypothesis passes to the components of the inverse image along a chain of blowups at closed points. normalPosition is the intersection-multiplicity iteration in the middle of the source's proof.

public theorem exists_pointBlowupChain_comap_isStrictNormalCrossings
    (descent : ∀ (Y : Scheme.{u}) (S : Finset Y) (J : Y.IdealSheafData),
      (∀ y ∈ S, IsClosed ({y} : Set Y)) →
      (∀ y ∈ S, IsRegularLocalRing (Y.presheaf.stalk y)) →
      (∀ y ∈ S, ringKrullDim (Y.presheaf.stalk y) = 2) →
      (J.support : Set Y) ⊆ (S : Set Y) →
      ∀ y ∈ (J.support : Set Y), ∀ hy : IsClosed ({y} : Set Y),
      ∀ M : Y.IdealSheafData, M = Scheme.IdealSheafData.vanishingIdeal ⟨{y}, hy⟩ →
        ∃ (d : ℕ) (S' : Finset (blowUp M)) (J' : (blowUp M).IdealSheafData),
          exceptionalIdeal M ^ d * J' = J.comap (blowUpToBase M) ∧
          (∀ z ∈ S', IsClosed ({z} : Set (blowUp M))) ∧
          (∀ z ∈ S', IsRegularLocalRing ((blowUp M).presheaf.stalk z)) ∧
          (∀ z ∈ S', ringKrullDim ((blowUp M).presheaf.stalk z) = 2) ∧
          (J'.support : Set (blowUp M)) ⊆ (S' : Set (blowUp M)) ∧
          (∀ z ∈ S', (blowUpToBase M).base z ∈ S) ∧
          totalColength J' S' < totalColength J S)
    (blowupRegular : ∀ Y : Scheme.{u}, IsNoetherian Y → AlgebraicGeometry.IsRegular Y →
      topologicalKrullDim Y = 2 → ∀ (y : Y) (hy : IsClosed ({y} : Set Y)),
        AlgebraicGeometry.IsRegular
            (blowUp (Scheme.IdealSheafData.vanishingIdeal (⟨{y}, hy⟩ : Closeds Y))) ∧
          topologicalKrullDim
            (blowUp (Scheme.IdealSheafData.vanishingIdeal (⟨{y}, hy⟩ : Closeds Y))) = 2)
    (resInherited : ∀ (Y V : Scheme.{u}) (f : V ⟶ Y), PointBlowupChain Y Set.univ V f →
      ∀ E : Y.IdealSheafData,
      (∀ C : irreducibleComponents E.subscheme,
        topologicalKrullDim (componentIdeal E C).subscheme = 1 →
        ∃ (P : Scheme.{u}) (g : P ⟶ (componentIdeal E C).subscheme),
          PointBlowupChain (componentIdeal E C).subscheme Set.univ P g ∧
            AlgebraicGeometry.IsRegular P) →
      ∀ C : irreducibleComponents (E.comap f).subscheme,
        topologicalKrullDim (componentIdeal (E.comap f) C).subscheme = 1 →
        ∃ (P : Scheme.{u}) (g : P ⟶ (componentIdeal (E.comap f) C).subscheme),
          PointBlowupChain (componentIdeal (E.comap f) C).subscheme Set.univ P g ∧
            AlgebraicGeometry.IsRegular P)
    (normalPosition : ∀ Y : Scheme.{u}, IsNoetherian Y → AlgebraicGeometry.IsRegular Y →
      topologicalKrullDim Y = 2 → ∀ E : Y.IdealSheafData, IsEffectiveCartierDivisor E →
      (∀ C : irreducibleComponents E.subscheme,
        topologicalKrullDim (componentIdeal E C).subscheme = 1 →
        ∃ (P : Scheme.{u}) (g : P ⟶ (componentIdeal E C).subscheme),
          PointBlowupChain (componentIdeal E C).subscheme Set.univ P g ∧
            AlgebraicGeometry.IsRegular P) →
      ∃ (V : Scheme.{u}) (f : V ⟶ Y), PointBlowupChain Y Set.univ V f ∧
        IsEffectiveCartierDivisor
            (Scheme.IdealSheafData.vanishingIdeal (E.comap f).support) ∧
          ComponentsInNormalPosition
            (Scheme.IdealSheafData.vanishingIdeal (E.comap f).support))
    (X : Scheme.{u}) [IsNoetherian X] (hX : AlgebraicGeometry.IsRegular X)
    (hdim : topologicalKrullDim X = 2) (Z : X.IdealSheafData)
    (hZ : IsNowhereDense (Z.support : Set X))
    (hres : ∀ C : irreducibleComponents Z.subscheme,
      topologicalKrullDim (componentIdeal Z C).subscheme = 1 →
      ∃ (P : Scheme.{u}) (g : P ⟶ (componentIdeal Z C).subscheme),
        PointBlowupChain (componentIdeal Z C).subscheme Set.univ P g ∧
          AlgebraicGeometry.IsRegular P) :
    ∃ (W : Scheme.{u}) (f : W ⟶ X), PointBlowupChain X Set.univ W f ∧
      IsEffectiveCartierDivisor (Z.comap f) ∧
      ∃ (hW : IsLocallyNoetherian W) (D : W.IdealSheafData),
        @IsStrictNormalCrossingsDivisor W hW D ∧
          ((Z.comap f).support : Set W) = (D.support : Set W)

Stacks.ResolutionOfSurfaces.exists_pointBlowupChain_comap_support_eq_isStrictNormalCrossings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/EmbeddedResolution/NormalCrossingsResolution.lean, line 152.

Stacks Project, Tag 0BIC. Let X be a regular Noetherian scheme of dimension two and let Z ⊆ X be a closed subscheme containing no irreducible component of X — the source's "proper closed subscheme" — each of whose one-dimensional irreducible components satisfies the equivalent conditions of [Stacks, Tag 0BI4], in the point-blowup form of clause (3) there. Then there is a sequence Xₙ → … → X₁ → X of blowups at closed points such that the inverse image Zₙ of Z in Xₙ is an effective Cartier divisor whose support is the support of a strict normal crossings divisor.

public theorem exists_pointBlowupChain_comap_support_eq_isStrictNormalCrossings
    (X : Scheme.{u}) [IsNoetherian X] (hX : AlgebraicGeometry.IsRegular X)
    (hdim : topologicalKrullDim X = 2) (Z : X.IdealSheafData)
    (hZ : IsNowhereDense (Z.support : Set X))
    (hres : ∀ C : irreducibleComponents Z.subscheme,
      topologicalKrullDim (componentIdeal Z C).subscheme = 1 →
      ∃ (P : Scheme.{u}) (g : P ⟶ (componentIdeal Z C).subscheme),
        PointBlowupChain (componentIdeal Z C).subscheme Set.univ P g ∧
          AlgebraicGeometry.IsRegular P) :
    ∃ (W : Scheme.{u}) (f : W ⟶ X), PointBlowupChain X Set.univ W f ∧
      IsEffectiveCartierDivisor (Z.comap f) ∧
      ∃ (hW : IsLocallyNoetherian W) (D : W.IdealSheafData),
        @IsStrictNormalCrossingsDivisor W hW D ∧
          ((Z.comap f).support : Set W) = (D.support : Set W)

Sources

LeanAlgebraicGeometry.resolveCurve_tfae · AlgebraicGeometry.exists_pointBlowupChain_chainTransform_isRegular · AlgebraicGeometry.IntersectionMultiplicityContext.intersectionMultiplicity_natCast_eq_length · AlgebraicGeometry.strictTransformToCurve_isIso · AlgebraicGeometry.strictTransform_exceptional_unique · AlgebraicGeometry.strictTransform_exceptional_multiplicity_one · AlgebraicGeometry.strictTransform_intersectionMultiplicity_lt · AlgebraicGeometry.exists_pointBlowupChain_familyTransform_isRegular_pairwise_disjoint

Section54.16 Contracting exceptional curves #

Section 54.16 of the Stacks Project, Tag 0C2I. 12 tags here are carried by 48 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0C2I, the section

Tag 0C2I in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.ExistsContraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ExceptionalCurvesFirstKind.lean, line 75. The attribute's comment: “there exists a contraction of E: a morphism X ⟶ X' to a Noetherian scheme carrying E to a closed point x with O_{X',x} regular of dimension 2 and exhibiting X as the blowing up of X' at x”. References: SGA 7 X (1.14), “partial”.

There exists a contraction of E (Section 0C2I): for the closed subscheme E of X cut out by the ideal sheaf D, there is a morphism X ⟶ X' carrying E to a closed point x of a Noetherian scheme X' with 𝒪_{X',x} regular of dimension two, which exhibits X as the blowing up of X' at x.

def Scheme.IdealSheafData.ExistsContraction {X : Scheme.{u}} (D : X.IdealSheafData) : Prop

Declarations registered for the tag:

AlgebraicGeometry.Scheme.IdealSheafData.IsExceptionalCurveOfFirstKind, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ExceptionalCurvesFirstKind.lean, line 60 (StacksFrontier): “an exceptional curve of the first kind: an effective Cartier divisor E with an isomorphism 𝐏¹_k ≅ E under which the normal sheaf of E pulls back to 𝒪(-1)”.
Stacks.Blowup.exists_isExceptionalCurveOfFirstKind_exceptionalIdeal_vanishingIdeal, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ExceptionalCurvesFirstKind.lean, line 64 (StacksFrontier): “the exceptional fibre E of the blowing up of X' at a closed point x with O_{X',x} regular of dimension 2 is an exceptional curve of the first kind (from Tag 0AGQ)”.

Tag 0C5J, a lemma

Tag 0C5J in the Stacks Project.

AlgebraicGeometry.existsUnique_comp_eq_of_isContractionOfExceptionalCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ContractExceptionalCurve.lean, line 320. The attribute's comment: “unique factorization through the contraction”.

Stacks Project, Tag 0C5J. Let E ⊆ X be an exceptional curve of the first kind on a Noetherian scheme, given by its ideal sheaf D, and let b : X ⟶ X' be a contraction of E. Then every morphism φ : X ⟶ Y carrying E to a single point factors as φ = b ≫ ψ for a unique ψ : X' ⟶ Y.

public theorem existsUnique_comp_eq_of_isContractionOfExceptionalCurve
    {X X' Y : Scheme.{u}} (D : X.IdealSheafData) (b : X ⟶ X')
    (hb : IsContractionOfExceptionalCurve D b) (φ : X ⟶ Y)
    (hφ : ∃ y : Y, ∀ z : D.subscheme, φ (D.subschemeι z) = y) :
    ∃! ψ : X' ⟶ Y, b ≫ ψ = φ

Tag 0C5K, a lemma

Tag 0C5K in the Stacks Project.

AlgebraicGeometry.existsUnique_iso_of_isContractionOfExceptionalCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ContractExceptionalCurve.lean, line 353. The attribute's comment: “a contraction is unique up to unique isomorphism”.

Stacks Project, Tag 0C5K. A contraction of an exceptional curve of the first kind is unique up to unique isomorphism: if b₁ : X ⟶ X₁ and b₂ : X ⟶ X₂ both contract the ideal sheaf D, there is exactly one isomorphism X₁ ≅ X₂ compatible with them.

public theorem existsUnique_iso_of_isContractionOfExceptionalCurve {X X₁ X₂ : Scheme.{u}}
    {D : X.IdealSheafData} {b₁ : X ⟶ X₁} {b₂ : X ⟶ X₂}
    (h₁ : IsContractionOfExceptionalCurve D b₁) (h₂ : IsContractionOfExceptionalCurve D b₂) :
    ∃! e : X₁ ≅ X₂, b₁ ≫ e.hom = b₂

Tag 0C2K, a lemma

Tag 0C2K in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.isNoetherianCompleteLocalRing_formalNeighborhoodRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhood.lean, line 145. The attribute's comment: “the complete Noetherian local clause, granting the five geometric inputs as ExceptionalMonomialData”.

For an exceptional curve of the first kind on a Noetherian scheme, given the five inputs M : ExceptionalMonomialData D, the ring of compatible global functions on the infinitesimal thickenings is a Noetherian complete local ring.

public theorem isNoetherianCompleteLocalRing_formalNeighborhoodRing [IsNoetherian X]
    (_hE : IsExceptionalCurveOfFirstKind D k e) (M : ExceptionalMonomialData D) :
    IsNoetherianCompleteLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.isRegularLocalRing_formalNeighborhoodRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhood.lean, line 155. The attribute's comment: “the regularity clause, granting the five geometric inputs as ExceptionalMonomialData”.

For an exceptional curve of the first kind on a Noetherian scheme, given the five inputs M : ExceptionalMonomialData D, the ring of compatible global functions on the infinitesimal thickenings is a regular local ring.

public theorem isRegularLocalRing_formalNeighborhoodRing [IsNoetherian X]
    (_hE : IsExceptionalCurveOfFirstKind D k e) (M : ExceptionalMonomialData D) :
    IsRegularLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.ringKrullDim_formalNeighborhoodRing_eq_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhood.lean, line 165. The attribute's comment: “the dimension clause, granting the five geometric inputs as ExceptionalMonomialData”.

For an exceptional curve of the first kind on a Noetherian scheme, given the five inputs M : ExceptionalMonomialData D, the ring of compatible global functions on the infinitesimal thickenings has Krull dimension 2.

public theorem ringKrullDim_formalNeighborhoodRing_eq_two [IsNoetherian X]
    (_hE : IsExceptionalCurveOfFirstKind D k e) (M : ExceptionalMonomialData D) :
    ringKrullDim (formalNeighborhoodRing D) = 2

AlgebraicGeometry.Scheme.IdealSheafData.ker_formalNeighborhoodProjection_eq_maximalIdeal_pow_of_isExceptionalCurveOfFirstKind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhood.lean, line 176. The attribute's comment: “the projection-kernel clause, granting the five geometric inputs as ExceptionalMonomialData”.

For an exceptional curve of the first kind on a Noetherian scheme, given the five inputs M : ExceptionalMonomialData D, the kernel of the projection from the ring of compatible global functions to the (n + 1)-st thickening is the (n + 1)-st power of its maximal ideal.

public theorem ker_formalNeighborhoodProjection_eq_maximalIdeal_pow_of_isExceptionalCurveOfFirstKind
    [IsNoetherian X] (_hE : IsExceptionalCurveOfFirstKind D k e)
    (M : ExceptionalMonomialData D) (n : ℕ) :
    letI : IsLocalRing (formalNeighborhoodRing D) := M.monomialFiltration.isLocalRing
    RingHom.ker (formalNeighborhoodProjection D n) =
      IsLocalRing.maximalIdeal (formalNeighborhoodRing D) ^ (n + 1)

AlgebraicGeometry.Scheme.IdealSheafData.isNoetherianCompleteLocalRing_formalNeighborhoodRing_of_isExceptionalCurveOfFirstKind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhoodUnconditional.lean, line 261. The attribute's comment: “the complete Noetherian local clause”.

Stacks 0C2K, the complete Noetherian local clause. For an exceptional curve of the first kind on a Noetherian scheme, the ring lim H⁰(Eₙ, 𝒪ₙ) of compatible functions on the infinitesimal thickenings is a Noetherian complete local ring.

public theorem isNoetherianCompleteLocalRing_formalNeighborhoodRing_of_isExceptionalCurveOfFirstKind
    [IsNoetherian X] (hE : D.IsExceptionalCurveOfFirstKind k e) :
    IsNoetherianCompleteLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.isRegularLocalRing_formalNeighborhoodRing_of_isExceptionalCurveOfFirstKind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhoodUnconditional.lean, line 269. The attribute's comment: “the regularity clause”.

Stacks 0C2K, the regularity clause. For an exceptional curve of the first kind on a Noetherian scheme, the ring of compatible functions on the thickenings is a regular local ring.

public theorem isRegularLocalRing_formalNeighborhoodRing_of_isExceptionalCurveOfFirstKind
    [IsNoetherian X] (hE : D.IsExceptionalCurveOfFirstKind k e) :
    IsRegularLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.ringKrullDim_formalNeighborhoodRing_eq_two_of_isExceptionalCurveOfFirstKind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhoodUnconditional.lean, line 277. The attribute's comment: “the dimension clause”.

Stacks 0C2K, the dimension clause. For an exceptional curve of the first kind on a Noetherian scheme, the ring of compatible functions on the thickenings has dimension 2.

public theorem ringKrullDim_formalNeighborhoodRing_eq_two_of_isExceptionalCurveOfFirstKind
    [IsNoetherian X] (hE : D.IsExceptionalCurveOfFirstKind k e) :
    ringKrullDim (formalNeighborhoodRing D) = 2

AlgebraicGeometry.Scheme.IdealSheafData.IsExceptionalCurveOfFirstKind.ker_formalNeighborhoodProjection_eq_maximalIdeal_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveFormalNeighborhoodUnconditional.lean, line 288. The attribute's comment: “the kernel clause: the kernel of the projection to E_{n+1} is the (n+1)-st power of the maximal ideal”.

Stacks 0C2K, the kernel clause. For an exceptional curve of the first kind on a Noetherian scheme, the kernel of the projection of the ring of compatible functions to H⁰(Eₙ₊₁, 𝒪) is the (n + 1)-st power of the maximal ideal, for the local ring structure that comes with the regularity clause.

public theorem IsExceptionalCurveOfFirstKind.ker_formalNeighborhoodProjection_eq_maximalIdeal_pow
    [IsNoetherian X] (hE : D.IsExceptionalCurveOfFirstKind k e) (n : ℕ) :
    letI : IsLocalRing (formalNeighborhoodRing D) :=
      (isRegularLocalRing_formalNeighborhoodRing_of_isExceptionalCurveOfFirstKind hE).toIsLocalRing
    RingHom.ker (formalNeighborhoodProjection D n) =
      IsLocalRing.maximalIdeal (formalNeighborhoodRing D) ^ (n + 1)

AlgebraicGeometry.Scheme.IdealSheafData.isNoetherianCompleteLocalRing_formalNeighborhoodRing_of_monomialData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveMonomialData.lean, line 219. The attribute's comment: “the complete Noetherian local clause, unconditionally”.

Stacks 0C2K, the complete Noetherian local clause. For an exceptional curve of the first kind on a Noetherian scheme, the ring of compatible global functions on the infinitesimal thickenings is a Noetherian complete local ring.

public theorem isNoetherianCompleteLocalRing_formalNeighborhoodRing_of_monomialData [IsNoetherian X]
    (hE : IsExceptionalCurveOfFirstKind D k e) :
    IsNoetherianCompleteLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.isRegularLocalRing_formalNeighborhoodRing_of_monomialData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveMonomialData.lean, line 227. The attribute's comment: “the regularity clause, unconditionally”.

Stacks 0C2K, the regularity clause.

public theorem isRegularLocalRing_formalNeighborhoodRing_of_monomialData [IsNoetherian X]
    (hE : IsExceptionalCurveOfFirstKind D k e) :
    IsRegularLocalRing (formalNeighborhoodRing D)

AlgebraicGeometry.Scheme.IdealSheafData.ringKrullDim_formalNeighborhoodRing_eq_two_of_monomialData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveMonomialData.lean, line 235. The attribute's comment: “the dimension clause, unconditionally”.

Stacks 0C2K, the dimension clause.

public theorem ringKrullDim_formalNeighborhoodRing_eq_two_of_monomialData [IsNoetherian X]
    (hE : IsExceptionalCurveOfFirstKind D k e) :
    ringKrullDim (formalNeighborhoodRing D) = 2

AlgebraicGeometry.Scheme.IdealSheafData.ker_formalNeighborhoodProjection_eq_maximalIdeal_pow_of_monomialData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveMonomialData.lean, line 244. The attribute's comment: “the projection-kernel clause, unconditionally”.

Stacks 0C2K, the projection-kernel clause. The kernel of the projection to the (n + 1)-st thickening is the (n + 1)-st power of the maximal ideal.

public theorem ker_formalNeighborhoodProjection_eq_maximalIdeal_pow_of_monomialData
    [IsNoetherian X] (hE : IsExceptionalCurveOfFirstKind D k e) (n : ℕ) :
    letI : IsLocalRing (formalNeighborhoodRing D) :=
      (ExceptionalMonomialData.ofIsExceptionalCurveOfFirstKind k hE).monomialFiltration.isLocalRing
    RingHom.ker (formalNeighborhoodProjection D n) =
      IsLocalRing.maximalIdeal (formalNeighborhoodRing D) ^ (n + 1)

Tag 0C2L, a lemma

Tag 0C2L in the Stacks Project.

AlgebraicGeometry.exists_isContractionOfExceptionalCurve_isSteinFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/Contraction/ExistsContraction.lean, line 91.

Stacks Project, Tag 0C2L. Let X be a Noetherian scheme and E ⊆ X an exceptional curve of the first kind, cut out by D and presented as 𝐏¹_k by e. Let f : X ⟶ Y be a morphism such that Y is Noetherian, f is proper, f maps E to a point y of Y, and f is quasi-finite at every point not in E. Then there exists a contraction b : X ⟶ Z of E, and it is the Stein factorization of f: f = b ≫ π with 𝒪_Z ⟶ b_* 𝒪_X an isomorphism and π integral, which characterises the Stein factorization ([Stacks, Tag 03H0]).

public theorem exists_isContractionOfExceptionalCurve_isSteinFactorization
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y] {D : X.IdealSheafData} {k : Type u}
    [Field k] {e : projectiveLineProj k ≅ D.subscheme} (hE : D.IsExceptionalCurveOfFirstKind k e)
    (f : X ⟶ Y) [IsProper f] (y : Y)
    (hmaps : ∀ z : D.subscheme, f.base (D.subschemeι.base z) = y)
    (hqf : ∀ x ∉ (D.support : Set X), quasiFiniteAt f x) :
    ∃ (Z : Scheme.{u}) (b : X ⟶ Z) (π : Z ⟶ Y), b ≫ π = f ∧ IsIso b.c ∧ IsIntegralHom π ∧
      IsContractionOfExceptionalCurve D b

Tag 0C5L, a lemma

Tag 0C5L in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.contractionPicardExactness_of_isContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 306. The attribute's comment: “exactness at Pic(X), the inclusion of the kernel of the degree in the image of b^*, for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction”.

Let b : X ⟶ X' contract the exceptional curve of the first kind cut out by D, presented as 𝐏¹_k by e. Then every Picard class of X of degree zero on the exceptional curve is pulled back along b.

public theorem contractionPicardExactness_of_isContraction
    (hb : IsContractionOfExceptionalCurve D b) :
    D.ContractionPicardExactness k e b

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalRestrictionHom_negativeExceptionalMultiple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicard.lean, line 158. The attribute's comment: “the splitting map n ↦ O_X(-nE), stated through Pic(P¹_k) rather than Z: the restriction of O_X(-nE) to the exceptional curve is O(n)”.

The restriction of 𝒪_X(-nE) to the exceptional curve is 𝒪(n), written as the (-n)-th multiple of the class of 𝒪(-1) in Pic(𝐏¹_k).

public theorem exceptionalRestrictionHom_negativeExceptionalMultiple
    (hE : D.IsExceptionalCurveOfFirstKind k e) (n : ℤ) :
    exceptionalRestrictionHom D k e (negativeExceptionalMultipleHom D n) =
      (-n) • Stacks.SheafOfModules.picardClass (projectiveLineProj k).presheaf
        (structureIsSheaf (projectiveLineProj k).toRingedSpace)
        (ProjectiveSpectrum.Proj.twistingSheaf
          (MvPolynomial.homogeneousSubmodule (Fin 2) k) (-1))
        (isInvertible_twistingSheaf_projectiveLine k (-1))

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegreeHom_negativeExceptionalMultiple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicard.lean, line 185. The attribute's comment: “the splitting: the degree of O_X(-nE) on the exceptional curve is n. The identification Z ≃+ Pic(P¹_k) of Tag 0BXJ is an explicit hypothesis, the library having only the injectivity half of that tag”.

If φ : ℤ ≃+ Pic(𝐏¹_k) carries -1 to the class of 𝒪(-1), then the degree of 𝒪_X(-nE) on the exceptional curve is n.

public theorem exceptionalDegreeHom_negativeExceptionalMultiple
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = Stacks.SheafOfModules.picardClass (projectiveLineProj k).presheaf
      (structureIsSheaf (projectiveLineProj k).toRingedSpace)
      (ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) (-1))
      (isInvertible_twistingSheaf_projectiveLine k (-1)))
    (n : ℤ) :
    exceptionalDegreeHom D k e φ (negativeExceptionalMultipleHom D n) = n

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegreeHom_picardClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicard.lean, line 207. The attribute's comment: “the normalization of the degree map: O_X(E) has degree -1 on the exceptional curve. The identification Z ≃+ Pic(P¹_k) of Tag 0BXJ is an explicit hypothesis, the library having only the injectivity half of that tag”.

If φ : ℤ ≃+ Pic(𝐏¹_k) carries -1 to the class of 𝒪(-1), then the degree of 𝒪_X(E) on the exceptional curve is -1.

public theorem exceptionalDegreeHom_picardClass
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = Stacks.SheafOfModules.picardClass (projectiveLineProj k).presheaf
      (structureIsSheaf (projectiveLineProj k).toRingedSpace)
      (ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) (-1))
      (isInvertible_twistingSheaf_projectiveLine k (-1))) :
    exceptionalDegreeHom D k e φ (Stacks.Divisors.picardClass D) = -1

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegreeHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicard.lean, line 225. The attribute's comment: “right exactness: the degree map Pic(X) ⟶ Z on the exceptional curve is surjective, witnessed by the splitting n ↦ O_X(-nE). The identification Z ≃+ Pic(P¹_k) of Tag 0BXJ is an explicit hypothesis, the library having only the injectivity half of that tag”.

If φ : ℤ ≃+ Pic(𝐏¹_k) carries -1 to the class of 𝒪(-1), then the degree map on the exceptional curve is surjective onto ℤ.

public theorem exceptionalDegreeHom_surjective
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = Stacks.SheafOfModules.picardClass (projectiveLineProj k).presheaf
      (structureIsSheaf (projectiveLineProj k).toRingedSpace)
      (ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) (-1))
      (isInvertible_twistingSheaf_projectiveLine k (-1))) :
    Function.Surjective (exceptionalDegreeHom D k e φ)

AlgebraicGeometry.Scheme.IdealSheafData.negativeExceptionalMultipleHom_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicard.lean, line 241. The attribute's comment: “the splitting n ↦ O_X(-nE) is injective, so Z is a direct summand of Pic(X). The identification Z ≃+ Pic(P¹_k) of Tag 0BXJ is an explicit hypothesis, the library having only the injectivity half of that tag”.

If φ : ℤ ≃+ Pic(𝐏¹_k) carries -1 to the class of 𝒪(-1), then n ↦ [𝒪_X(-nE)] is injective, so ℤ is a direct summand of Pic(X).

public theorem negativeExceptionalMultipleHom_injective
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = Stacks.SheafOfModules.picardClass (projectiveLineProj k).presheaf
      (structureIsSheaf (projectiveLineProj k).toRingedSpace)
      (ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) (-1))
      (isInvertible_twistingSheaf_projectiveLine k (-1))) :
    Function.Injective (negativeExceptionalMultipleHom D)

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegree_negativeExceptionalMultiple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 112. The attribute's comment: “the splitting: the degree of O_X(-nE) on the exceptional curve is n”.

Stacks Project, Tag 0C5L, the splitting. The degree of 𝒪_X(-nE) on the exceptional curve is n, so the sequence of the tag is split by n ↦ 𝒪_X(-nE).

public theorem exceptionalDegree_negativeExceptionalMultiple
    (hE : D.IsExceptionalCurveOfFirstKind k e) (n : ℤ) :
    D.exceptionalDegree k e (negativeExceptionalMultipleHom D n) = n

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegree_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 122. The attribute's comment: “right exactness: the degree map Pic(X) ⟶ Z on the exceptional curve is surjective, witnessed by the splitting n ↦ O_X(-nE)”.

Stacks Project, Tag 0C5L, right exactness. The degree map on the exceptional curve is surjective onto ℤ, because 𝒪_X(-nE) has degree n.

public theorem exceptionalDegree_surjective (hE : D.IsExceptionalCurveOfFirstKind k e) :
    Function.Surjective (D.exceptionalDegree k e)

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegree_picardClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 130. The attribute's comment: “the normalization of the degree map: O_X(E) has degree -1 on the exceptional curve”.

The degree of 𝒪_X(E) on the exceptional curve is -1, the source's reading of the definition of an exceptional curve of the first kind.

public theorem exceptionalDegree_picardClass (hE : D.IsExceptionalCurveOfFirstKind k e) :
    D.exceptionalDegree k e (Stacks.Divisors.picardClass D) = -1

AlgebraicGeometry.Scheme.IdealSheafData.negativeExceptionalMultipleHom_injective', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 138. The attribute's comment: “the splitting n ↦ O_X(-nE) is injective, so Z is a direct summand of Pic(X)”.

The splitting of the sequence is injective, so ℤ is a direct summand of Pic(X): distinct multiples 𝒪_X(-nE) have distinct degrees on the exceptional curve.

public theorem negativeExceptionalMultipleHom_injective'
    (hE : D.IsExceptionalCurveOfFirstKind k e) :
    Function.Injective (negativeExceptionalMultipleHom D)

AlgebraicGeometry.Scheme.IdealSheafData.injective_schemePullbackClassHom_of_isContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 153. The attribute's comment: “left exactness: pullback Pic(X') ⟶ Pic(X) along the contraction of the exceptional curve is injective”.

Stacks Project, Tag 0C5L, left exactness. Pullback of Picard classes along the contraction of an exceptional curve of the first kind is injective: the structure-sheaf comparison 𝒪_{X'} ⟶ b_*𝒪_X of a contraction is an isomorphism, and pullback along a morphism with that property is injective.

public theorem injective_schemePullbackClassHom_of_isContraction
    (hb : IsContractionOfExceptionalCurve D b) :
    Function.Injective (Stacks.Picard.schemePullbackClassHom b)

AlgebraicGeometry.Scheme.IdealSheafData.exceptionalDegree_schemePullbackClassHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardContraction.lean, line 208. The attribute's comment: “exactness at Pic(X), the inclusion of the image of b^* in the kernel of the degree: a class pulled back along the contraction has degree zero on the exceptional curve”.

Stacks Project, Tag 0C5L, the inclusion im(b^*) ⊆ ker(deg). A Picard class pulled back along the contraction has degree zero on the exceptional curve: the curve maps into the one-point subscheme it is contracted to, whose Picard group vanishes.

public theorem exceptionalDegree_schemePullbackClassHom
    (hb : IsContractionOfExceptionalCurve D b) (L' : Stacks.Picard.ofScheme X') :
    D.exceptionalDegree k e (Stacks.Picard.schemePullbackClassHom b L') = 0

AlgebraicGeometry.contractionPicardExactness_exceptionalIdealData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardExactness.lean, line 123. The attribute's comment: “exactness at Pic(X), the inclusion of the kernel of the degree in the image of b^*, for the blowup of a regular local ring of dimension two in its maximal ideal: with nothing assumed”.

Let (A, 𝔪, κ) be a regular local ring of dimension two, let X ⟶ Spec A be the blowing up of Spec A in 𝔪 and let E be its exceptional divisor, presented as an exceptional curve of the first kind by e : 𝐏¹_k ≅ E. Then every Picard class of X of degree zero on E is pulled back along any morphism out of X.

public theorem contractionPicardExactness_exceptionalIdealData (A : Type u) [CommRing A]
    [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) (k : Type u) [Field k]
    {e : projectiveLineProj k ≅
      (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).subscheme}
    (hE : (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).IsExceptionalCurveOfFirstKind k e)
    {X' : Scheme.{u}} (b : Stacks.Blowup.blowUpSpec (maximalIdeal A) ⟶ X') :
    (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).ContractionPicardExactness k e b

AlgebraicGeometry.Scheme.IdealSheafData.picardShortExactSequence_of_isContraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardShortExactSequence.lean, line 79. The attribute's comment: “the short exact sequence 0 → Pic(X') → Pic(X) → Z → 0 of the contraction of an exceptional curve of the first kind, in one statement with every clause written out: pullback along b is injective, a class has degree zero on the exceptional curve iff it is pulled back along b, the degree is surjective onto Z, the splitting n ↦ O_X(-nE) is a section of the degree, and O_X(E) has degree -1”.

Stacks Project, Tag 0C5L: the Picard short exact sequence of the contraction of an exceptional curve of the first kind, together with its splitting. Let b : X ⟶ X' contract the exceptional curve of the first kind E ⊆ X cut out by the ideal sheaf D and presented as 𝐏¹_k by the isomorphism e. Then

0 ⟶ Pic(X') ⟶ Pic(X) ⟶ ℤ ⟶ 0

is exact, and split by n ↦ 𝒪_X(-nE); the first map is pullback along b and the second is the degree on E. The five clauses below are, in order:

exactness at Pic(X'): pullback along b is injective;

exactness at Pic(X), both inclusions at once: a class of X has degree zero on E if and only if it is pulled back along b;

exactness at ℤ: the degree on E is onto ℤ;

the splitting: 𝒪_X(-nE) has degree n on E, so n ↦ 𝒪_X(-nE) is a section of the degree map;

the normalization of the degree: 𝒪_X(E) has degree -1 on E.

Being an effective Cartier divisor is the first clause of the hypothesis that D cuts out an exceptional curve of the first kind, so nothing is assumed here beyond the contraction and the curve it contracts.

public theorem picardShortExactSequence_of_isContraction
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e) :
    Function.Injective (Stacks.Picard.schemePullbackClassHom b) ∧
      (∀ L : Stacks.Picard.ofScheme X, D.exceptionalDegree k e L = 0 ↔
        ∃ L' : Stacks.Picard.ofScheme X', Stacks.Picard.schemePullbackClassHom b L' = L) ∧
      Function.Surjective (D.exceptionalDegree k e) ∧
      (∀ n : ℤ, D.exceptionalDegree k e (negativeExceptionalMultipleHom D n) = n) ∧
      D.exceptionalDegree k e (Stacks.Divisors.picardClass D) = -1

Tag 0C5M, a remark

Tag 0C5M in the Stacks Project.

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition_of_isContraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 331. The attribute's comment: “the identification Pic(X) = Pic(X') ⊕ Z for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction, exactness at Pic(X) discharged”.

The identification Pic(X) = Pic(X') ⊕ ℤ for b : X ⟶ X' the contraction of an exceptional curve of the first kind E ⊆ X: a class ℒ on X corresponds to the pair (ℒ', n) with n the degree of ℒ on E, and a pair (ℒ', n) to the class of (b^*ℒ')(-nE).

public def picardDecomposition_of_isContraction
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e) :
    Stacks.Picard.ofScheme X ≃+ Stacks.Picard.ofScheme X' × ℤ

AlgebraicGeometry.Scheme.IdealSheafData.contractedPicardHom_of_isContraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 344. The attribute's comment: “the assignment L ↦ L' is a group homomorphism, for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction, exactness at Pic(X) discharged”.

The homomorphism ℒ ↦ ℒ' of the contraction b : X ⟶ X' of an exceptional curve of the first kind. It sends a Picard class ℒ of X to the unique class ℒ' on X' with ℒ(nE) = b^*ℒ', where n is the degree of ℒ on the exceptional curve.

public def contractedPicardHom_of_isContraction
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e) :
    Stacks.Picard.ofScheme X →+ Stacks.Picard.ofScheme X'

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition_of_isContraction_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 373. The attribute's comment: “the characterisation: L corresponds to the pair (L', n) if and only if L = (b^*L')(-nE), for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction”.

For the contraction of an exceptional curve of the first kind, a class ℒ corresponds under the decomposition to the pair (ℒ', n) if and only if ℒ = (b^*ℒ')(-nE).

public theorem picardDecomposition_of_isContraction_eq_iff
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e) (L : Stacks.Picard.ofScheme X)
    (L' : Stacks.Picard.ofScheme X') (n : ℤ) :
    D.picardDecomposition_of_isContraction k e b hb hE L = (L', n) ↔
      L = Stacks.Picard.schemePullbackClassHom b L' + negativeExceptionalMultipleHom D n

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition_of_isContraction_eq_iff_exceptionalTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 388. The attribute's comment: “the characterisation in the source's second form: L corresponds to (L', n) if and only if L(nE) = b^*L', for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction”.

For the contraction of an exceptional curve of the first kind, a class ℒ corresponds under the decomposition to the pair (ℒ', n) if and only if ℒ(nE) is the pullback of ℒ' along b.

public theorem picardDecomposition_of_isContraction_eq_iff_exceptionalTwist
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e) (L : Stacks.Picard.ofScheme X)
    (L' : Stacks.Picard.ofScheme X') (n : ℤ) :
    D.picardDecomposition_of_isContraction k e b hb hE L = (L', n) ↔
      D.exceptionalTwist n L = Stacks.Picard.schemePullbackClassHom b L'

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition_of_isContraction_apply_fst_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ContractionPicardDescent.lean, line 413. The attribute's comment: “the formula L' = b_L(nE) read off the proof of Tag 0C5L, stated for every pushforward on Picard classes left inverse to b^, for a general contraction of an exceptional curve of the first kind: with nothing assumed beyond the contraction, exactness at Pic(X) discharged and such a pushforward exhibited”.

For the contraction of an exceptional curve of the first kind, the Pic(X')-component of the decomposition is p(ℒ(nE)), with n the degree of ℒ on the exceptional curve, for every pushforward p on Picard classes left inverse to b^*.

public theorem picardDecomposition_of_isContraction_apply_fst_pushforward
    (hb : IsContractionOfExceptionalCurve D b)
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (p : Stacks.Picard.ofScheme X →+ Stacks.Picard.ofScheme X')
    (hp : ∀ L' : Stacks.Picard.ofScheme X',
      p (Stacks.Picard.schemePullbackClassHom b L') = L')
    (L : Stacks.Picard.ofScheme X) :
    (D.picardDecomposition_of_isContraction k e b hb hE L).1 =
      p (D.exceptionalTwist (D.exceptionalDegree k e L) L)

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardDecomposition.lean, line 254. The attribute's comment: “the identification Pic(X) = Pic(X') ⊕ Z, granted the two halves of Tag 0C5L the library does not prove — a pushforward b_ left inverse to b^, and exactness at Pic(X) — bundled as the hypothesis ContractionPicardSplitting, and granted the identification Z ≃+ Pic(P¹_k) of Tag 0BXJ, of which the library has only the injectivity half”.

Stacks Project, Tag 0C5M: the identification Pic(X) = Pic(X') ⊕ ℤ. For the contraction b : X ⟶ X' of an exceptional curve of the first kind, a class ℒ on X is sent to the pair (b_*ℒ(nE), n) with n the degree of ℒ on the exceptional curve, and a pair (ℒ', n) back to the class of (b^*ℒ')(-nE).

public def picardDecomposition (hb : D.ContractionPicardSplitting k e φ b)
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = projectiveLineTwistPicardClass k (-1)) :
    Stacks.Picard.ofScheme X ≃+ Stacks.Picard.ofScheme X' × ℤ

AlgebraicGeometry.Scheme.IdealSheafData.picardDecomposition_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardDecomposition.lean, line 290. The attribute's comment: “the characterisation: L corresponds to the pair (L', n) if and only if L = (b^*L')(-nE), granted the two halves of Tag 0C5L the library does not prove, bundled as the hypothesis ContractionPicardSplitting, and the identification Z ≃+ Pic(P¹_k) of Tag 0BXJ”.

Stacks Project, Tag 0C5M: the characterisation of the decomposition. A class ℒ corresponds to the pair (ℒ', n) if and only if ℒ = (b^*ℒ')(-nE).

public theorem picardDecomposition_eq_iff (hb : D.ContractionPicardSplitting k e φ b)
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = projectiveLineTwistPicardClass k (-1)) (L : Stacks.Picard.ofScheme X)
    (L' : Stacks.Picard.ofScheme X') (n : ℤ) :
    picardDecomposition hb hE hφ L = (L', n) ↔
      L = Stacks.Picard.schemePullbackClassHom b L' + D.negativeExceptionalMultipleHom n

AlgebraicGeometry.Scheme.IdealSheafData.contractedPicardHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardDecomposition.lean, line 308. The attribute's comment: “the assignment L ↦ L' is a group homomorphism, granted the two halves of Tag 0C5L the library does not prove, bundled as the hypothesis ContractionPicardSplitting, and granted the identification Z ≃+ Pic(P¹_k) of Tag 0BXJ”.

Stacks Project, Tag 0C5M: the assignment ℒ ↦ ℒ' is a group homomorphism. It is the Pic(X')-component of the decomposition Pic(X) ≃+ Pic(X') × ℤ.

public def contractedPicardHom (hb : D.ContractionPicardSplitting k e φ b)
    (hE : D.IsExceptionalCurveOfFirstKind k e)
    (hφ : φ (-1) = projectiveLineTwistPicardClass k (-1)) :
    Stacks.Picard.ofScheme X →+ Stacks.Picard.ofScheme X'

AlgebraicGeometry.picardDecomposition_exceptionalIdealData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardExactness.lean, line 168. The attribute's comment: “the identification Pic(X) = Pic(X') ⊕ Z for the blowup of a regular local ring of dimension two in its maximal ideal: with nothing assumed, both hypotheses of the general decomposition discharged”.

Let (A, 𝔪, κ) be a regular local ring of dimension two and let b : X ⟶ Spec A be the blowing up of Spec A in 𝔪, with exceptional divisor E presented as an exceptional curve of the first kind by e : 𝐏¹_k ≅ E. Then Pic(X) ≃+ Pic(Spec A) × ℤ, a class ℒ corresponding to the pair (ℒ', n) with n the degree of ℒ on E exactly when ℒ = (b^*ℒ')(-nE).

public def picardDecomposition_exceptionalIdealData (A : Type u) [CommRing A]
    [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) (k : Type u) [Field k]
    {e : projectiveLineProj k ≅
      (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).subscheme}
    (hE : (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).IsExceptionalCurveOfFirstKind
      k e) :
    Stacks.Picard.ofScheme (Stacks.Blowup.blowUpSpec (maximalIdeal A)) ≃+
      Stacks.Picard.ofScheme (Spec (CommRingCat.of A)) × ℤ

AlgebraicGeometry.contractedPicardHom_exceptionalIdealData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurvePicardExactness.lean, line 188. The attribute's comment: “the assignment L ↦ L' is a group homomorphism, for the blowup of a regular local ring of dimension two in its maximal ideal: with nothing assumed”.

The homomorphism ℒ ↦ ℒ' of the blowup of a regular local ring of dimension two in its maximal ideal. It sends a Picard class ℒ of the blowup to the unique class ℒ' on Spec A with ℒ(nE) = b^*ℒ', where n is the degree of ℒ on the exceptional curve. It is the Pic(Spec A)-component of AlgebraicGeometry.picardDecomposition_exceptionalIdealData.

public def contractedPicardHom_exceptionalIdealData (A : Type u) [CommRing A]
    [IsRegularLocalRing A] (hdim : ringKrullDim A = 2) (k : Type u) [Field k]
    {e : projectiveLineProj k ≅
      (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).subscheme}
    (hE : (Stacks.Blowup.exceptionalIdealData (maximalIdeal A)).IsExceptionalCurveOfFirstKind
      k e) :
    Stacks.Picard.ofScheme (Stacks.Blowup.blowUpSpec (maximalIdeal A)) →+
      Stacks.Picard.ofScheme (Spec (CommRingCat.of A))

Tag 0C2J, a lemma

Tag 0C2J in the Stacks Project.

Stacks.Surfaces.isZero_rightDerived_one_divisorTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveDivisorTwist.lean, line 135. The attribute's comment: “assertion (1): H^1 vanishes on the twists ℒ(iE) for 0 ≤ i ≤ n+1”.

[Stacks, Tag 0C2J], assertion (1). Let E ⊆ X be an exceptional curve of the first kind on a scheme X, let ℒ be an invertible 𝒪_X-module, and let n be the degree of ℒ|_E as an invertible module on 𝐏¹, recorded as an isomorphism e^*i^*ℒ ≅ 𝒪(n). If H¹(X, ℒ) = 0 and 0 ≤ n then

H¹(X, ℒ(iE)) = 0 for every 0 ≤ i ≤ n + 1.

The induction is on i, along the ideal sequence of E twisted by ℒ((i+1)E):

0 ⟶ ℒ(iE) ⟶ ℒ((i+1)E) ⟶ ℒ((i+1)E)|_E ⟶ 0,

whose first term is identified by Stacks.Surfaces.twistedIdealIso and whose third restricts to 𝒪(n - i - 1) on 𝐏¹. For i ≤ n that degree is at least -1, so the third term has no H¹ by Stacks.Surfaces.isZero_rightDerived_one_tensorPushforwardUnit, and the degree-one row of the long exact sequence forces H¹ of the middle term to vanish. The hypothesis 0 ≤ n is the source's and is carried unchanged; the induction consumes only i ≤ n + 1, since the step that produces ℒ((j+1)E) gets the j ≤ n it needs from j + 1 ≤ n + 1.

theorem isZero_rightDerived_one_divisorTwist (E : X.IdealSheafData) (k : Type u) [Field k]
    {e : projectiveLineProj k ≅ E.subscheme}
    (hE : E.IsExceptionalCurveOfFirstKind k e)
    (L : _root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf))
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    {n : ℤ} (_hn : 0 ≤ n)
    (hdeg : (modulePullback e.hom.toLRSHom.toShHom).obj
        ((modulePullback E.subschemeι.toLRSHom.toShHom).obj L) ≅
      ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) n)
    (hL : IsZero (((moduleGlobalSections X).rightDerived 1).obj L))
    (i : ℕ) (hi : (i : ℤ) ≤ n + 1) :
    IsZero (((moduleGlobalSections X).rightDerived 1).obj (divisorTwist E L i))

Stacks.Surfaces.mono_rightDerived_one_map_tensorCanonicalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveTwistInjectivity.lean, line 421. The attribute's comment: “assertion (2): injectivity on H^1 when the degree is non-positive”.

[Stacks, Tag 0C2J], assertion (2). Let E ⊆ X be an exceptional curve of the first kind on a scheme X, let ℒ be an invertible 𝒪_X-module, and let n be the degree of ℒ|_E as an invertible module on 𝐏¹, recorded as an isomorphism e^*i^*ℒ ≅ 𝒪(n). If n ≤ 0 then multiplication by the canonical section 1_E makes H¹(X, ℒ) a submodule of H¹(X, ℒ(E)).

The map is Stacks.Divisors.tensorCanonicalSection, the canonical map ℒ ⟶ ℒ ⊗ 𝒪_X(E) of multiplication by 1_E, and not merely some isomorphic copy of it.

theorem mono_rightDerived_one_map_tensorCanonicalSection (E : X.IdealSheafData) (k : Type u)
    [Field k] {e : projectiveLineProj k ≅ E.subscheme}
    (hE : E.IsExceptionalCurveOfFirstKind k e)
    (L : _root_.SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (X).sheaf)))
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    {n : ℤ} (hn : n ≤ 0)
    (hdeg : (modulePullback e.hom.toLRSHom.toShHom).obj
        ((modulePullback E.subschemeι.toLRSHom.toShHom).obj L) ≅
      ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) n) :
    Mono (((moduleGlobalSections X).rightDerived 1).map (tensorCanonicalSection E L))

Stacks.Surfaces.isZero_rightDerived_one_tensorInvertibleSheafPow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Surfaces/ExceptionalCurveTwistVanishing.lean, line 329. The attribute's comment: “assertion (1): vanishing through the twists of nonnegative degree”.

[Stacks, Tag 0C2J], assertion (1). Let E ⊆ X be an exceptional curve of the first kind on a scheme X, let ℒ be an invertible 𝒪_X-module, and let n be the degree of ℒ|_E as an invertible module on 𝐏¹, recorded as an isomorphism e^*i^*ℒ ≅ 𝒪(n). If H¹(X, ℒ) = 0 and n ≥ 0 then H¹(X, ℒ(iE)) = 0 for every 0 ≤ i ≤ n + 1.

Here ℒ(iE) is ℒ ⊗ 𝒪_X(iE) with iE = E ^ i the i-fold sum of E with itself in the monoid of effective Cartier divisors.

theorem isZero_rightDerived_one_tensorInvertibleSheafPow (E : X.IdealSheafData) (k : Type u)
    [Field k] {e : projectiveLineProj k ≅ E.subscheme}
    (hE : E.IsExceptionalCurveOfFirstKind k e)
    (L : _root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf))
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    {n : ℤ} (_hn : 0 ≤ n)
    (hdeg : (modulePullback e.hom.toLRSHom.toShHom).obj
        ((modulePullback E.subschemeι.toLRSHom.toShHom).obj L) ≅
      ProjectiveSpectrum.Proj.twistingSheaf
        (MvPolynomial.homogeneousSubmodule (Fin 2) k) n)
    (h0 : IsZero (((moduleGlobalSections X).rightDerived 1).obj L))
    (i : ℕ) (hi : (i : ℤ) ≤ n + 1) :
    IsZero (((moduleGlobalSections X).rightDerived 1).obj
      (MonoidalCategory.tensorObj (C := _root_.SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf X.sheaf))
        L (invertibleSheaf' (E ^ i))))

Tag 0C2M, a lemma

Tag 0C2M in the Stacks Project.

AlgebraicGeometry.exists_contraction_isProper_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/ContractExceptionalCurveAmple.lean, line 326.

[Stacks, Tag 0C2M]. Let S = Spec R be an affine Noetherian scheme, f : X ⟶ S a proper morphism, ℒ an ample invertible 𝒪_X-module, and E ⊆ X an exceptional curve of the first kind, cut out by D and presented as 𝐏¹_k by e. Then

there exists a contraction b : X ⟶ X' of E;

X' is proper over S: the structure morphism factors as b ≫ f' with f' proper;

the invertible 𝒪_{X'}-module ℒ' of [Stacks, Remark 0C5M] is ample. Here ℒ has a degree n on E (its restriction to 𝐏¹_k is 𝒪(n)), and ℒ' is an invertible 𝒪_{X'}-module with b^*ℒ' = ℒ(nE) in Pic(X), i.e. b^*[ℒ'] = [ℒ] + n • [𝒪_X(E)] (AlgebraicGeometry.Scheme.IdealSheafData.exceptionalTwist). Such an ℒ' exists, and every such ℒ' is ample; it is unique up to isomorphism by AlgebraicGeometry.IsContractionOfExceptionalCurve.nonempty_iso_of_schemePullbackClass_eq.

public theorem exists_contraction_isProper_isAmple {R : Type u} [CommRing R] [IsNoetherianRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of R)) [IsProper f]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L] (hL : Scheme.Modules.IsAmple X L)
    {D : X.IdealSheafData} {k : Type u} [Field k] {e : projectiveLineProj k ≅ D.subscheme}
    (hE : D.IsExceptionalCurveOfFirstKind k e) :
    ∃ (X' : Scheme.{u}) (b : X ⟶ X'),
      IsContractionOfExceptionalCurve D b ∧
      (∃ f' : X' ⟶ Spec (.of R), b ≫ f' = f ∧ IsProper f') ∧
      (∃ n : ℤ, Nonempty ((modulePullback e.hom.toLRSHom.toShHom).obj
          ((modulePullback D.subschemeι.toLRSHom.toShHom).obj L) ≅
        ProjectiveSpectrum.Proj.twistingSheaf (MvPolynomial.homogeneousSubmodule (Fin 2) k) n)) ∧
      ∀ n : ℤ, Nonempty ((modulePullback e.hom.toLRSHom.toShHom).obj
          ((modulePullback D.subschemeι.toLRSHom.toShHom).obj L) ≅
        ProjectiveSpectrum.Proj.twistingSheaf (MvPolynomial.homogeneousSubmodule (Fin 2) k) n) →
        (∃ (L' : X'.Modules) (_ : Stacks.Ample.IsInvertibleModule X' L'),
          Stacks.Picard.schemePullbackClass b (cls L') =
            (haveI := hE.isEffectiveCartierDivisor; D.exceptionalTwist n (cls L))) ∧
        ∀ (L' : X'.Modules) [Stacks.Ample.IsInvertibleModule X' L'],
          Stacks.Picard.schemePullbackClass b (cls L') =
            (haveI := hE.isEffectiveCartierDivisor; D.exceptionalTwist n (cls L)) →
          Scheme.Modules.IsAmple X' L'

Tag 0C2N, a lemma

Tag 0C2N in the Stacks Project.

AlgebraicGeometry.exists_isContractionOfExceptionalCurve_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/Contraction/ProjectiveContraction.lean, line 409. The attribute's comment: “(1)”.

[Stacks, Tag 0C2N] (1). Let S be a Noetherian scheme and f : X ⟶ S a morphism of finite type. Let E ⊆ X be an exceptional curve of the first kind, cut out by D and presented as 𝐏¹_k by e, which lies in the fibre of f over a point s. If X is projective over S, then there exists a contraction b : X ⟶ X' of E, and X' is projective over S: the structure morphism factors as b ≫ g with g projective.

theorem exists_isContractionOfExceptionalCurve_isProjective {X S : Scheme.{u}} [IsNoetherian S]
    (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f] {D : X.IdealSheafData} {k : Type u}
    [Field k] {e : projectiveLineProj k ≅ D.subscheme} (hE : D.IsExceptionalCurveOfFirstKind k e)
    (s : S) (hs : ∀ x ∈ (D.support : Set X), f.base x = s) (hf : IsProjective f) :
    ∃ (X' : Scheme.{u}) (b : X ⟶ X') (g : X' ⟶ S),
      IsContractionOfExceptionalCurve D b ∧ b ≫ g = f ∧ IsProjective g

AlgebraicGeometry.exists_isContractionOfExceptionalCurve_isQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/Contraction/QuasiProjectiveContraction.lean, line 219. The attribute's comment: “(2)”.

[Stacks, Tag 0C2N] (2). Let S be a Noetherian scheme and f : X ⟶ S a morphism of finite type. Let E ⊆ X be an exceptional curve of the first kind, cut out by D and presented as 𝐏¹_k by e, which lies in the fibre of f over a point s. If X is quasi-projective over S, then there exists a contraction b : X ⟶ X' of E, and X' is quasi-projective over S: the structure morphism factors as b ≫ g with g quasi-projective.

theorem exists_isContractionOfExceptionalCurve_isQuasiProjective {X S : Scheme.{u}}
    [IsNoetherian S] (f : X ⟶ S) [LocallyOfFiniteType f] [QuasiCompact f]
    {D : X.IdealSheafData} {k : Type u} [Field k] {e : projectiveLineProj k ≅ D.subscheme}
    (hE : D.IsExceptionalCurveOfFirstKind k e) (s : S)
    (hs : ∀ x ∈ (D.support : Set X), f.base x = s) (hf : IsQuasiProjective f) :
    ∃ (X' : Scheme.{u}) (b : X ⟶ X') (g : X' ⟶ S),
      IsContractionOfExceptionalCurve D b ∧ b ≫ g = f ∧ IsQuasiProjective g

Tag 0C5N, a lemma

Tag 0C5N in the Stacks Project.

AlgebraicGeometry.isQuasiProjective_of_isRegular_of_topologicalKrullDim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuasiProjectiveRegularSurface.lean, line 193.

Stacks Project, Tag 0C5N. Let S be a Noetherian scheme and f : X ⟶ S a separated morphism of finite type with X regular of dimension (at most) two. Then f is quasi-projective.

The source assumes dim X = 2; the argument only uses dim X ≤ 2, which is what is assumed.

theorem isQuasiProjective_of_isRegular_of_topologicalKrullDim_le_two
    {X S : Scheme.{u}} [IsNoetherian S] (f : X ⟶ S) [IsSeparated f]
    [LocallyOfFiniteType f] [QuasiCompact f] (hreg : IsRegular X)
    (hdim : topologicalKrullDim X ≤ 2) : IsQuasiProjective f

Tag 0C5P, a lemma

Tag 0C5P in the Stacks Project.

AlgebraicGeometry.isProjective_of_isRegular_of_topologicalKrullDim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuasiProjectiveRegularSurface.lean, line 238. References: SGA 7 X (1.10), “more general”.

Stacks Project, Tag 0C5P. Let S be a Noetherian scheme and f : X ⟶ S a proper morphism with X regular of dimension (at most) two. Then f is projective.

This is [Stacks, Tag 0C5N] together with [Stacks, Tag 0BCL]: a proper quasi-projective morphism to a quasi-compact quasi-separated scheme is projective. The source assumes dim X = 2; the argument only uses dim X ≤ 2.

theorem isProjective_of_isRegular_of_topologicalKrullDim_le_two {X S : Scheme.{u}}
    [IsNoetherian S] (f : X ⟶ S) [IsProper f] (hreg : IsRegular X)
    (hdim : topologicalKrullDim X ≤ 2) : IsProjective f

Sources

LeanAlgebraicGeometry.Scheme.IdealSheafData.ExistsContraction · AlgebraicGeometry.Scheme.IdealSheafData.IsExceptionalCurveOfFirstKind · Stacks.Blowup.exists_isExceptionalCurveOfFirstKind_exceptionalIdeal_vanishingIdeal · AlgebraicGeometry.existsUnique_comp_eq_of_isContractionOfExceptionalCurve · AlgebraicGeometry.existsUnique_iso_of_isContractionOfExceptionalCurve · AlgebraicGeometry.Scheme.IdealSheafData.isNoetherianCompleteLocalRing_formalNeighborhoodRing · AlgebraicGeometry.Scheme.IdealSheafData.isRegularLocalRing_formalNeighborhoodRing · AlgebraicGeometry.Scheme.IdealSheafData.ringKrullDim_formalNeighborhoodRing_eq_two

Section54.17 Factorization birational maps #

Section 54.17 of the Stacks Project, Tag 0C5Q. 2 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0C5R, a lemma

Tag 0C5R in the Stacks Project.

Stacks.ResolutionOfSurfaces.factorsAsPointBlowups_of_proper_birational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/FactorizationBirationalSurfaces.lean, line 278. The attribute's comment: “the conclusion in full; the inputs hsec, blowUpSurface and square remain named arguments and descent is reduced to the drop of the measure, as the module documentation records”.

Stacks Project, Tag 0C5R. Let f : X ⟶ Y be a proper birational morphism between integral Noetherian schemes regular of dimension two. Then f is a sequence of blowups in closed points, that is, f is up to an isomorphism of its source the composite of a chain of blowups at closed points.

Three inputs are arguments rather than theorems: hsec, the second arrow of [Stacks, Tag 067L]; blowUpSurface, the regularity ([Stacks, Tag 0AGR] globally) and the dimension of the blowup at a closed point; and square, the reduction of [Stacks, Tag 0C5H] to a single blowup together with the dichotomy of the source's step 3. The fourth argument descent is the strict drop of the measure μ, the bookkeeping the source omits. None of them is inter-derivable with the conclusion; see the module documentation.

public theorem factorsAsPointBlowups_of_proper_birational
    (hsec : ConormalSequenceSecondArrow.{u}) (μ : ∀ (A B : Scheme.{u}), (B ⟶ A) → ℕ)
    (blowUpSurface : ∀ (A : Scheme.{u}) (a : A) (ha : IsClosed ({a} : Set A)),
      IsIntegralRegularSurface A →
        IsRegular (pointBlowUp ha) ∧ topologicalKrullDim (pointBlowUp ha) = 2)
    (square : ∀ (A B : Scheme.{u}) (g : B ⟶ A), IsIntegralRegularSurface A →
      IsIntegralRegularSurface B → IsProper g → IsBirational g → ¬ IsIso g →
      ∀ (a : A) (ha : IsClosed ({a} : Set A)) (U : A.Opens),
        IsGreatest { V : A.Opens | IsIso (g ∣_ V) } U → a ∉ U →
          HasExceptionalSquareAt g a ha)
    (descent : ∀ (A B : Scheme.{u}) (g : B ⟶ A), IsIntegralRegularSurface A →
      IsIntegralRegularSurface B → IsProper g → IsBirational g → ¬ IsIso g →
      ∀ (a : A) (ha : IsClosed ({a} : Set A)) (U : A.Opens),
        IsGreatest { V : A.Opens | IsIso (g ∣_ V) } U → a ∉ U →
          ∀ ψ : B ⟶ pointBlowUp ha, ψ ≫ pointBlowUpToBase ha = g →
            μ (pointBlowUp ha) B ψ < μ A B g)
    {X Y : Scheme.{u}} (f : X ⟶ Y) (hY : IsIntegralRegularSurface Y)
    (hX : IsIntegralRegularSurface X) (hproper : IsProper f) (hbirational : IsBirational f) :
    FactorsAsPointBlowups Y Set.univ X f

Stacks.ResolutionOfSurfaces.factorsAsPointBlowups_of_isProper_of_isBirational, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/PointBlowupFactorizationStep.lean, line 876.

Stacks Project, Tag 0C5R. Let f : X ⟶ Y be a proper birational morphism between integral Noetherian schemes regular of dimension two. Then f is a sequence of blowups in closed points.

theorem factorsAsPointBlowups_of_isProper_of_isBirational {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hY : IsIntegralRegularSurface Y) (hX : IsIntegralRegularSurface X) (hproper : IsProper f)
    (hbirational : IsBirational f) : FactorsAsPointBlowups Y Set.univ X f

Tag 0C5S, a lemma

Tag 0C5S in the Stacks Project.

Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/FactorizationBirationalMaps.lean, line 244. The attribute's comment: “the converse direction, which the source states without proof: a two-sided chain of blowups in closed points makes X and Y birational over the base. Unconditional apart from blowUpSurface (the globalization of Tag 0AGR); the route is Tag 02OS, nonvanishing of the point's ideal sheaf, and Tag 0BAD”.

The converse direction of [Stacks, Tag 0C5S], whose proof the source omits. A morphism which is a finite sequence of blowups at closed points of an integral Noetherian scheme regular of dimension two makes its source birational to the target over any base.

public theorem birationalOver_comp_of_factorsAsPointBlowups
    (blowUpSurface : ∀ (A : Scheme.{u}) (a : A) (ha : IsClosed ({a} : Set A)),
      IsIntegralRegularSurface A →
        IsIntegralRegularSurface
          (blowUp (Scheme.IdealSheafData.vanishingIdeal (⟨{a}, ha⟩ : Closeds A))))
    {S X Z : Scheme.{u}} (sX : X ⟶ S) (hX : IsIntegralRegularSurface X) {f : Z ⟶ X}
    (hf : FactorsAsPointBlowups X Set.univ Z f) :
    Scheme.BirationalOver (f ≫ sX) sX

Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/FactorizationBirationalMapsUnconditional.lean, line 106. The attribute's comment: “one side of the converse direction, which the source states without proof: a chain of blowups in closed points out of X makes its source birational to X over the base. The route is Tag 02OS, nonvanishing of the point's ideal sheaf, and Tag 0BAD, and the blowup of such a scheme at a closed point is again such a scheme by the globalization of Tag 0AGR, AlgebraicGeometry.isRegular_and_topologicalKrullDim_blowUp_vanishingIdeal_singleton”.

One side of the converse direction of [Stacks, Tag 0C5S], whose proof the source omits. A morphism which is a finite sequence of blowups at closed points of an integral Noetherian scheme regular of dimension two makes its source birational to the target over any base.

public theorem birationalOver_comp_of_factorsAsPointBlowups_unconditional
    {S X Z : Scheme.{u}} (sX : X ⟶ S) (hX : IsIntegralRegularSurface X) {f : Z ⟶ X}
    (hf : FactorsAsPointBlowups X Set.univ Z f) :
    Scheme.BirationalOver (f ≫ sX) sX

Stacks.ResolutionOfSurfaces.birationalOver_of_exists_factorsAsPointBlowups, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/FactorizationBirationalMapsUnconditional.lean, line 130. The attribute's comment: “the implication from the two-sided chain of blowups in closed points to S-birationality of X and Y, which is the direction the source states without proof. Nothing is assumed: the two sides are composed through Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups_unconditional and the symmetry and transitivity of AlgebraicGeometry.Scheme.BirationalOver”.

The converse direction of [Stacks, Tag 0C5S], whose proof the source omits. Let S be a Noetherian scheme and let X and Y be proper integral schemes over S which are regular of dimension two. If there is a scheme Z with S-morphisms f : Z ⟶ X and g : Z ⟶ Y, each a finite sequence of blowups at closed points, then X and Y are S-birational.

This is the implication of the source's if and only if that the source states without proof, and it is proved here with nothing assumed: each of the two sides makes Z birational to its target over S by Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups_unconditional, and S-birationality is symmetric and transitive.

public theorem birationalOver_of_exists_factorsAsPointBlowups
    {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
    (hX : IsIntegralRegularSurface X) (hY : IsIntegralRegularSurface Y)
    (h : ∃ (Z : Scheme.{u}) (f : Z ⟶ X) (g : Z ⟶ Y),
      f ≫ (X ↘ S) = g ≫ (Y ↘ S) ∧
        FactorsAsPointBlowups X Set.univ Z f ∧ FactorsAsPointBlowups Y Set.univ Z g) :
    Scheme.BirationalOver (X ↘ S) (Y ↘ S)

Stacks.ResolutionOfSurfaces.birationalOver_iff_exists_factorsAsPointBlowups_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/FactorizationBirationalSurfacesProperOverNoetherian.lean, line 60. The attribute's comment: “the tag's hypothesis list, with the surface predicate derived rather than assumed: S is Noetherian and X and Y are proper over S, integral, regular and of dimension two. The bundled Stacks.ResolutionOfSurfaces.IsIntegralRegularSurface of the other registration asks of the two schemes that they be Noetherian as well; here that is obtained from properness over S by Tag 01T6”.

Let S be a Noetherian scheme and let X and Y be proper integral schemes over S which are regular of dimension two. Then X and Y are S-birational if and only if there is a scheme Z with S-morphisms f : Z ⟶ X and g : Z ⟶ Y, each a finite sequence of blowups at closed points.

Of X and Y only the tag's own conditions are assumed: integral, regular, of dimension two, and proper over the Noetherian base. Their Noetherianness, which Stacks.ResolutionOfSurfaces.IsIntegralRegularSurface demands in addition, is derived from properness over S.

public theorem birationalOver_iff_exists_factorsAsPointBlowups_of_isRegular
    {S X Y : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S] [X.Over S] [Y.Over S]
    [IsProper (X ↘ S)] [IsProper (Y ↘ S)]
    (hXintegral : AlgebraicGeometry.IsIntegral X) (hXregular : AlgebraicGeometry.IsRegular X)
    (hXdim : topologicalKrullDim X = 2) (hYintegral : AlgebraicGeometry.IsIntegral Y)
    (hYregular : AlgebraicGeometry.IsRegular Y) (hYdim : topologicalKrullDim Y = 2) :
    Scheme.BirationalOver (X ↘ S) (Y ↘ S) ↔
      ∃ (Z : Scheme.{u}) (f : Z ⟶ X) (g : Z ⟶ Y),
        f ≫ (X ↘ S) = g ≫ (Y ↘ S) ∧
          FactorsAsPointBlowups X Set.univ Z f ∧ FactorsAsPointBlowups Y Set.univ Z g

Stacks.ResolutionOfSurfaces.birationalOver_iff_exists_factorsAsPointBlowups_of_isIntegralRegularSurface, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionOfSurfaces/QuadraticTransformations/PointBlowupFactorizationStep.lean, line 907.

Stacks Project, Tag 0C5S. Let S be a Noetherian scheme and let X and Y be proper integral schemes over S which are regular of dimension two. Then X and Y are S-birational if and only if there is a scheme Z with S-morphisms Z ⟶ X and Z ⟶ Y, each a sequence of blowups in closed points.

theorem birationalOver_iff_exists_factorsAsPointBlowups_of_isIntegralRegularSurface
    {S X Y : Scheme.{u}} [AlgebraicGeometry.IsNoetherian S] [X.Over S] [Y.Over S]
    [IsProper (X ↘ S)] [IsProper (Y ↘ S)] (hX : IsIntegralRegularSurface X)
    (hY : IsIntegralRegularSurface Y) :
    Scheme.BirationalOver (X ↘ S) (Y ↘ S) ↔
      ∃ (Z : Scheme.{u}) (f : Z ⟶ X) (g : Z ⟶ Y),
        f ≫ (X ↘ S) = g ≫ (Y ↘ S) ∧
          FactorsAsPointBlowups X Set.univ Z f ∧ FactorsAsPointBlowups Y Set.univ Z g

Sources

LeanStacks.ResolutionOfSurfaces.factorsAsPointBlowups_of_proper_birational · Stacks.ResolutionOfSurfaces.factorsAsPointBlowups_of_isProper_of_isBirational · Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups · Stacks.ResolutionOfSurfaces.birationalOver_comp_of_factorsAsPointBlowups_unconditional · Stacks.ResolutionOfSurfaces.birationalOver_of_exists_factorsAsPointBlowups · Stacks.ResolutionOfSurfaces.birationalOver_iff_exists_factorsAsPointBlowups_of_isRegular · Stacks.ResolutionOfSurfaces.birationalOver_iff_exists_factorsAsPointBlowups_of_isIntegralRegularSurface

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

54.15 Embedded resolution to 54.17 Factorization birational…

Section54.15 Embedded resolution#

Tag 0BI4, a lemma

Tag 0BI5, a lemma

Tag 0BI6, an equation

Tag 0BI7, a lemma

Tag 0BI8, a lemma

Tag 0BIB, a lemma

Tag 0BIC, a lemma

Sources

Section54.16 Contracting exceptional curves#

Tag 0C2I, the section

Tag 0C5J, a lemma

Tag 0C5K, a lemma

Tag 0C2K, a lemma

Tag 0C2L, a lemma

Tag 0C5L, a lemma

Tag 0C5M, a remark

Tag 0C2J, a lemma

Tag 0C2M, a lemma

Tag 0C2N, a lemma

Tag 0C5N, a lemma

Tag 0C5P, a lemma

Sources

Section54.17 Factorization birational maps#

Tag 0C5R, a lemma

Tag 0C5S, a lemma

Sources

Section54.15 Embedded resolution #

Section54.16 Contracting exceptional curves #

Section54.17 Factorization birational maps #